smulCommClass_filter — Mathlib

English

The structure SMulCommClass α β (Filter γ) holds when SMul α γ, SMul β γ, and SMulCommClass α β γ hold.

Русский

Структура SMulCommClass α β (Filter γ) сохраняется при условии SMul α γ, SMul β γ и SMulCommClass α β γ.

LaTeX

$$$ SMulCommClass\; \alpha\; \beta\; (Filter\; \gamma)$$$

Lean4

@[to_additive]
instance smulCommClass_filter [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Filter γ) :=
  ⟨fun _ _ _ => map_comm (funext <| smul_comm _ _) _⟩

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