smulCommClass_filter' — Mathlib

English

Instance SMulCommClass α (Filter β) (Filter γ) holds under SMul α γ, SMul β γ, SMulCommClass α β γ.

Русский

Инстанс SMulCommClass α (Filter β) (Filter γ) существует при условии SMul α γ, SMul β γ, SMulCommClass α β γ.

LaTeX

$$$ [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Filter β) (Filter γ) $$$

Lean4

@[to_additive]
instance smulCommClass_filter' [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Filter β) (Filter γ) :=
  ⟨fun a _ _ => map_map₂_distrib_right <| smul_comm a⟩

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