instIsScalarTower — Mathlib

English

There is a natural IsScalarTower structure on R, MvPolynomial(σ,R), MvPolynomial(σ,S) coming from the algebra-map-based construction.

Русский

Существует естественная структура IsScalarTower на R, MvPolynomial(σ,R), MvPolynomial(σ,S), получаемая через алгебраическое отображение.

LaTeX

$$$$\text{instance } IsScalarTower\, R\ (MvPolynomial(\sigma,R))\ (MvPolynomial(\sigma,S)).$$$$

Lean4

instance : IsScalarTower R (MvPolynomial σ R) (MvPolynomial σ S) :=
  IsScalarTower.of_algebraMap_eq' (by ext; simp)

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