[Merged by Bors] - feat: Port algebra.order.EuclideanAbsoluteValue #1267
Conversation
aricursion
added
the
awaiting-review
The best way to ask a question like this is to start a review of your own PR in which you add the comment directly on the relevant line. And if the issue gets resolved (which seems to be the case here), you can clearly mark it as such. |
|
Ah ok. Good to know! Thanks! |
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
|
You can have a look at the new naming convention here in the section "Aligning names". Since it's a bit more fine-grained than in mathlib3, mathport gets it wrong quite often and a lot of it has to be done manually. |
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
|
Thanks! Sorry I'm new to porting and completely forgot to update the names in the docstrings. thank you so much! |
|
bors merge |
github-actions
bot
added
ready-to-merge
Small PR. Nothing super special here, although I did have a question. On line 74, is it within style guidelines to use `@` to make the parameters explicit? Thanks! Co-authored-by: z <32079362+xoers@users.noreply.github.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Small PR. Nothing super special here, although I did have a question. On line 74, is it within style guidelines to use
@to make the parameters explicit? Thanks!