[Merged by Bors] - chore: resolve (coe : ℤ → α) to ((↑) : ℤ → α) porting notes#11250
[Merged by Bors] - chore: resolve (coe : ℤ → α) to ((↑) : ℤ → α) porting notes#11250pitmonticone wants to merge 3 commits intomasterfrom
(coe : ℤ → α) to ((↑) : ℤ → α) porting notes#11250Conversation
pitmonticone
added
awaiting-review
easy
|
Let's just fix these; all the |
|
@eric-wieser Fixed and edited the issue and PR titles. |
pitmonticone
changed the title
(coe : ℤ → α) to (Int.cast : ℤ → α) porting notes(coe : ℤ → α) to ((↑) : ℤ → α) porting notes
|
|
||
|
|
||
| -- Porting note: changed `(coe : ℤ → α)` to `(Int.cast : ℤ → α)` | ||
| theorem gc_coe_floor : GaloisConnection (Int.cast : ℤ → α) floor := | ||
| theorem gc_coe_floor : GaloisConnection ((↑) : ℤ → α) floor := | ||
| FloorRing.gc_coe_floor | ||
| #align int.gc_coe_floor Int.gc_coe_floor |
There was a problem hiding this comment.
@YaelDillies, do you know why we have both Int.gc_coe_floor and FloorRing.gc_coe_floor? Was one about a different coercion in mathlib3?
There was a problem hiding this comment.
I think it was just for discoverability as the operator is Int.floor, not FloorRing.floor.
pitmonticone
changed the title
(coe : ℤ → α) to ((↑) : ℤ → α) porting notes(coe : ℤ → α) to ((↑) : ℤ → α) porting notes
|
bors d=@YaelDillies |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
Why not just remove the porting notes? |
|
Hi @YaelDillies, I’ve removed them and updated title and description. |
|
No, that's not what I meant. I meant "Why are you replacing |
|
@YaelDillies, I don't understand your comment, it seems to be talking about a patch that doesn't exist in this PR. |
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Oh I see I swapped the diff colors in my head 🙈
bors merge
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
(coe : ℤ → α) to ((↑) : ℤ → α) porting notes(coe : ℤ → α) to ((↑) : ℤ → α) porting notes
|
Closes #11249 |
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
3 participants
Resolves porting notes claiming "change
(coe : ℤ → α)to((↑) : ℤ → α)" by substitutingInt.castwith(↑).