Theorems · Theorem · dynamical systems

Function.IsFixedPt.birkhoffSum_eq

∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → α} {x : α},
  Function.IsFixedPt f x → ∀ (g : α → M) (n : ℕ), birkhoffSum f g n x = n • g x

Defined in

Mathlib.Dynamics.BirkhoffSum.Basic

Cited by

1 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoid