nsmul_eq_mul — Mathlib

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

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