Theorem birkhoffAverage_of_comp_eq

Modification history

2026-02-18 19:23

Mathlib/Dynamics/BirkhoffSum/Average.lean

fix(Dynamics/BirkhoffSum): birkhoffAverage_of_comp_eq only needs AddCommMonoid (#35307)

Modified birkhoffAverage_of_comp_eq View on Github →

2025-08-17 06:46

Mathlib/Dynamics/BirkhoffSum/Average.lean

feat(Dynamics/BirkhoffSum/Average): add lemma `birkhoffAverage_of_invariant` (#26842) …

Added birkhoffAverage_of_comp_eq View on Github →