isScalarTower — Mathlib

English

If α, β, γ are such that SMul α β, SMul α γ, SMul β γ, and IsScalarTower α β γ, then IsScalarTower α β (Finset γ).

Русский

Если даны действии по схожей схеме и тождество IsScalarTower между α, β и γ, то это верно и на Finset γ, с соответствующим образованием действия.

LaTeX

$$$IsScalarTower\ α\ β\ (Finset\ γ).$$$

Lean4

@[to_additive]
instance isScalarTower [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Finset γ) :=
  ⟨fun a b s => by simp only [← image_smul, image_image, smul_assoc, Function.comp_def]⟩

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