Theorem IsArtinianRing.mem_minimalPrimes

Modification history

2026-03-26 08:33
Mathlib/RingTheory/Artinian/Module.lean
feat(RingTheory/Unramified/Dedekind): a domain finite and unramified over a Dedekind domain is a Dedekind domain (#36838) …
Added IsArtinianRing.mem_minimalPrimesView on Github →