instIsScalarTowerPolynomial — Mathlib

English

There is a scalar tower IsScalarTower R R[X] A[X], i.e., the natural compatibility of scalar actions holds in the polynomial setting.

Русский

Существует пространственный тензорный торовой порядок IsScalarTower R R[X] A[X], то есть совместимость скалярных действий в полиномном случае.

LaTeX

$$$\text{IsScalarTower } R\; R[X]\; A[X].$$$

Lean4

instance : IsScalarTower R R[X] A[X] :=
  .of_algebraMap_eq' (mapRingHom_comp_C _).symm

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