intCast_apply — Mathlib

English

For AddCommGroup M, the action of integers on endomorphisms corresponds to scalar multiplication: (z : ℤ) • m maps to z • m.

Русский

Для AddCommGroup M действие целых чисел на концевые отображения соответствует умножению: z • m.

LaTeX

$$$\forall z\in\mathbb{Z},\;\forall m\in M:\; (\uparrow z : \mathrm{AddMonoid.End}\,M)\,m = z\cdot m$$$

Lean4

/-- See also `AddMonoid.End.intCast_def`. -/
@[simp]
theorem intCast_apply [AddCommGroup M] (z : ℤ) (m : M) : (↑z : AddMonoid.End M) m = z • m :=
  rfl

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