ringKrullDim_succ_le_ringKrullDim_polynomial

English

The Krull dimension grows when passing to polynomial rings in one indeterminate: ringKrullDim(R) + 1 ≤ ringKrullDim(R[X]).

Русский

Размерность Крулля растёт при переходе к кольцу многочленов в одной переменной: ringKrullDim(R) + 1 ≤ ringKrullDim(R[X]).

LaTeX

$$$\\operatorname{ringKrullDim}(R) + 1 \\le \\operatorname{ringKrullDim}(R[X])$$$

Lean4

theorem ringKrullDim_succ_le_ringKrullDim_polynomial : ringKrullDim R + 1 ≤ ringKrullDim R[X] :=
  ringKrullDim_succ_le_of_surjective constantCoeff (⟨C ·, coeff_C_zero⟩) X_mem_nonzeroDivisors coeff_X_zero

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