Commit 2025-09-30 17:24 0c04c3ec

View on Github →

feat(GroupTheory/FreeGroup): add definition of cyclically reduced words (#27672) This PR adds the definition of cyclically reduced words for free groups. It is a part of a series of PR on the theory of cyclically reduced words. Upstreamed from the EquationalTheories project.

depends on: #25966

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/FreeGroup/CyclicallyReduced.lean

added theorem FreeGroup.IsCyclicallyReduced.flatten_replicate

added theorem FreeGroup.IsCyclicallyReduced.isReduced

added theorem FreeGroup.IsCyclicallyReduced.nil

added theorem FreeGroup.IsCyclicallyReduced.singleton

added def FreeGroup.IsCyclicallyReduced

added theorem FreeGroup.isCyclicallyReduced_cons_append_iff

added theorem FreeGroup.isCyclicallyReduced_iff