Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-14 04:40 6ffb6137

View on Github →

chore(algebra/free_monoid): add a custom rec_on (#2670)

Estimated changes

Modified src/algebra/free_monoid.lean

modified theorem free_monoid.mul_def

added theorem free_monoid.of_def

deleted theorem free_monoid.of_mul_eq_cons

modified theorem free_monoid.one_def

added def free_monoid.rec_on

Modified src/group_theory/submonoid.lean