Harmonic contributions to Mathlib

Stream: mathlib4

[Kim Morrison]

This thread can continue discussion from #announce > Harmonic opensources large parts of the in-house package.

[Kim Morrison]

Thank you, @Yury G. Kudryashov for these PRs and the announcement!

[Kim Morrison]

It's great to see contributions from AI lab's in-house libraries coming back to Mathlib.

[Kim Morrison]

And even better to see that they are such high quality! (i.e. thanks to you in particular for preparing them, and thanks to Harmonic for hiring someone with who can do this work so well.)