coe_nsmul — Mathlib

English

The embedding respects natural-number scalar multiplication: toEReal(n•x) = n•toEReal(x).

Русский

Встраивание сохраняет умножение на натуральные числа: toEReal(n•x) = n•toEReal(x).

LaTeX

$$$\mathrm{toEReal}(n\cdot x) = n\cdot \mathrm{toEReal}(x)$$$

Lean4

@[norm_cast]
theorem coe_nsmul (n : ℕ) (x : ℝ) : (↑(n • x) : EReal) = n • (x : EReal) :=
  map_nsmul (⟨⟨Real.toEReal, coe_zero⟩, coe_add⟩ : ℝ →+ EReal) _ _

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