Skip to content

Commit 5de7ba0

Browse files
committed
chore(Geometry/Manifold/Submersion): reword 'project intentions' phrase
As suggested privately by ; the current phrasing reads nicer and conveys what the original phrasing meant to say.
1 parent ae588ec commit 5de7ba0

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

Mathlib/Geometry/Manifold/Submersion.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -83,8 +83,8 @@ The implementation strategy is identical to the one for immersions. See the impl
8383
[schmeding2023]
8484
* Note that Margelef-Roig and Dominguez have a slightly different definition of submersions.
8585
86-
**Please do not work** on this file without prior discussion with Michael Rothgang.
87-
This will be the topic of Samantha Naranjo's master's thesis, and it's nice to coordinate.
86+
**Please talk** to Michael Rothgang before working on this file, to avoid duplicate work.
87+
The above TODOs are the topic of Samantha Naranjo's master's thesis; it's nicer to coordinate.
8888
8989
-/
9090

0 commit comments

Comments
 (0)