smulCommClass_left — Mathlib

English

Left commutativity of scalar actions transfers from ENNReal to NNReal under the given compatible actions.

Русский

Левая симметричность скалярных действий сохраняется при переходе от ENNReal к NNReal.

LaTeX

$$$\\text{smulCommClass\_left}:\\ SMulCommClass\\ NNReal\\ M\\ N$$$

Lean4

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

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