wip markdown cleanup - #42578
Conversation
harahu
commented
Aug 8, 2026
PR summary a699d63277Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| ## TODO | ||
| * relate this to `ChosenPullbacksAlong` which is defined in |
There was a problem hiding this comment.
| ## TODO | |
| * relate this to `ChosenPullbacksAlong` which is defined in | |
| ## TODO | |
| * Relate this to `ChosenPullbacksAlong` which is defined in |
I think
There was a problem hiding this comment.
I'd like to fix this as well, but across mathlib there is at least 1000 instances of headers missing a newline after it, so I think that is best done as a separate PR. Makes for easier reviewing.