Commit 2025-11-04 07:54 9a7cdf50

View on Github →

feat(GroupTheory/FreeGroup): reduction theorem for powers (#27678) This PR adds the theorem reduce_flatten_replicate, it describes the reduction of a power of a reduced word in terms of its cyclic reduction. It is a part of a series of PR on the theory of cyclically reduced words. Upstreamed from the EquationalTheories project.

depends on: #25966
depends on: #27672
depends on: #27673

Estimated changes

Modified Mathlib/GroupTheory/FreeGroup/CyclicallyReduced.lean

modified theorem FreeGroup.IsCyclicallyReduced.flatten_replicate

added theorem FreeGroup.IsReduced.append_flatten_replicate_append

modified theorem FreeGroup.reduceCyclically.conj_conjugator_reduceCyclically

modified theorem FreeGroup.reduceCyclically.isCyclicallyReduced

added theorem FreeGroup.reduceCyclically.reduce_flatten_replicate

added theorem FreeGroup.reduceCyclically.reduce_flatten_replicate_succ