smulCommClass_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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