Theorem minimalPrimes_eq_minimals

Modification history

2025-02-05 10:58
Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
feat(RingTheory): `Ring.KrullDimLE` type class (#21452) …
Modified minimalPrimes_eq_minimalsView on Github →
2024-08-05 16:52
Mathlib/RingTheory/Ideal/MinimalPrime.lean
refactor(Order/Minimal): change minimality to a predicate (#14721) …
Modified minimalPrimes_eq_minimalsView on Github →
2024-02-08 13:29
Mathlib/RingTheory/Ideal/MinimalPrime.lean
chore: tidy various files (#10311)
Modified minimalPrimes_eq_minimalsView on Github →
2024-01-18 10:31
Mathlib/RingTheory/Ideal/MinimalPrime.lean
feat: Lemma on Monoid Localization and Consequences on Minimal Primes (#9640)
Modified minimalPrimes_eq_minimalsView on Github →
2024-01-01 07:00
Mathlib/RingTheory/Ideal/MinimalPrime.lean
feat(AlgebraicGeometry/PrimeSpectrum/*) : the collection of minimal prime ideals of a Noetherian ring is finite (#9088) …
Added minimalPrimes_eq_minimalsView on Github →