Zulip Chat Archive
Stream: triage
Topic: issue !4#5265: Improve positivity extension for norm
Random Issue Bot (Sep 12 2023 at 14:04):
Today I chose issue 5265 for discussion!
Improve positivity extension for norm
Created by @Yury G. Kudryashov (@urkud) on 2023-06-19
Labels: enhancement, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 05 2024 at 14:06):
Today I chose issue 5265 for discussion!
Improve positivity extension for norm
Created by @Yury G. Kudryashov (@urkud) on 2023-06-19
Labels: enhancement, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Eric Rodriguez (Feb 05 2024 at 16:41):
Closed in #10276.
Random Issue Bot (Nov 24 2024 at 14:11):
Today I chose issue 5265 for discussion!
Improve positivity extension for norm
Created by @Yury G. Kudryashov (@urkud) on 2023-06-19
Labels: enhancement, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Yaël Dillies (Nov 24 2024 at 15:04):
I've fixed #10276 which closes this issue. #10276 now depends on a small cleanup of normed groups lemmas in #19438
Ruben Van de Velde (Nov 24 2024 at 15:35):
#19438 is red
Yaël Dillies (Nov 24 2024 at 15:54):
@Ruben Van de Velde, fixed
Yaël Dillies (Nov 25 2024 at 13:15):
#10276 itself is ready now
Random Issue Bot (Dec 26 2024 at 14:11):
Today I chose issue 5265 for discussion!
Improve positivity extension for norm
Created by @Yury G. Kudryashov (@urkud) on 2023-06-19
Labels: enhancement, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Yaël Dillies (Dec 26 2024 at 14:14):
Should be closed later today
Last updated: May 02 2025 at 03:31 UTC