natCast_def — Mathlib

English

Let N be an R-module. For every natural number n, the endomorphism of N obtained by the canonical embedding of ℕ into End_R(N) is the same as the endomorphism given by multiplying every element by n; i.e. the endomorphism corresponding to n is the n-fold scalar action: x ↦ n·x.

Русский

Пусть N — модуль над кольцом R. Для каждого натурального числа n тождественный эндоморфизм, получаемый из канонического отображения ℕ в End_R(N), совпадает с эндоморфизмом, заданным умножением на n: x ↦ n·x.

LaTeX

$$$ (n : \operatorname{End}_R(N)) = n \cdot \mathrm{id}_N $$$

Lean4

theorem natCast_def (n : ℕ) [AddCommMonoid N₁] [Module R N₁] : (↑n : Module.End R N₁) = Module.toModuleEnd R N₁ n :=
  rfl

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