Commit 2026-08-19 13:14 7250706e

View on Github →

chore(Dynamics/BirkhofSum): improve the API for birkhoffSum and birkhoffAverage (#42447) The new changes increase naming consistency and plug API gaps.

Estimated changes

Modified Mathlib/Dynamics/BirkhoffSum/Average.lean

added theorem birkhoffAverage_add_apply

added theorem birkhoffAverage_apply_congr_ring

added theorem birkhoffAverage_apply_of_comp_eq

added theorem birkhoffAverage_comp_sub_birkhoffAverage

deleted theorem birkhoffAverage_congr_ring'

modified theorem birkhoffAverage_congr_ring

added theorem birkhoffAverage_neg_apply

deleted theorem birkhoffAverage_one'

modified theorem birkhoffAverage_one

added theorem birkhoffAverage_one_apply

added theorem birkhoffAverage_sub_apply

deleted theorem birkhoffAverage_zero'

modified theorem birkhoffAverage_zero

added theorem birkhoffAverage_zero_apply

added theorem map_comp_birkhoffAverage

Modified Mathlib/Dynamics/BirkhoffSum/Basic.lean

deleted theorem birkhoffSum_add'

modified theorem birkhoffSum_add

added theorem birkhoffSum_add_apply

added theorem birkhoffSum_add_right

added theorem birkhoffSum_add_right_apply

added theorem birkhoffSum_apply_of_comp_eq

added theorem birkhoffSum_comp_sub_birkhoffSum

modified theorem birkhoffSum_neg

added theorem birkhoffSum_neg_apply

deleted theorem birkhoffSum_one'

modified theorem birkhoffSum_one

added theorem birkhoffSum_one_apply

modified theorem birkhoffSum_sub

added theorem birkhoffSum_sub_apply

modified theorem birkhoffSum_succ'

modified theorem birkhoffSum_succ

added theorem birkhoffSum_succ_apply'

added theorem birkhoffSum_succ_apply

deleted theorem birkhoffSum_zero'

modified theorem birkhoffSum_zero

added theorem birkhoffSum_zero_apply

added theorem map_comp_birkhoffSum