[Merged by Bors] - chore: fix upper/lowercase in comments#4360
[Merged by Bors] - chore: fix upper/lowercase in comments#4360
Conversation
|
I skimmed through to Mathlib/RingTheory/Ideal/Over.lean, after which github wasn't showing me the diffs without clicking once for each file. I'd be happy to merge. If anyone wants to look through the tail, that's fine too. |
| lemmas. These show the quotient map `mk : M → S → Localization S` equals the | ||
| surjection `LocalizationMap.mk'` induced by the map | ||
| `monoid_of : localization_map S (localization S)` (where `of` establishes the | ||
| `monoid_of : localization_map S (Localization S)` (where `of` establishes the |
There was a problem hiding this comment.
How about localization_map and monoid_of?
There was a problem hiding this comment.
@Ruben-VandeVelde , could you please have another look at this file?
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
Thanks! Just the one left.
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
|
bors merge |
* Run a non-interactive version of `fix-comments.py` on all files. * Go through the diff and manually add/discard/edit chunks.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
fix-comments.pyon all files.