English
Let f: α → α and g, g': α → M with M an AddCommMonoid. Then for all n ∈ ℕ and x ∈ α, birkhoffSum f (g+g') n x = birkhoffSum f g n x + birkhoffSum f g' n x.
Русский
Пусть f: α → α и два наблюдаемых g, g': α → M, где M — аддитивный коммутативный моноид. Тогда для любого n ∈ ℕ и x ∈ α выполняется birkhoffSum(f, g+g', n, x) = birkhoffSum(f, g, n, x) + birkhoffSum(f, g', n, x).
LaTeX
$$$\\mathrm{birkhoffSum}(f,g+g',n,x)=\\mathrm{birkhoffSum}(f,g,n,x)+\\mathrm{birkhoffSum}(f,g',n,x)$$$
Lean4
theorem birkhoffSum_add' (f : α → α) (g g' : α → M) (n : ℕ) (x : α) :
birkhoffSum f (g + g') n x = birkhoffSum f g n x + birkhoffSum f g' n x := by
simpa [birkhoffSum] using sum_add_distrib
