Commit 2024-10-17 07:12 4f4f4ec6

View on Github →

feat(Algebra/FreeMonoid/Basic): define length, symbols, membership, reversing, induction principles (#17180) add these properties for future use in the braid monoid (I have avoided duplicating the List API when possible, ex: using FreeMonoid.lift. These are the remaining properties I need to add)

Estimated changes

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

added def FreeMonoid.length

added theorem FreeMonoid.length_eq_one

added theorem FreeMonoid.length_eq_two

added theorem FreeMonoid.length_eq_zero

added theorem FreeMonoid.length_mul

added theorem FreeMonoid.length_of

added theorem FreeMonoid.length_one

added theorem FreeMonoid.length_reverse

added theorem FreeMonoid.map_map

added theorem FreeMonoid.map_surjective

added def FreeMonoid.mem

added theorem FreeMonoid.mem_map

added theorem FreeMonoid.mem_mul

added theorem FreeMonoid.mem_of

added theorem FreeMonoid.mem_of_self

added theorem FreeMonoid.not_mem_one

added theorem FreeMonoid.of_ne_one

added def FreeMonoid.reverse

added theorem FreeMonoid.reverse_mul

added theorem FreeMonoid.reverse_of

added theorem FreeMonoid.reverse_reverse

Modified Mathlib/Algebra/Group/Submonoid/Membership.lean

Modified Mathlib/Control/Fold.lean

Modified Mathlib/GroupTheory/Coprod/Basic.lean