Theorem Ideal.ringJacobson_le_jacobson

Modification history

2025-11-10 13:35
Mathlib/RingTheory/Jacobson/Ideal.lean
feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence (#26219) …
Added Ideal.ringJacobson_le_jacobsonView on Github →