instIsScalarTower — Mathlib

English

There is an IsScalarTower structure for S, T and LinearMap σ₁₂ M M₂, providing associativity of scalar actions on linear maps.

Русский

Существует структура IsScalarTower для S, T и LinearMap σ₁₂ M M₂, обеспечивающая ассоциативность скалярных действий на линейных отображениях.

LaTeX

$$$IsScalarTower\ S\ T\ (\mathrm{LinearMap}\ σ_{12}\ M\ M_2)$$$

Lean4

instance [SMul S T] [IsScalarTower S T M₂] : IsScalarTower S T (M →ₛₗ[σ₁₂] M₂) where
  smul_assoc _ _ _ := ext fun _ ↦ smul_assoc _ _ _

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