neg_apply — Mathlib

English

For every n, the nth term of the negated formal multilinear series is the negation of the nth term: (-f)(n) = -f(n).

Русский

Для каждого n n-ая компонента отрицательного формального мультилинейного ряда равна отрицанию соответствующей компоненты: (-f)(n) = -f(n).

LaTeX

$$$(-f)_n = -\,f_n$$$

Lean4

@[simp]
theorem neg_apply (f : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (-f) n = -f n :=
  rfl

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