[Merged by Bors] - chore: tidy various files #3124
Conversation
Ruben-VandeVelde
commented
Mar 27, 2023
Ruben-VandeVelde
commented
Ruben-VandeVelde
added
the
awaiting-review
Mathlib/Algebra/Ring/Basic.lean
Outdated
| theorem coe_mul_left [NonUnitalNonAssocSemiring R] (r : R) : | ||
| (mulLeft r : R → R) = HMul.hMul r := | ||
| theorem coe_mulLeft [NonUnitalNonAssocSemiring R] (r : R) : | ||
| (mulLeft r : R → R) = (r * ·) := |
There was a problem hiding this comment.
I'd be more inclined not to change this one. Somebody might want to write rw [<- coe_mulLeft] and that becomes harder with the new statement.
There was a problem hiding this comment.
Yeah, that's what I added mulLeft_apply for. In fact, your PR #2725 introduced this change relative to mathlib3. I think it's better to be consistent with mathlib3 as well as with coe_mulRight.
There was a problem hiding this comment.
The HMul.hMul version is closer to mathlib3, mathport introduced the change. Sometimes you want to use these lemmas on partially applied functions.
|
Apart from the one comment LGTM. bors d+ |
|
✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
Ruben-VandeVelde
added
awaiting-review
semorrison
added
awaiting-author
|
bors merge |
Ruben-VandeVelde
removed
the
awaiting-author
|
Build failed:
|
|
bors merge |
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
