isScalarTower — Mathlib

English

If scalar towers hold for M→N to α and to β, then the product α×β inherits a scalar tower from M and N.

Русский

Если тензор скаляров работает по координатам, то произведение действует по тем же правилам.

LaTeX

$$$IsScalarTower\\ M\\ N (α × β)$$$

Lean4

@[to_additive]
instance isScalarTower [SMul M N] [IsScalarTower M N α] [IsScalarTower M N β] : IsScalarTower M N (α × β) where
  smul_assoc _ _ _ := by ext <;> exact smul_assoc ..

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