English
If α, β, γ are related by SMul actions and IsScalarTower α β γ, then the induced Actions satisfy IsScalarTower (Filter α) (Filter β) (Filter γ); i.e., (X • Y) • Z = X • (Y • Z) for X ∈ Filter α, Y ∈ Filter β, Z ∈ Filter γ.
Русский
Пусть выполняются SMul-сложения между α, β, γ и IsScalarTower α β γ. Тогда индуцированные действия дают IsScalarTower (Filter α) (Filter β) (Filter γ); то есть (X • Y) • Z = X • (Y • Z) для всех X ∈ Filter α, Y ∈ Filter β, Z ∈ Filter γ.
LaTeX
$$$\\forall X \\in \\mathrm{Filter}(\\alpha),\\; Y \\in \\mathrm{Filter}(\\beta),\\; Z \\in \\mathrm{Filter}(\\gamma): (X \\cdot Y) \\cdot Z = X \\cdot (Y \\cdot Z).$$$
Lean4
@[to_additive]
instance isScalarTower'' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
IsScalarTower (Filter α) (Filter β) (Filter γ) :=
⟨fun _ _ _ => map₂_assoc smul_assoc⟩
