mathlib

b5776971 - feat(data/matrix/basic): add missing smul instances, generalize lemmas to work on scalar towers (#7544)

feat(data/matrix/basic): add missing smul instances, generalize lemmas to work on scalar towers (#7544) This also fixes the `add_monoid_hom.map_zero` etc lemmas to not require overly strong typeclasses on `α` This removes the `matrix.smul_apply` lemma since `pi.smul_apply` and `smul_eq_mul` together replace it.