supportDim_le_ringKrullDim — Mathlib

English

Alternative construction: if for all primes I, I ≠ ⊥ → I.IsPrime → I.IsMaximal, then Ring.KrullDimLE 1 R.

Русский

Альтернативное построение: если для каждого простого идеала I, I ≠ ⊥ → I.IsPrime → I.IsMaximal, тогда Ring.KrullDimLE 1 R.

LaTeX

$$$(\forall I:\mathrm{Ideal}(R), I \neq \perp \rightarrow I.IsPrime \rightarrow I.IsMaximal) \Rightarrow \mathrm{Ring.KrullDimLE }1\;R$$$

Lean4

theorem supportDim_le_ringKrullDim : supportDim R M ≤ ringKrullDim R :=
  krullDim_le_of_strictMono (fun a ↦ a) fun {_ _} lt ↦ lt

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