English
Krull's principal theorem in ENat form: the height of a prime p is bounded by n iff there exists an ideal I with p ∈ minimalPrimes(I) and spanRank(I) ≤ n.
Русский
Теорема о крилле в форме ENat: высота p ограничена n тогда и только тогда, когда существует идеал I с p ∈ minimalPrimes(I) и spanRank(I) ≤ n.
LaTeX
$$$p.height \le n \iff \exists I: \mathrm{Ideal}(R), p \in I.minimalPrimes \land I.spanRank \le n$$$
Lean4
/-- In a commutative Noetherian ring `R`, the height of a (finitely-generated) ideal is smaller
than or equal to the minimum number of generators for this ideal. -/
theorem height_le_spanRank_toENat (I : Ideal R) (hI : I ≠ ⊤) : I.height ≤ I.spanRank.toENat :=
by
obtain ⟨J, hJ⟩ := nonempty_minimalPrimes hI
refine (iInf₂_le J hJ).trans ?_
convert (I.height_le_spanRank_toENat_of_mem_minimal_primes J hJ)
exact Eq.symm (@height_eq_primeHeight _ _ J hJ.1.1)
