Commit 2025-08-14 15:45 ed5dc595

View on Github →

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

  • birkhoffAverage_add
  • birkhoffAverage_neg
  • birkhoffAverage_sub
  • birkhoffSum_add'
  • birkhoffSum_neg
  • birkhoffSum_sub

Estimated changes

added theorem birkhoffAverage_add
added theorem birkhoffAverage_neg
added theorem birkhoffAverage_sub
added theorem birkhoffSum_add'
added theorem birkhoffSum_neg
added theorem birkhoffSum_sub