New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(*): replace abs
with vertical bar notation
#8891
Conversation
bf845d2
to
e7d7de2
Compare
bdc242b
to
01c403e
Compare
56d1e81
to
4a69021
Compare
673b796
to
4850439
Compare
4850439
to
0951baf
Compare
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
After you resolve the merge conflict, can you update the PR title / description to make it more clear how this differs from / builds on #9172? Thanks! |
abs
with vertical bar notation
Okay, if you could just fix the minor issue above, all else looks great. Thanks for this. bors d+ |
✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
bors r- |
Canceled. |
bors r+ |
Canceled. |
bors r- |
bors r+ |
The notion of an "absolute value" occurs both in algebra (e.g. lattice ordered groups) and analysis (e.g. GM and GL-spaces). I introduced a `has_abs` notation class in #9172, along with the conventional mathematical vertical bar notation `|.|` for `abs`. The notation vertical bar notation was already in use in some files as a local notation. This PR replaces `abs` with the vertical bar notation throughout mathlib.
Pull request successfully merged into master. Build succeeded: |
abs
with vertical bar notationabs
with vertical bar notation
The notion of an "absolute value" occurs both in algebra (e.g. lattice ordered groups) and analysis (e.g. GM and GL-spaces). I introduced a
has_abs
notation class in #9172, along with the conventional mathematical vertical bar notation|.|
forabs
.The notation vertical bar notation was already in use in some files as a local notation. This PR replaces
abs
with the vertical bar notation throughout mathlib.