isScalarTower — Mathlib

English

If S1 acts on S2 and S2 acts on R in a scalar-tower way, then S1 acts on the polynomial ring R[X] compatibly with the tower structure.

Русский

Если S1 действует на S2 и S2 действует на R так, что образуется тензорный тандем, то S1 действует на R[X] совместно с тензорной структурой.

LaTeX

$$$\forall {R} [\mathrm{Semiring} R] {S_1 S_2} [\mathrm{SMul} S_1 S_2] [\mathrm{IsScalarTower} S_1 S_2 R] \Rightarrow \mathrm{IsScalarTower} S_1 S_2 (\mathrm{Polynomial} R)$$$

Lean4

instance isScalarTower {S₁ S₂} [SMul S₁ S₂] [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [IsScalarTower S₁ S₂ R] :
    IsScalarTower S₁ S₂ R[X] :=
  ⟨by
    rintro _ _ ⟨⟩
    simp_rw [← ofFinsupp_smul, smul_assoc]⟩

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