ofNat_smul_eq_nsmul — Mathlib

English

The equality (n : R) • b = n • b holds for all natural numbers n and elements b of any module M over a ring R.

Русский

Необходимо, чтобы равенство (n : R) • b = n • b выполнялось для всех натуральных чисел n и элементов b модуля M над кольцом R.

LaTeX

$$$ (n : R) \cdot b = n \cdot b $$$

Lean4

/-- `nsmul` is equal to any other module structure via a cast. -/
theorem ofNat_smul_eq_nsmul (n : ℕ) [n.AtLeastTwo] (b : M) : (ofNat(n) : R) • b = ofNat(n) • b :=
  Nat.cast_smul_eq_nsmul ..

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