Commit 2020-05-06 19:39 c3d76d01

View on Github →

chore(*): a few missing simp lemmas (#2615) Also replaces monoid_hom.exists_inv_of_comp_exists_inv with monoid_hom.map_exists_right_inv and adds monoid_hom.map_exists_left_inv.

Estimated changes

Modified src/algebra/group/hom.lean

deleted theorem monoid_hom.exists_inv_of_comp_exists_inv

added theorem monoid_hom.id_apply

added theorem monoid_hom.map_exists_left_inv

added theorem monoid_hom.map_exists_right_inv

added theorem monoid_hom.map_mul_eq_one

Modified src/data/equiv/mul_add.lean

added theorem mul_equiv.coe_mk

added theorem mul_equiv.coe_symm_mk

Modified src/data/sigma/basic.lean

added theorem sigma.eta