English
If for each i, SMul M (α i), SMul (α i) (β i), SMul M (β i) and IsScalarTower M (α i) (β i) hold, then IsScalarTower M ((i → α i)) ((i → β i)).
Русский
Для каждого i есть SMul M (α_i), SMul (α_i) (β_i), SMul M (β_i) и IsScalarTower M (α_i) (β_i); тогда IsScalarTower M ((i → α_i)) ((i → β_i)).
LaTeX
$$$[\forall i, SMul M (α i)] [\forall i, SMul (α i) (β i)] [\forall i, SMul M (β i)] [\forall i, IsScalarTower M (α i) (β i)] \Rightarrow IsScalarTower M ((i) → α i) ((i) → β i)$$$
Lean4
@[to_additive]
instance isScalarTower' [∀ i, SMul M (α i)] [∀ i, SMul (α i) (β i)] [∀ i, SMul M (β i)]
[∀ i, IsScalarTower M (α i) (β i)] : IsScalarTower M (∀ i, α i) (∀ i, β i) where
smul_assoc x y z := funext fun i ↦ smul_assoc x (y i) (z i)
