heartbeats

Stream: mathlib4

[Antoine Chambert-Loir]

Just a short message to thank whoever wrote stuff that diminishes drastically the number of heartbeats in the presence of quotient algebras for the divided power algebra (https://github.com/AntoineChambert-Loir/DividedPowers4).
Last summer, we needed a million heartbeats to compute a lemma, now less than 2000 suffice!

[Anatole Dedecker]

I think @Matthew Ballard is the main person to thank here! But really thanks to anyone who worked on performance issues, I've also encountered a few "magical speedups" by merging master.

[Matthew Ballard]

I did some here I would guess but this predates the fix to defeq caching in core and depending on the precise lemma there might be a function involved @Anne Baanen

[Antoine Chambert-Loir]

Well, thanks to both of you !