Commit 2022-01-31 22:22 59643439

View on Github →

feat(data/equiv): define mul_equiv_class (#10760) This PR defines a class of types of multiplicative (additive) equivalences, along the lines of #9888.

Estimated changes

Modified src/data/equiv/mul_add.lean

deleted theorem add_equiv.map_sub

modified theorem mul_equiv.ext

modified theorem mul_equiv.ext_iff

deleted theorem mul_equiv.map_eq_one_iff

deleted theorem mul_equiv.map_inv

deleted theorem mul_equiv.map_mul

deleted theorem mul_equiv.map_one

added theorem mul_equiv_class.map_eq_one_iff

added theorem mul_equiv_class.map_ne_one_iff

Modified src/data/fun_like/basic.lean

added theorem fun_like.coe_eq_coe_fn