isEmptyAlgEquiv — Mathlib

English

There is a natural algebra isomorphism between the polynomial algebra in no variables over R and R itself, provided σ is empty.

Русский

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

LaTeX

$$$\text{isEmptyAlgEquiv} \;R\;\sigma : MvPolynomial\,\sigma\,R \cong_{R} R$ (при IsEmpty\,\sigma)$$

Lean4

/-- The algebra isomorphism between multivariable polynomials in no variables
and the ground ring. -/
@[simps! apply]
def isEmptyAlgEquiv : MvPolynomial σ R ≃ₐ[R] R :=
  .ofAlgHom (aeval isEmptyElim) (Algebra.ofId _ _) (by ext) (by ext i m; exact isEmptyElim i)

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