Theorem FreeCommRing.of_ne_zero

Modification history

2026-09-03 15:14

Mathlib/RingTheory/FreeCommRing.lean

chore(FreeRing): use `MonoidAlgebra ℤ` instead of `FreeAbelianGroup` (#42245) …

Modified FreeCommRing.of_ne_zero View on Github →

2024-10-29 10:07

Mathlib/RingTheory/FreeCommRing.lean

feat: trivial nontrivialities for free (constructions) (#18363) …

Added FreeCommRing.of_ne_zero View on Github →