ringKrullDim_quotient_le — Mathlib

English

For any ideal I ⊆ R, ringKrullDim(R/I) ≤ ringKrullDim R.

Русский

Для любого идеала I ⊆ R выполняется ringKrullDim(R/I) ≤ ringKrullDim R.

LaTeX

$$$ringKrullDim(R/I) \\le ringKrullDim R$$$

Lean4

/-- If `I` is an ideal of `R`, then `ringKrullDim (R ⧸ I) ≤ ringKrullDim R`. -/
theorem ringKrullDim_quotient_le {R : Type*} [CommRing R] (I : Ideal R) : ringKrullDim (R ⧸ I) ≤ ringKrullDim R :=
  ringKrullDim_le_of_surjective _ Ideal.Quotient.mk_surjective

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