birkhoffSum_neg — Mathlib

English

For any f: α→α and g: α→G with G an AddCommGroup, birkhoffSum f (-g) n x = - birkhoffSum f g n x for all n ∈ ℕ and x ∈ α.

Русский

Для любого f: α→α и g: α→G, где G — аддитивная коммутативная группа, выполняется birkhoffSum(f, -g, n, x) = -birkhoffSum(f, g, n, x).

LaTeX

$$$\\mathrm{birkhoffSum}(f,-g,n,x)=-\\mathrm{birkhoffSum}(f,g,n,x)$$$

Lean4

theorem birkhoffSum_neg (f : α → α) (g : α → G) (n : ℕ) (x : α) : birkhoffSum f (-g) n x = -birkhoffSum f g n x := by
  simp [birkhoffSum]

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