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