Theorem FreeGroup.one_ne_of

Modification history

2024-11-27 09:56
Mathlib/GroupTheory/FreeGroup/Basic.lean
chore(GroupTheory/FreeGroup): split off `Reduce.lean` (#19501)
Modified FreeGroup.one_ne_ofView on Github →
2024-10-29 10:07
Mathlib/GroupTheory/FreeGroup/Basic.lean
feat: trivial nontrivialities for free (constructions) (#18363) …
Added FreeGroup.one_ne_ofView on Github →