Commit 2024-10-29 10:07 6c2c697b

View on Github →

feat: trivial nontrivialities for free (constructions) (#18363) This adds some Unique and Nontrivial instances for free constructions, and some simp lemmas of the form of x ≠ 0.

Estimated changes

added theorem FreeMonoid.one_ne_of
added theorem FreeGroup.norm_of
added theorem FreeGroup.of_ne_one
added theorem FreeGroup.one_ne_of
added theorem FreeGroup.toWord_of
added theorem FreeCommRing.of_ne_one
added theorem FreeCommRing.one_ne_of
added theorem FreeRing.of_ne_one
added theorem FreeRing.of_ne_zero
added theorem FreeRing.one_ne_of
added theorem FreeRing.zero_ne_of