English
If for all i, SMul (α i) (β i) and SMul (β i) (γ i) and SMul (α i) (γ i) and IsScalarTower (α i) (β i) (γ i) hold, then IsScalarTower ((i → α i)) ((i → β i)) ((i → γ i)).
Русский
Если для всех i выполняются смулы (α_i)→(β_i), (β_i)→(γ_i) и (α_i)→(γ_i) и IsScalarTower для каждого i, тогда IsScalarTower для функций: (i→α_i) там (i→β_i) и (i→γ_i).
LaTeX
$$$\forall i, IsScalarTower (α i) (β i) (γ i) \Rightarrow IsScalarTower ((i) → α i) ((i) → β i) ((i) → γ i)$$$
Lean4
@[to_additive]
instance isScalarTower'' [∀ i, SMul (α i) (β i)] [∀ i, SMul (β i) (γ i)] [∀ i, SMul (α i) (γ i)]
[∀ i, IsScalarTower (α i) (β i) (γ i)] : IsScalarTower (∀ i, α i) (∀ i, β i) (∀ i, γ i) where
smul_assoc x y z := funext fun i ↦ smul_assoc (x i) (y i) (z i)
