intCast_def — Mathlib

English

For any N₁ that is an additive group and an R-module, and any integer z, the endomorphism of N₁ corresponding to z via the canonical integer-to-endomorphism embedding equals the endomorphism given by z acting by scalar multiplication: z • id_N.

Русский

Пусть N₁ — аддитивная группа и R-модуль. Для любого целого z эндоморфизм End_R(N₁), соответствующий z через каноническое отображение Z → End_R(N₁), совпадает с эндоморфизмом, задаваемым умножением на z: z · id_N.

LaTeX

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

Lean4

theorem intCast_def (z : ℤ) [AddCommGroup N₁] [Module R N₁] : (z : Module.End R N₁) = Module.toModuleEnd R N₁ z :=
  rfl

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