isScalarTower — Mathlib

English

There is an IsScalarTower structure: S2 acts on M2, T2 acts on M2, and the two actions compose to act on the space of continuous linear maps M1 →SL[σ12] M2.

Русский

Существует структура IsScalarTower: S2 действует на M2, T2 действует на M2, и две действия объединяются, образуя действие на пространство непрерывных линейных отображений M1 →SL[σ12] M2.

LaTeX

$$$ IsScalarTower S_2 T_2 (C\!L[\sigma_{12}] M_1 M_2). $$$

Lean4

instance isScalarTower [SMul S₂ T₂] [IsScalarTower S₂ T₂ M₂] : IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂) :=
  ⟨fun a b f => ext fun x => smul_assoc a b (f x)⟩

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