Theorem FreeGroup.isMulCommutative_iff_subsingleton

Modification history

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