cast_smul_eq_nsmul — Mathlib

English

The cast from ℕ to any ring coheres with scalar action on modules, i.e., the natural cast of numbers acts the same as repeated addition.

Русский

Натуральные числа, приводимые в кольцо через каноническое преобразование, действуют на модуле так же, как повторное сложение.

LaTeX

$$$\forall n\in\mathbb{N},\; (n)\mapsto n$ acts compatibly with smul on M$$

Lean4

/-- `nsmul` is equal to any other module structure via a cast. -/
@[norm_cast]
theorem cast_smul_eq_nsmul (n : ℕ) (b : M) : (n : R) • b = n • b := by
  induction n with
  | zero => rw [Nat.cast_zero, zero_smul, zero_smul]
  | succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]

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