Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-15 16:29 38a5f5d6

View on Github →

chore(data/equiv/mul_add): add monoid_hom.to_mul_equiv (#4628)

Estimated changes

Modified src/algebra/category/Group/basic.lean

Modified src/algebra/category/Mon/basic.lean

Modified src/data/equiv/mul_add.lean

added def add_monoid_hom.to_add_equiv

added theorem monoid_hom.coe_to_mul_equiv

added def monoid_hom.to_mul_equiv

added theorem mul_equiv.coe_to_monoid_hom