smulCommClass_left — Mathlib

English

If M,N carry compatible actions with Real on the left, then NNReal M N also forms a SMulCommClass on the left; the left action commutes as required.

Русский

Если M,N имеют совместимые действия слева с Real, то для NNReal M N выполняется условие SMulCommClass слева: скаляры NNReal и элементы M коммьютируют с действием на N.

LaTeX

$$$SMulCommClass\, NNReal\, M\, N,$$$

Lean4

instance smulCommClass_left {M N : Type*} [MulAction ℝ N] [SMul M N] [SMulCommClass ℝ M N] : SMulCommClass ℝ≥0 M N where
  smul_comm r := smul_comm (r : ℝ)

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