instSMulCommClass_1 — Mathlib

English

There is SMulCommClass PUnit R S, i.e., the scalar actions by R and S commute on PUnit when PUnit carries compatible SMul structures.

Русский

Существует SMulCommClass PUnit R S, то есть скалярные действия R и S commute на PUnit при наличии совместимых структур скалярного умножения.

LaTeX

$$$\\text{SMulCommClass } PUnit\\; R\\; S.$$$

Lean4

@[to_additive]
instance [SMul R S] : SMulCommClass PUnit R S :=
  ⟨by simp⟩

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