Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-17 14:18 21d74c7a

View on Github →

feat(data/equiv/mul_add): use @[simps] (#7213) Add some @[simps] for some algebra maps. This came up in #6795.

Estimated changes

Modified src/algebra/group/hom.lean

deleted theorem monoid_hom.coe_mk'

deleted theorem monoid_hom.id_apply

deleted theorem monoid_with_zero_hom.id_apply

deleted theorem mul_hom.id_apply

deleted theorem one_hom.id_apply

Modified src/algebra/group/hom_instances.lean

deleted theorem monoid_hom.eval_apply

Modified src/analysis/normed_space/normed_group_hom.lean

Modified src/data/equiv/mul_add.lean

deleted theorem equiv.coe_inv

deleted theorem equiv.coe_mul_left'

deleted theorem equiv.coe_mul_right'

deleted theorem equiv.mul_left'_symm_apply

deleted theorem equiv.mul_right'_symm_apply

deleted theorem monoid_hom.coe_to_mul_equiv

deleted theorem units.coe_mul_left

deleted theorem units.coe_mul_right

Modified src/group_theory/free_abelian_group.lean

Modified src/group_theory/subgroup.lean