Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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`.
- Loading branch information