ringKrullDim_succ_le_ringKrullDim_powerseries

English

The Krull dimension increases by at least one when passing from R to PowerSeries R: ringKrullDim(R) + 1 ≤ ringKrullDim(PowerSeries R).

Русский

Размерность Крулля возрастает как минимум на единицу, переходя от R к кольцу степенных серий PowerSeries R: ringKrullDim(R) + 1 ≤ ringKrullDim(PowerSeries R).

LaTeX

$$$\\operatorname{ringKrullDim}(R) + 1 \\le \\operatorname{ringKrullDim}(\\operatorname{PowerSeries}(R))$$$

Lean4

theorem ringKrullDim_succ_le_ringKrullDim_powerseries : ringKrullDim R + 1 ≤ ringKrullDim (PowerSeries R) :=
  ringKrullDim_succ_le_of_surjective constantCoeff (⟨C ·, rfl⟩) MvPowerSeries.X_mem_nonzeroDivisors constantCoeff_X

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