isEmptyRingEquiv — Mathlib

English

There is a canonical ring isomorphism between the multivariable polynomial ring with no variables and the base ring when the index type is empty.

Русский

Существует каноническое изоморфизм кольца между полиномиальной алгеброй в ноль переменных и базовым кольцом, если множество индексов пустое.

LaTeX

$$$MvPolynomial\;\isEmptyRingEquiv\;R\;σ \cong+* R\quad\text{for } IsEmpty\; σ$$$

Lean4

/-- The ring isomorphism between multivariable polynomials in no variables
and the ground ring. -/
@[simps! apply]
def isEmptyRingEquiv : MvPolynomial σ R ≃+* R :=
  (isEmptyAlgEquiv R σ).toRingEquiv

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