mathlib

118e809b - refactor(algebra/module/linear_map): Move elementwise structure from linear_algebra/basic (#9331)

refactor(algebra/module/linear_map): Move elementwise structure from linear_algebra/basic (#9331) This helps reduce the size of linear_algebra/basic, and by virtue of being a smaller file makes it easier to spot typeclasses which can be relaxed. As an example, `linear_map.endomorphism_ring` now requires only `semiring R` not `ring R`. Having instances available as early as possible is generally good, as otherwise it is hard to even state things elsewhere.