Commit 2022-12-06 09:40 e753057a
View on Github →feat(algebra/hom/equiv/basic): Add to_additive to Pi_congr_right lemmas (#17827)
Add to_additive attribute to three lemmas about mul_equiv.Pi_congr_right.
feat(algebra/hom/equiv/basic): Add to_additive to Pi_congr_right lemmas (#17827)
Add to_additive attribute to three lemmas about mul_equiv.Pi_congr_right.