smulCommClass_filter'' — Mathlib

English

Another variant of lifting SMulCommClass to Filter objects: SMulCommClass (Filter α) β (Filter γ).

Русский

Ещё один вариант переноса SMulCommClass на объекты Filter: SMulCommClass (Filter α) β (Filter γ).

LaTeX

$$$ SMulCommClass (Filter α) \beta (Filter γ) $$$

Lean4

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

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