algebraMvPolynomial — Mathlib

English

The aevalTower with the identity algebra homomorphism equals the standard aeval map.

Русский

Стек aevalTower с тождественным отображением совпадает с обычным aeval.

LaTeX

$$$$ \operatorname{aevalTower}(\mathrm{AlgHom}.id \; S S) = (\operatorname{aeval} : (σ \to S) \rightarrow MvPolynomial(σ,S) \rightarrow_{S} S). $$$$

Lean4

/-- If `S` is an `R`-algebra, then `MvPolynomial σ S` is a `MvPolynomial σ R` algebra.

Warning: This produces a diamond for
`Algebra (MvPolynomial σ R) (MvPolynomial σ (MvPolynomial σ S))`. That's why it is not a
global instance.
-/
noncomputable def algebraMvPolynomial : Algebra (MvPolynomial σ R) (MvPolynomial σ S) :=
  (MvPolynomial.map (algebraMap R S)).toAlgebra

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