instSMulCommClass — Mathlib

English

There is an SMulCommClass instance for Option α induced from SMulCommClass M N α using option_map; any two actions commute on Option α.

Русский

Для типа Option α имеется инстанс SMulCommClass, выведенный из SMulCommClass M N α через Function.Commute и option_map; действия совместимы на Option α.

LaTeX

$$$[SMulCommClass M N α] \Rightarrow SMulCommClass M N (Option α)$$

Lean4

@[to_additive]
instance [SMulCommClass M N α] : SMulCommClass M N (Option α) :=
  ⟨fun _ _ => Function.Commute.option_map <| smul_comm _ _⟩

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