int_smul_eq_zsmul — Mathlib

English

If h is a Module ℤ M and n ∈ ℤ, then h.smul n x equals the standard ℤ-action, i.e., h.smul n x = n • x.

Русский

Если h — модуль ℤ на M и n ∈ ℤ, тогда h.smul n x равен обычному действию ℤ: h.smul n x = n • x.

LaTeX

$$$\\forall {M} [\\text{AddCommGroup } M] (h : \\text{Module } \\mathbb{Z} M) (n : \\mathbb{Z}) (x : M), h.smul n x = n \\cdot x$$$

Lean4

/-- Convert back any exotic `ℤ`-smul to the canonical instance. This should not be needed since in
mathlib all `AddCommGroup`s should normally have exactly one `ℤ`-module structure by design. -/
theorem int_smul_eq_zsmul (h : Module ℤ M) (n : ℤ) (x : M) : h.smul n x = n • x :=
  Int.cast_smul_eq_zsmul ..

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