smulCommClass_finset' — Mathlib

English

If SMul α γ, SMul β γ, SMulCommClass α β γ, then SMulCommClass α (Finset β) (Finset γ).

Русский

Если α и β действуют на γ и соблюдается SMulCommClass, то Finset β и Finset γ образуют SMulCommClass α (Finset β) (Finset γ).

LaTeX

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

Lean4

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

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