Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-26 05:21 121c9a49

View on Github →

chore(algebra/group/hom): use coe_comp in simp lemmas (#4780) This way Lean will simplify ⇑(f.comp g) even if it is not applied to an element.

Estimated changes

added theorem monoid_hom.coe_comp
modified theorem monoid_hom.comp_apply
added theorem mul_hom.coe_comp
modified theorem mul_hom.comp_apply
added theorem one_hom.coe_comp
modified theorem one_hom.comp_apply