smulCommClass_finset — Mathlib

English

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

Русский

Пусть α и β действуют на γ и выполнено условие SMulCommClass α β γ. Тогда на Finset γ действие α и β также коммутируют: SMulCommClass α β (Finset γ).

LaTeX

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

Lean4

@[to_additive]
instance smulCommClass_finset [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Finset γ) :=
  ⟨fun _ _ => Commute.finset_image <| smul_comm _ _⟩

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