Lie group and ODEs

Stream: PR reviews

[Winston Yin]

#15763 (Lie group of ring units) #16348 (Corollaries of Picard-Lindelöf ODE existence theorem)

[Winston Yin]

#15763 has already been reviewed. I believe it only needs a quick look before merging @Heather Macbeth

#16348 has only had stylistic comments, no proper review yet. It’s being used in #17140 (integral curves of vector fields)

[Oliver Nash]

I just left some review on #16348

[Winston Yin]

After playing with Lean for 1.5 years, I'm very happy to say that #16348 is my first PR merged into mathlib! Thanks very much to @Oliver Nash for the detailed review

[Oliver Nash]

Thank you @Winston Yin our library is the union of contributions from everyone just like you. Looking forward to seeing more of your PRs get merged.