instDistribSMulOfIsScalarTower — Mathlib

English

Under a scalar action of S on R, AdjoinRoot f naturally inherits a DistribSMul structure, compatible with the quotient construction.

Русский

При действии S на R AdjoinRoot f естественно получает распределённое скалярное умножение, совместимое с факторной конструкцией.

LaTeX

$$$AdjoinRoot f\\;\\text{ has a DistribSMul by } S$$$

Lean4

instance [DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f) :=
  Submodule.Quotient.distribSMul' _

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