Commit 2021-05-10 07:36 b5776971
View on Github →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.