Theorem FreeGroup.eq_of_commute_of_of

Modification history

2026-10-17 11:31
Mathlib/GroupTheory/FreeGroup/Reduce.lean
feat(FreeGroup): characterize commutative/cyclic free groups (#41988) …
Added FreeGroup.eq_of_commute_of_ofView on Github →