English
The embedding commutes with natural-number scalar multiplication: (n • x) in ENNReal maps to n • (x:EReal).
Русский
Вложение коммутирует умножение на натуральное число: n • x в ENNReal сопоставляется n • (x:EReal).
LaTeX
$$$$ (n \cdot x)^{EReal} = n \cdot (x^{EReal}), \; n \in \mathbb{N}, \; x \in ENNReal. $$$$
Lean4
@[norm_cast]
theorem coe_ennreal_nsmul (n : ℕ) (x : ℝ≥0∞) : (↑(n • x) : EReal) = n • (x : EReal) :=
map_nsmul (⟨⟨(↑), coe_ennreal_zero⟩, coe_ennreal_add⟩ : ℝ≥0∞ →+ EReal) _ _