instIsScalarTower — Mathlib

English

If SMul M α and SMul N α and IsScalarTower M N α hold, and similarly for β, then Sum α β also has IsScalarTower M N (Sum α β).

Русский

Если существуют SMul M α, SMul N α и IsScalarTower M N α, как и на β, то Sum α β также имеет IsScalarTower M N (Sum α β).

LaTeX

$$$[SMul M α][SMul N α][IsScalarTower M N α][SMul M β][SMul N β][IsScalarTower M N β] \Rightarrow IsScalarTower M N (\Sigma α β).$$$

Lean4

instance [SMul M N] [IsScalarTower M N α] [IsScalarTower M N β] : IsScalarTower M N (α ⊕ β) :=
  ⟨fun a b x => by
    cases x
    exacts [congr_arg inl (smul_assoc _ _ _), congr_arg inr (smul_assoc _ _ _)]⟩

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