Differential Geometry PRs

Stream: mathlib4

[Dominic Steinitz]

Following the talk on the distribution of PRs on Lean Together, I did a quick query:

https://github.com/leanprover-community/mathlib4/pulls?q=is%3Apr+is%3Aopen+label%3At-differential-geometry

I didn't see anything of differential forms though. I'd love one that says WIP :thank_you:

[Michael Rothgang]

I'd love a PR that's ready for review :-)

[Michael Rothgang]

Look at https://github.com/urkud/DeRhamCohomology and e.g. docs#extDeriv_apply_vectorField. As I understand it, differential forms have been formalised (and most of d²=0 for differential forms also). The missing part is largely upstreaming to mathlib.