Theorem FreeGroup.IsReduced.of_forall_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.of_forall_not_stepView on Github →