Noetherian

📁 Source: Mathlib/RingTheory/Ideal/MinimalPrime/Noetherian.lean

Statistics

Metric	Count
Definitions	0
Theorems finite_minimalPrimes_of_isNoetherianRing, finite_of_isNoetherianRing	2
Total	2

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_minimalPrimes_of_isNoetherianRing 📖	mathematical	—	Set.Finite Ideal CommSemiring.toSemiring minimalPrimes	—	set_has_maximal_iff_noetherian Mathlib.Tactic.Contrapose.contrapose₄ minimalPrimes_eq_subsingleton_self minimalPrimes_top not_isPrime_iff Set.Finite.subset Set.Finite.union left_lt_sup span_singleton_le_iff_mem IsPrime.mem_or_mem' sup_le LE.le.trans LT.lt.le

minimalPrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_of_isNoetherianRing 📖	mathematical	—	Set.Finite Ideal CommSemiring.toSemiring minimalPrimes	—	Ideal.finite_minimalPrimes_of_isNoetherianRing

---

← Back to Index