English
For every natural number n and every extended real x, the n-fold additive scaling equals ordinary multiplication by n, i.e., n • x = n · x.
Русский
Для каждого натурального числа n и каждого элемента расширенных вещественных чисел x выполняется n • x = n · x.
LaTeX
$$$\\forall n \\in \\mathbb{N},\\ \\forall x \\in \\overline{\\mathbb{R}},\\ n\\cdot x = n\\,x$$$
Lean4
@[simp]
theorem nsmul_eq_mul (n : ℕ) (x : EReal) : n • x = n * x := by
induction n with
| zero => rw [zero_smul, Nat.cast_zero, zero_mul]
| succ n ih =>
rw [succ_nsmul, ih, Nat.cast_succ]
convert (EReal.right_distrib_of_nonneg _ _).symm <;> simp