Zulip Chat Archive

Stream: triage

Topic: issue #2910: Port convexity to affine spaces


Random Issue Bot (Jan 04 2022 at 14:17):

Today I chose issue 2910 for discussion!

Port convexity to affine spaces
Created by @Yury G. Kudryashov (@urkud) on 2020-06-01
Labels: enhancement

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Feb 28 2022 at 14:12):

Today I chose issue 2910 for discussion!

Port convexity to affine spaces
Created by @Yury G. Kudryashov (@urkud) on 2020-06-01
Labels: enhancement

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (May 13 2022 at 14:23):

Today I chose issue 2910 for discussion!

Port convexity to affine spaces
Created by @Yury G. Kudryashov (@urkud) on 2020-06-01
Labels: enhancement

Is this issue still relevant? Any recent updates? Anyone making progress?

Yaël Dillies (May 13 2022 at 16:06):

The first half is done, namely porting to semimodules. The second half requires redefining affine spaces to not talk about negation. I went to do that 6 months ago but I wasn't getting the axioms right.

Random Issue Bot (Feb 10 2023 at 14:09):

Today I chose issue 2910 for discussion!

Port convexity to affine spaces
Created by @Yury G. Kudryashov (@urkud) on 2020-06-01
Labels: enhancement

Is this issue still relevant? Any recent updates? Anyone making progress?

Yury G. Kudryashov (Feb 10 2023 at 15:40):

Probably, the answer is: not before we port to Lean 4.

Reid Barton (Feb 10 2023 at 15:43):

Port Convexity to AffineSpaces

Random Issue Bot (Jul 02 2023 at 14:07):

Today I chose issue 2910 for discussion!

Port convexity to affine spaces
Created by @Yury G. Kudryashov (@urkud) on 2020-06-01
Labels: enhancement

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Jul 18 2023 at 14:07):

Today I chose issue 2910 for discussion!

Port convexity to affine spaces
Created by @Yury G. Kudryashov (@urkud) on 2020-06-01
Labels: enhancement

Is this issue still relevant? Any recent updates? Anyone making progress?


Last updated: Dec 20 2023 at 11:08 UTC