instIsScalarTower — Mathlib

English

The tower of scalar actions passes to AdjoinRoot f: if R₁, R₂ act on R with appropriate towers, then AdjoinRoot f inherits a compatible IsScalarTower structure.

Русский

Использование башни скаляров сохраняется: AdjoinRoot f наследует совместимую структуру IsScalarTower.

LaTeX

$$$IsScalarTower R_1 R_2 (AdjoinRoot f)$$$

Lean4

instance (R₁ R₂ : Type*) [SMul R₁ R₂] [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R]
    [IsScalarTower R₂ R R] [IsScalarTower R₁ R₂ R] (f : R[X]) : IsScalarTower R₁ R₂ (AdjoinRoot f) :=
  Submodule.Quotient.isScalarTower _ _

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