Zulip Chat Archive

Stream: triage

Topic: PR #2819: [WIP] feat(number_theory/geometry_of_numbers): ...


Random Issue Bot (Nov 09 2020 at 14:18):

Today I chose PR 2819 for discussion!

[WIP] feat(number_theory/geometry_of_numbers): Minkowski's theorem
Created by @Alex J Best (@alexjbest) on 2020-05-25
Labels: WIP, help wanted, incomplete, not-ready-to-merge, please-adopt

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

Random Issue Bot (Nov 24 2020 at 14:20):

Today I chose PR 2819 for discussion!

[WIP] feat(number_theory/geometry_of_numbers): Minkowski's theorem
Created by @Alex J Best (@alexjbest) on 2020-05-25
Labels: WIP, help wanted, incomplete, not-ready-to-merge, please-adopt

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

Alex J. Best (Nov 24 2020 at 15:33):

Wow the issue bot really likes this issue, no updates since https://leanprover.zulipchat.com/#narrow/stream/263328-triage/topic/random.20PR.3A.20.5BWIP.5D.20feat%28number_theory.2Fgeometry_of_numbers%29.3A.2E.2E.2E/near/215193598

Adam Topaz (Nov 24 2020 at 15:35):

I think everyone (including the robot) wants to see this in mathlib @Alex J. Best !

Random Issue Bot (Jan 30 2021 at 14:23):

Today I chose PR 2819 for discussion!

[WIP] feat(number_theory/geometry_of_numbers): Minkowski's theorem
Created by @Alex J Best (@alexjbest) on 2020-05-25
Labels: WIP, help wanted, incomplete, not-ready-to-merge, please-adopt

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

Random Issue Bot (Feb 27 2021 at 14:19):

Today I chose PR 2819 for discussion!

[WIP] feat(number_theory/geometry_of_numbers): Minkowski's theorem
Created by @Alex J Best (@alexjbest) on 2020-05-25
Labels: WIP, help wanted, incomplete, not-ready-to-merge, please-adopt

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


Last updated: Dec 20 2023 at 11:08 UTC