Def minimalPrimes

Modification history

2025-02-05 10:58
Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
feat(RingTheory): `Ring.KrullDimLE` type class (#21452) …
Modified minimalPrimesView on Github →
2024-02-08 13:29
Mathlib/RingTheory/Ideal/MinimalPrime.lean
chore: tidy various files (#10311)
Modified minimalPrimesView on Github →
2024-01-18 10:31
Mathlib/RingTheory/Ideal/MinimalPrime.lean
feat: Lemma on Monoid Localization and Consequences on Minimal Primes (#9640)
Modified minimalPrimesView on Github →
2023-08-10 19:52
Mathlib/RingTheory/Ideal/MinimalPrime.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified minimalPrimesView on Github →
2023-05-21 15:37
Mathlib/RingTheory/Ideal/MinimalPrime.lean
feat: port RingTheory.Ideal.MinimalPrime (#4146) …
Added minimalPrimesView on Github →