smulCommClass_finset'' — Mathlib

English

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

Русский

Если α и β действуют на γ и соблюдается SMulCommClass, то Finset α действует на Finset γ так, что их действия commute.

LaTeX

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

Lean4

@[to_additive]
instance smulCommClass_finset'' [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Finset α) β (Finset γ) :=
  haveI := SMulCommClass.symm α β γ
  SMulCommClass.symm _ _ _

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