instIsScalarTower — Mathlib

English

If S acts on M and T on M with an IsScalarTower structure, then LieDerivation R L M inherits an IsScalarTower structure with S and T: IsScalarTower S T (LieDerivation R L M).

Русский

Если S действует на M и T действует на M с структурой IsScalarTower, то LieDerivation R L M наследует структуру IsScalarTower: IsScalarTower S T (LieDerivation R L M).

LaTeX

$$$\text{IsScalarTower } S T (\text{LieDerivation } R L M)$$$

Lean4

instance [SMul S T] [IsScalarTower S T M] : IsScalarTower S T (LieDerivation R L M) :=
  ⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩

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