[Merged by Bors] - feat(algebra/group_with_zero): add some equational lemmas #7705
Conversation
fpvandoorn
added
the
awaiting-review
| @@ -366,7 +366,7 @@ classical.by_contradiction $ λ ha, h₁ $ mul_right_cancel' ha $ h₂.symm ▸ | |||
| end cancel_monoid_with_zero | |||
|
|
|||
| section group_with_zero | |||
| variables [group_with_zero G₀] | |||
| variables [group_with_zero G₀] {a b c g h x : G₀} | |||
There was a problem hiding this comment.
I'm not convinced this actually makes things better (unless you also renamed the x g and h to a b c), but also realistically it doesn't matter at all.
There was a problem hiding this comment.
I personally find lemmas where implicit arguments like this are omitted more readable (and I didn't want to add them to the lemmas I just wrote). I guess I could rename all variable names to a,b,c, but I don't really care about that myself.
There was a problem hiding this comment.
Maybe I've just been bitten too much by variables at the top of the file that steal the names I want in a smaller section and have typeclass assumptions I can't revert, and am overgeneralizing.
No change needed, the d+ was just for CI
|
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
Add some equations for `group_with_zero` that are direct analogues of lemmas for `group`. Useful for #6923.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Add some equations for
group_with_zerothat are direct analogues of lemmas forgroup.Useful for #6923.