Zulip Chat Archive
Stream: triage
Topic: PR #7891: feat(algebra/ordered_{field, group}): lemmas ab...
Random Issue Bot (Jan 09 2022 at 14:17):
Today I chose PR 7891 for discussion!
feat(algebra/ordered_{field, group}): lemmas about a / b ≤ a / c
Created by @Benjamin Davidson (@benjamindavidson) on 2021-06-11
Labels: awaiting-author, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Arthur Paulino (Jan 09 2022 at 14:59):
I can try to fix this one. Seems like a merge conflict
Arthur Paulino (Jan 09 2022 at 16:16):
Alright, master advanced a lot since this one was open and the only things that I could spot that haven't been declared on master are on this PR: #11333
I didn't want to push directly to that branch because I had to drop some declarations. Please let me know if I forgot something important!
Random Issue Bot (Apr 09 2022 at 14:13):
Today I chose PR 7891 for discussion!
feat(algebra/ordered_{field, group}): lemmas about a / b ≤ a / c
Created by @Benjamin Davidson (@benjamindavidson) on 2021-06-11
Labels: awaiting-author, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Eric Wieser (Apr 09 2022 at 16:05):
@Arthur Paulino, am I right in thinking that in your opinion this PR is now fully merged elsewhere, and you just want someone else to double check?
Arthur Paulino (Apr 09 2022 at 16:42):
Eric Wieser said:
Arthur Paulino, am I right in thinking that in your opinion this PR is now fully merged elsewhere, and you just want someone else to double check?
Yeah I did the migration myself because I didn't want to push to that branch directly
Arthur Paulino (Apr 09 2022 at 16:43):
Random Issue Bot (Apr 25 2022 at 14:20):
Today I chose PR 7891 for discussion!
feat(algebra/ordered_{field, group}): lemmas about a / b ≤ a / c
Created by @Benjamin Davidson (@benjamindavidson) on 2021-06-11
Labels: awaiting-author, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Yaël Dillies (Apr 25 2022 at 14:21):
I believe this is outdated now. Can you confirm @Damiano Testa?
Damiano Testa (Apr 26 2022 at 13:13):
I have a little of a backlog, but I agree that this is outdated. These lemmas were ported over by Arthur, and will likely be true in a more general context via covariant_classes soon.
Last updated: Dec 20 2023 at 11:08 UTC