Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-26 13:30 099ffd38

View on Github →

chore(algebra/free_monoid): use implicit args in lift (#2821)

Estimated changes

Modified src/algebra/free_monoid.lean

modified theorem free_monoid.comp_lift

added theorem free_monoid.hom_map_lift

modified theorem free_monoid.lift_apply

modified theorem free_monoid.lift_comp_of

modified theorem free_monoid.lift_eval_of

modified theorem free_monoid.lift_restrict

added theorem free_monoid.lift_symm_apply

Modified src/algebra/group/hom.lean

added theorem monoid_hom.coe_mk'

Modified src/group_theory/submonoid.lean

modified theorem submonoid.closure_eq_mrange