instIsScalarTower — Mathlib

English

If SMul structures exist with a scalar tower, then the induced tower on SimpleFunc preserves associativity: (k • (γ • f)) = (k • γ) • f.

Русский

Если существуют структуры умножения на скаляры с тензорной связью, то соответствующая связка на SimpleFunc сохраняет ассоциативность: (k • (γ • f)) = (k • γ) • f.

LaTeX

$$$\\text{instIsScalarTower }[SMul K \\gamma][SMul \\gamma \\beta][SMul K \\beta][IsScalarTower K \\gamma \\beta] : IsScalarTower K \\gamma (\\alpha \\to_{S} \\beta).$$$

Lean4

instance [SMul K γ] [SMul γ β] [SMul K β] [IsScalarTower K γ β] : IsScalarTower K γ (α →ₛ β) where
  smul_assoc _ _ _ := ext fun _ ↦ smul_assoc ..

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