instSMulCommClassForall_2 — Mathlib

English

If SMul actions of M on α and N on α commute, then the lifted actions on α → β also commute, i.e., the instance provides SMulCommClass (DomMulAct M) (DomMulAct N) (α → β).

Русский

Если действия скаляров M и N на α коммутируют, то их увеличенное действие на множество функций α → β также коммутирует.

LaTeX

$$$SMulCommClass (DomMulAct M) (DomMulAct N) (\alpha \to \beta)$$$

Lean4

@[to_additive]
instance [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (α → β) where
  smul_comm _ _ f := funext fun _ ↦ congr_arg f (smul_comm _ _ _).symm

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