Theorem birkhoffAverage_add

Modification history

2025-08-14 15:45

Mathlib/Dynamics/BirkhoffSum/Average.lean

feat(Mathlib/Dynamics/BirkhoffSum/Average): add 3 BirkhoffAverage lemmas (#26840) …

Added birkhoffAverage_add View on Github →