ringKrullDim_mvPolynomial_of_isEmpty

English

If σ is empty, the multivariate polynomial ring MvPolynomial σ R is isomorphic to R, hence their Krull dimensions coincide: ringKrullDim(MvPolynomial ∅ R) = ringKrullDim(R).

Русский

Если множество σ пустое, кольцо многочленов MvPolynomial σ R изоморфно R, следовательно размерности совпадают: ringKrullDim(MvPolynomial ∅ R) = ringKrullDim(R).

LaTeX

$$$\\operatorname{ringKrullDim}(\\operatorname{MvPolynomial}\\emptyset R) = \\operatorname{ringKrullDim}(R)$$$

Lean4

@[simp]
theorem ringKrullDim_mvPolynomial_of_isEmpty (σ : Type*) [IsEmpty σ] :
    ringKrullDim (MvPolynomial σ R) = ringKrullDim R :=
  ringKrullDim_eq_of_ringEquiv (isEmptyRingEquiv _ _)

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