Commit 2025-08-13 15:26 f6852835

View on Github →

feat(GroupTheory/FreeGroup): add predicate for reduced words (#25966) This PR adds the predicate of reduced words IsReduced in the construction of free groups. It is shown that reduce and toWord produce reduced words. This is done in preparation for the theory of cyclically reduced words. Upstreamed from the EquationalTheories project.

Estimated changes

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

added theorem FreeGroup.IsReduced.append_overlap

added theorem FreeGroup.IsReduced.infix

added theorem FreeGroup.IsReduced.nil

added theorem FreeGroup.IsReduced.not_step

added theorem FreeGroup.IsReduced.of_forall_not_step

added theorem FreeGroup.IsReduced.red_iff_eq

added theorem FreeGroup.IsReduced.singleton

added def FreeGroup.IsReduced

added theorem FreeGroup.isReduced_cons_cons

added theorem FreeGroup.isReduced_iff_not_step

Modified Mathlib/GroupTheory/FreeGroup/Reduce.lean

added theorem FreeGroup.IsReduced.of_reduce_eq

added theorem FreeGroup.IsReduced.reduce_eq

added theorem FreeGroup.isReduced_iff_reduce_eq

added theorem FreeGroup.isReduced_toWord