Theorem FreeCommRing.isSupported_int

Modification history

2026-09-03 15:14

Mathlib/RingTheory/FreeCommRing.lean

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

Modified FreeCommRing.isSupported_int View on Github →

2023-05-17 06:12

Mathlib/RingTheory/FreeCommRing.lean

feat: port RingTheory.FreeCommRing (#3994) …

Added FreeCommRing.isSupported_int View on Github →