algebraMap_def — Mathlib

English

If S is an R-algebra, then MvPolynomial(σ,S) has the natural structure of an MvPolynomial(σ,R)-algebra through the map induced by the base algebra map.

Русский

Если S является R-алгеброй, то MvPolynomial(σ,S) имеет естественную структуру Algebra(MvPolynomial(σ,R), MvPolynomial(σ,S)) через отображение, порожденное базовым отображением алгебры.

LaTeX

$$$$ \text{MvPolynomial}(\sigma, S) \text{ becomes an } \text{MvPolynomial}(\sigma,R)\text{-algebra via } map(\mathrm{algebraMap}(R,S)). $$$$

Lean4

@[simp]
theorem algebraMap_def : algebraMap (MvPolynomial σ R) (MvPolynomial σ S) = MvPolynomial.map (algebraMap R S) :=
  rfl

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