Theorem FreeCommRing.of_ne_one

Modification history

2024-10-29 10:07
Mathlib/RingTheory/FreeCommRing.lean
feat: trivial nontrivialities for free (constructions) (#18363) …
Added FreeCommRing.of_ne_oneView on Github →