Theorem IsLocalRing.ringJacobson_eq_maximalIdeal

Modification history

2025-11-10 13:35
Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean
feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence (#26219) …
Added IsLocalRing.ringJacobson_eq_maximalIdealView on Github →