mathlib

56a6ed6e - chore(algebra/algebra/basic): remove a duplicate instance (#9320)

chore(algebra/algebra/basic): remove a duplicate instance (#9320) `algebra.linear_map.module'` is just a special case of `linear_map.module'`. `by apply_instance` finds this instance provided it's used after the definition of `is_scalar_tower.to_smul_comm_class`.