coe_neg — Mathlib

English

Negation commutes with the evaluation: the function obtained by negating a locally finitely supported Y-valued function corresponds to the pointwise negation of its values.

Русский

Отрицание функции с локальной конечной поддержкой соответствует по точки-значениям отрицанию значений функции.

LaTeX

$$$((-D) : X \\to Y) = -(D : X \\to Y)$$$

Lean4

@[simp]
theorem coe_neg [AddCommGroup Y] (D : locallyFinsuppWithin U Y) : (↑(-D) : X → Y) = -(D : X → Y) :=
  rfl

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