PR !4#33307: Orientable manifolds updated

Stream: triage

[Random Issue Bot]

Today I chose PR #33307 for discussion!

Orientable manifolds updated
Created by @Michael Rothgang (@grunweg) on 2025-12-26
Labels: WIP, t-differential-geometry

Is this PR still relevant? Any recent updates? Anyone making progress?

[Rida Hamadani]

I have some free time this week so I will try to take another stab at this.

[Rida Hamadani]

@Michael Rothgang is it possible to acquire writing permission to this PR?

[Michael Rothgang]

It's great to hear that you'd like to move this forward. I'm not sure if writing permissions to this PR (without permissions to all my PRs... which I'm careful with) is possible. That said: can you just create a new branch based off my PR, and work on that?

[Michael Rothgang]

(Then you can make a PR to mathlib against #33307, I can review and merge this... or we actually close #33307 in favour of your PR, as I was mostly just merging master on your old PR...)

[Michael Rothgang]

If you have gh installed, I can do gh pr checkout 12345 to locally check out the branch for PR 12345 (assuming I don't have it already). Then, doing git switch -c mynewbranch will create a new branch on my fork, to which I can push commits. Does that help? If you have questions, please ask!

[Rida Hamadani]

Ah I thought giving acess to a single PR would be feature github will have. I will see if I'm able to do progress on this locally and then I can leave suggestions as reviews (the old PR should be closed anyways since it is from the pre-fork days)