isScalarTower'' — Mathlib

English

IsScalarTower for Finset α, Finset β, Finset γ when IsScalarTower α β γ and SMul structures exist coordinatewise.

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance isScalarTower'' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower (Finset α) (Finset β) (Finset γ) :=
  ⟨fun a s t => coe_injective <| by simp only [coe_smul, smul_assoc]⟩

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