[Merged by Bors] - chore(algebra/invertible): units coerced to their monoid are invertible #8195
Conversation
eric-wieser
commented
Jul 5, 2021
•
eric-wieser
commented
Also enables two obvious instances.
eric-wieser
added
the
awaiting-review
src/algebra/invertible.lean
Outdated
| instance units.invertible [monoid α] (u : units α) : invertible (u : α) := | ||
| { inv_of := ↑(u⁻¹), inv_of_mul_self := u.inv_mul, mul_inv_of_self := u.mul_inv } |
There was a problem hiding this comment.
I'm also a bit wary about coherence issues between this instance and others, especially invertible_of_group. Probably this one + invertible_one are fine since there is a cast in the conclusion. So e.g. we won't see the typeclass system reduce ↑(1 : units ℤ) to 1 : ℤ, right?
There was a problem hiding this comment.
Let's play it safe, I'll just back out the instances for now
There was a problem hiding this comment.
Let's put a warning in the "implementation notes" above, so the next people to come across the file will know. I can't make a suggestion there, but how about something like:
Since `invertible a` is not a `Prop` (but it is a `subsingleton`), we have to be careful about coherence issues:
we should avoid having multiple non-defeq instances for `invertible a` in the same context.
This file plays it safe and uses `def` rather than `instance` for most definitions,
users can choose which instances to use at the point of use.
For example, here's how you can use an `invertible 1` instance:
```lean
variables {α : Type*} [monoid α]
def something_that_needs_inverses (x : α) [invertible x] := sorry
section
local attribute [instance] invertible_one
def something_one := something_that_needs_inverses 1
end
```
There was a problem hiding this comment.
I don't fully buy that argument (and looking at the Zulip thread nor really did @digama0), so would prefer not to be responsible for PRing it.
Can you make a new PR adding that text?
…ances In the discussion on #8195, I suggested to add these implementation notes. Creating a new PR should allow for a bit more direct discussion on the use and plans for `invertible.`
|
LGTM! bors d+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
