mathlib3

c459d2b5 - feat(algebra/algebra/basic,data/matrix/basic): resolve a TODO about `alg_hom.map_smul_of_tower` (#12684)

feat(algebra/algebra/basic,data/matrix/basic): resolve a TODO about `alg_hom.map_smul_of_tower` (#12684) It turns out that this lemma doesn't actually help in the place I claimed it would, so I added the lemma that does help too.