Theorem birkhoffSum_add'

Modification history

2026-08-19 13:14
Mathlib/Dynamics/BirkhoffSum/Basic.lean
chore(Dynamics/BirkhofSum): improve the API for `birkhoffSum` and `birkhoffAverage` (#42447) …
Deleted birkhoffSum_add'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_add'View on Github →