Theorem FreeGroup.isReduced_iff_not_step

Modification history

2025-08-13 15:26

Mathlib/GroupTheory/FreeGroup/Basic.lean

feat(GroupTheory/FreeGroup): add predicate for reduced words (#25966) …

Added FreeGroup.isReduced_iff_not_step View on Github →