Theorem birkhoffSum_neg

Modification history

2026-08-19 13:14

Mathlib/Dynamics/BirkhoffSum/Basic.lean

chore(Dynamics/BirkhofSum): improve the API for `birkhoffSum` and `birkhoffAverage` (#42447) …

Modified birkhoffSum_neg View on Github →

2025-08-14 15:45

Mathlib/Dynamics/BirkhoffSum/Basic.lean

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

Added birkhoffSum_neg View on Github →