Theorem FreeRing.of_ne_one

Modification history

2026-09-03 15:14
Mathlib/RingTheory/FreeRing.lean
chore(FreeRing): use `MonoidAlgebra ℤ` instead of `FreeAbelianGroup` (#42245) …
Modified FreeRing.of_ne_oneView on Github →
2024-10-29 10:07
Mathlib/RingTheory/FreeRing.lean
feat: trivial nontrivialities for free (constructions) (#18363) …
Added FreeRing.of_ne_oneView on Github →