basic): Add `to_additive` to `Pi_congr_right` lemmas (#17827)

Commit

3 years ago

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`.

Author

winstonyin

Parents

10ee5ede

mathlib3 e753057a - feat(algebra/hom/equiv/basic): Add `to_additive` to `Pi_congr_right` lemmas (#17827)

mathlib3
e753057a - feat(algebra/hom/equiv/basic): Add `to_additive` to `Pi_congr_right` lemmas (#17827)