smulCommClass — Mathlib

English

The lifted IsScalarTower structure on the space of continuous linear maps holds, i.e., the tower law persists for S2, T2 acting on M2 via the mapping f.

Русский

Поднятая структура IsScalarTower действует на пространстве непрерывных линейных отображений, т.е. тождество башни сохраняется для действий S2 и T2 на M2 через отображение f.

LaTeX

$$$ IsScalarTower S_2 T_2 (\mathrm{ContinuousLinearMap} \; \sigma_{12} \; M_1 \; M_2). $$$

Lean4

instance smulCommClass [SMulCommClass S₂ T₂ M₂] : SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂) :=
  ⟨fun a b f => ext fun x => smul_comm a b (f x)⟩

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