toIntModule — Mathlib

English

Any Additive Abelian group M carries a canonical Z-module structure, giving an action of the integers on M extending the abelian group structure.

Русский

Любая абелева группа M с коммутативной операцией сложения обладает канонической структурой Z-модуля, задающей действие целых чисел на M.

LaTeX

$$$\text{Module}_{\mathbb{Z}} \;M$ with $n \cdot m$ defined via repeated addition and negation$$

Lean4

instance toIntModule : Module ℤ M where
  one_smul := one_zsmul
  mul_smul m n a := mul_zsmul a m n
  smul_add n a b := zsmul_add a b n
  smul_zero := zsmul_zero
  zero_smul := zero_zsmul
  add_smul r s x := add_zsmul x r s

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