Commit 2026-08-27 00:26 412da928
View on Github →feat(LocalRing): instance Finite (R / maximalIdeal R ^ n) (#42994)
For a noetherian local ring, we prove an instance Finite (R ⧸ maximalIdeal R ^ n) if the residue field of R is finite.
feat(LocalRing): instance Finite (R / maximalIdeal R ^ n) (#42994)
For a noetherian local ring, we prove an instance Finite (R ⧸ maximalIdeal R ^ n) if the residue field of R is finite.