English
Let α act on β and γ via SMul with IsScalarTower α β γ. The induced actions give a scalar tower between α, Filter β, and Filter γ; i.e., for all a ∈ α, F ∈ Filter β and G ∈ Filter γ, (a • F) • G = a • (F • G).
Русский
Пусть α действует на β и γ посредством SMul и выполняется IsScalarTower α β γ. Тогда соответствующие индуцированные действия образуют цепь скаляров между α, Filter β и Filter γ; то есть для любых a ∈ α, F ∈ Filter β и G ∈ Filter γ верно (a • F) • G = a • (F • G).
LaTeX
$$$\\forall a \\in \\alpha\\, \\forall F \\in \\mathrm{Filter}(\\beta)\\, \\forall G \\in \\mathrm{Filter}(\\gamma): (a \\cdot F) \\cdot G = a \\cdot (F \\cdot G).$$$
Lean4
@[to_additive]
instance isScalarTower' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
IsScalarTower α (Filter β) (Filter γ) :=
⟨fun a f g => by
refine (map_map₂_distrib_left fun _ _ => ?_).symm
exact (smul_assoc a _ _).symm⟩
