Commit 2026-09-03 15:14 991f3036

View on Github →

chore(FreeRing): use MonoidAlgebra ℤ instead of FreeAbelianGroup (#42245) Replace FreeAbelianGroup with MonoidAlgebra ℤ in the definition of FreeRing and FreeCommRing. The intent is to deprecate and remove the multiplication on FreeAbelianGroup so it can be @[to_additive]-ized.

Estimated changes

deleted theorem FreeCommRing.of_cons
modified theorem FreeCommRing.of_ne_zero
modified theorem FreeCommRing.zero_ne_of
deleted theorem FreeRing.coe_eq
modified theorem FreeRing.of_ne_one
modified theorem FreeRing.of_ne_zero
modified theorem FreeRing.one_ne_of
modified theorem FreeRing.zero_ne_of