coe_zsmul — Mathlib

English

For D and integer n, the integer scalar multiplication n • D matches the pointwise integer multiplication of the representing function.

Русский

Для целочисленного множителя n и функции D имеем: n • D равняется точечному умножению на n полученной функции.

LaTeX

$$$((n \\cdot D) : X \\to Y) = n \\cdot (D : X \\to Y)$$$

Lean4

@[simp]
theorem coe_zsmul [AddCommGroup Y] (D : locallyFinsuppWithin U Y) (n : ℤ) : (↑(n • D) : X → Y) = n • (D : X → Y) :=
  rfl

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