instSMulCommClass — Mathlib

English

Given separate scalar actions by R₁ and R₂, the induced action on AdjoinRoot f commutes: SMulCommClass R₁ R₂ (AdjoinRoot f).

Русский

При отдельном действии скаляров R₁ и R₂ действия на AdjoinRoot f коммутизируются.

LaTeX

$$$SMulCommClass R_1 R_2 (AdjoinRoot f)$$$

Lean4

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

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