Theorem birkhoffAverage_comp_sub_birkhoffAverage

Modification history

2026-08-19 13:14
Mathlib/Dynamics/BirkhoffSum/Average.lean
chore(Dynamics/BirkhofSum): improve the API for `birkhoffSum` and `birkhoffAverage` (#42447) …
Added birkhoffAverage_comp_sub_birkhoffAverageView on Github →