Theorem FreeMonoid.one_ne_of

Modification history

2024-10-29 10:07
Mathlib/Algebra/FreeMonoid/Basic.lean
feat: trivial nontrivialities for free (constructions) (#18363) …
Added FreeMonoid.one_ne_ofView on Github →