height_le_spanFinrank — Mathlib

English

In a Noetherian ring, the height of a (proper) ideal is bounded by its spanFinrank.

Русский

В Noetherian кольце высота (предел) идеала ограничена его spanFinrank.

LaTeX

$$$I.height \le I.spanFinrank$$$

Lean4

theorem height_le_spanFinrank (I : Ideal R) (hI : I ≠ ⊤) : I.height ≤ I.spanFinrank :=
  by
  have : I.spanFinrank = I.spanRank.toENat := by
    rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I), map_natCast]
  exact this ▸ height_le_spanRank_toENat I hI

Похожие утверждения