instSMulAdjoinRoot — Mathlib

English

If S acts on R in a compatible way, then AdjoinRoot f inherits a scalar action by S, turning it into an S-module via the induced quotient structure.

Русский

Если S действует на R совместимо, то AdjoinRoot f наследует скалярное действие от S, превращая его в S-модуль через индуцированную факторную структуру.

LaTeX

$$$AdjoinRoot(f) \\text{ carries an } S\\text{-module structure}$$$

Lean4

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

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