Theorem birkhoffAverage_of_comp_eq

Modification history

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 →