isScalarTower — Mathlib

English

If M acts on N and each α i has SMul by N, and IsScalarTower M N (α i) for each i, then IsScalarTower M N (∀ i, α i).

Русский

Если M действует на N, и для каждого i множество α i имеет SMul N и IsScalarTower M N (α i), то IsScalarTower M N (∀ i, α i).

LaTeX

$$$[SMul M N] [\forall i, SMul N (α i)] [\forall i, SMul M (α i)] [\forall i, IsScalarTower M N (α i)] \Rightarrow IsScalarTower M N (\forall i, α i)$$$

Lean4

@[to_additive]
instance isScalarTower [SMul M N] [∀ i, SMul N (α i)] [∀ i, SMul M (α i)] [∀ i, IsScalarTower M N (α i)] :
    IsScalarTower M N (∀ i, α i) where smul_assoc x y z := funext fun i ↦ smul_assoc x y (z i)

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