[Merged by Bors] - feat(algebra/*): Algebraic instances on lex/order_dual
#16122
Conversation
YaelDillies
added
awaiting-review
|
I can already hear Eric talking about |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
YaelDillies
changed the title
lexlex/order_dual
|
I moved the instances closer to the definitions of the corresponding typeclasses because the pattern of putting instances that are defined in |
src/algebra/group/basic.lean
Outdated
|
|
||
| open order_dual | ||
|
|
||
| @[to_additive] instance : Π [has_one α], has_one αᵒᵈ := id |
There was a problem hiding this comment.
@urkud said that using id was a bad idea since it's one more thing to unfold
| @[to_additive] instance : Π [has_one α], has_one αᵒᵈ := id | |
| @[to_additive] instance [has_one α] : has_one αᵒᵈ := ‹has_one α› |
There was a problem hiding this comment.
For future reference, here's a regex that works to turn one into the other: : Π \[(.*)\],(.*)id, [h : $1] :$2h
|
|
||
| open order_dual | ||
|
|
||
| @[to_additive] instance [h : has_one α] : has_one αᵒᵈ := h |
There was a problem hiding this comment.
Note that
| @[to_additive] instance [h : has_one α] : has_one αᵒᵈ := h | |
| @[to_additive] instance [has_one α] : has_one αᵒᵈ := ‹has_one α› |
avoids h : appearing in the docs; but perhaps this is too minor to care about.
There was a problem hiding this comment.
Yeah, it's mostly harder to industrialise because of the line-wrapping 😦
|
bors merge |
|
Merge conflict. |
|
Let's try again bors merge |
Copy over algebraic instances for `lex` and `order_dual`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
lex/order_duallex/order_dual
#16847 copied over the copyright from `algebra.group.basic` without actually attributing things properly. All the material in `algebra.group.commutator` is from #12309 and the material is mostly from #16122 with some dating back from #8564 Also fix `order_dual.has_pow` being additivized as `order_dual.has_nsmul` rather than `order_dual.has_smul`.
…e names (#16967) #16847 copied over the copyright from `algebra.group.basic` without actually attributing things properly. All the material in `algebra.group.commutator` is from #12309 and the material is mostly from #16122 with some dating back from #8564 Also fix `order_dual.has_pow` being additivized as `order_dual.has_nsmul` rather than `order_dual.has_smul`.
Copy over algebraic instances for
lexandorder_dual.