isScalarTower — Mathlib

English

If SMul α β, SMul α γ, SMul β γ and IsScalarTower α β γ hold, then IsScalarTower α β (Filter γ).

Русский

Если есть совместные скаляры α, β, γ и IsScalarTower α β γ, то IsScalarTower α β (Filter γ).

LaTeX

$$$ IsScalarTower\; \alpha\; \beta\; \gamma \Rightarrow IsScalarTower\; \alpha\; \beta\; (Filter\; \gamma) $$$

Lean4

@[to_additive]
instance isScalarTower [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Filter γ) :=
  ⟨fun a b f => by simp only [← Filter.map_smul, map_map, smul_assoc]; rfl⟩

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