nsmul_eq_mul — Mathlib

English

For a non-associative semiring α, and natural n, n • a = n · a (scalar multiplication by n equals nat-cast multiplication).

Русский

Для неполного полугруппы α и натурального n верно n • a = n · a (скалярное умножение на n равно умножению на натуральное число).

LaTeX

$$$ n \cdot a = n \cdot a $$$

Lean4

@[simp]
theorem nsmul_eq_mul (n : ℕ) (a : α) : n • a = n * a := by
  induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, zero_mul]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]

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