coe_nsmul — Mathlib

English

For a locally finitely supported Y-valued function D and a natural number n, the function n • D corresponds to n times the pointwise values of D.

Русский

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

LaTeX

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

Lean4

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

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