[Merged by Bors] - chore: remove duplicated definition of Invertible class in NormNum.Core.lean#1313
[Merged by Bors] - chore: remove duplicated definition of Invertible class in NormNum.Core.lean#1313
Conversation
Mathlib/Tactic/NormNum/Core.lean
Outdated
| inv : Invertible denom | ||
| /-- The element is equal to the fraction with the specified numerator and denominator. -/ | ||
| eq : a = num * ⅟denom | ||
| eq : a = num * ⅟ denom |
There was a problem hiding this comment.
We may want to define this syntax with prefix rather than notation here:
mathlib4/Mathlib/Algebra/Invertible.lean
Lines 79 to 81 in 089d3a2
As is, we need to insert this space.
There was a problem hiding this comment.
That seems reasonable to me. Are there any other side effects of making something prefix rather than notation?
There was a problem hiding this comment.
The usages of the syntax in that file (e.g. here:
mathlib4/Mathlib/Algebra/Invertible.lean
Line 94 in 089d3a2
There was a problem hiding this comment.
@ChrisHughes24 was there a reason for using notation rather than prefix here? It seems like prefix:max would be the most analogous to the Inv.inv notation:
mathlib4/Mathlib/Algebra/Group/Defs.lean
Line 111 in cac405f
There was a problem hiding this comment.
I was mistaken-- the prefix:max version does not actually seem to require other changes, so I went ahead and did that.
|
|
||
| /-- The inverse of an `Invertible` element -/ | ||
| notation:1034 | ||
| prefix:max |
There was a problem hiding this comment.
Note that this change makes this notation more closely match the Inv.inv notation:
mathlib4/Mathlib/Algebra/Group/Defs.lean
Line 111 in cac405f
and it makes the comment on the next line more true.
|
LGTM. I'm delegating rather than merging in case there was a reason that you didn't mark it "awaiting review" yet. bors d+ |
|
✌️ dwrensha can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
…re.lean (#1313) * Deletes the temporary `Invertible` class defined in `NormNum.Core`. This is possible because `Algebra.Invertible` landed in #930, and its dependence on `NormNum` was removed in #1055. * Updates the definition of the `Invertible.toInv` syntax to not require a space and to more closely match the `Inv.inv` syntax.
|
Pull request successfully merged into master. Build succeeded:
|
Invertibleclass defined inNormNum.Core. This is possible becauseAlgebra.Invertiblelanded in [Merged by Bors] - feat port: Algebra.Invertible #930, and its dependence onNormNumwas removed in [Merged by Bors] - feat port Algebra.GroupPower.Lemmas #1055.Invertible.toInvsyntax to not require a space and to more closely match theInv.invsyntax.