Theorem Ideal.minimalPrimes_eq_subsingleton_self

Modification history

2025-02-05 10:58
Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
feat(RingTheory): `Ring.KrullDimLE` type class (#21452) …
Modified Ideal.minimalPrimes_eq_subsingleton_selfView on Github →
2023-05-21 15:37
Mathlib/RingTheory/Ideal/MinimalPrime.lean
feat: port RingTheory.Ideal.MinimalPrime (#4146) …
Added Ideal.minimalPrimes_eq_subsingleton_selfView on Github →