English
Let F be a type equipped with FunLike and AddMonoidHomClass structures, and let g' : F be a monoid hom. Then for all f: α→α, g: α→M, n ∈ ℕ, x ∈ α, g'(birkhoffSum f g n x) = birkhoffSum f (g' ∘ g) n x.
Русский
Пусть F оборудован структурой FunLike и AddMonoidHomClass, и пусть g' : F является моноидным однородным отображением. Тогда для всех f: α→α, g: α→M, n ∈ ℕ и x ∈ α выполняется: g'(birkhoffSum f g n x) = birkhoffSum f (g' ∘ g) n x.
LaTeX
$$$g'(\\mathrm{birkhoffSum}(f,g,n,x))=\\mathrm{birkhoffSum}(f,g'\\circ g,n,x)$$$
Lean4
theorem map_birkhoffSum {F N : Type*} [AddCommMonoid N] [FunLike F M N] [AddMonoidHomClass F M N] (g' : F) (f : α → α)
(g : α → M) (n : ℕ) (x : α) : g' (birkhoffSum f g n x) = birkhoffSum f (g' ∘ g) n x :=
map_sum g' _ _
