Theorem birkhoffAverage_neg

Modification history

2025-08-14 15:45

Mathlib/Dynamics/BirkhoffSum/Average.lean

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

Added birkhoffAverage_neg View on Github →