Commit 2022-03-16 19:40 c459d2b5
View on Github →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.