Zulip Chat Archive

Stream: triage

Topic: issue #2553: Quadratic forms over Q_p

Random Issue Bot (Nov 17 2020 at 14:21):

Today I chose issue 2553 for discussion!

Quadratic forms over Q_p
Created by @Johan Commelin (@jcommelin) on 2020-04-28
Labels: feature-request

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

Johan Commelin (Nov 17 2020 at 14:21):

No progress. Nothing to see here. Please move on.

Random Issue Bot (Nov 30 2020 at 14:22):

Today I chose issue 2553 for discussion!

Quadratic forms over Q_p
Created by @Johan Commelin (@jcommelin) on 2020-04-28
Labels: feature-request

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

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

Today I chose issue 2553 for discussion!

Quadratic forms over Q_p
Created by @Johan Commelin (@jcommelin) on 2020-04-28
Labels: feature-request

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

Random Issue Bot (Mar 19 2021 at 14:21):

Today I chose issue 2553 for discussion!

Quadratic forms over Q_p
Created by @Johan Commelin (@jcommelin) on 2020-04-28
Labels: feature-request

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

Random Issue Bot (Apr 14 2021 at 14:23):

Today I chose issue 2553 for discussion!

Quadratic forms over Q_p
Created by @Johan Commelin (@jcommelin) on 2020-04-28
Labels: feature-request

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

Kevin Buzzard (Apr 14 2021 at 15:05):

This would be a neat student project. @Jason KY. would you be interested in working on this after exams? It would use bilinear forms and quadratic forms. It's the p-adic analogue of the theorem that every nondegenerate quadratic form over the reals is isomorphic to ∑i≤axi2−∑i>axi2.\sum_{i\leq a}x_i^2 - \sum_{i>a}x_i^2.

Jason KY. (Apr 14 2021 at 15:10):

Definitely, this sounds very interesting and I intend to work a lot more with lean after the exams. We still don't have the real version of this and I believe and it should be easy to knock out since we have most of the infrastructure now. I experimented a bit with this a long time before but the APIs for isometry is not quite there yet. So that can be a nice place to start!

Johan Commelin (Apr 14 2021 at 15:21):

There is a sibling issue for Sylvester's theorem

Johan Commelin (Apr 14 2021 at 15:22):

It's #2551

Random Issue Bot (Oct 05 2021 at 15:03):

Today I chose issue 2553 for discussion!

Quadratic forms over Q_p
Created by @Johan Commelin (@jcommelin) on 2020-04-28
Labels: feature-request

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

Johan Commelin (Oct 05 2021 at 15:04):

We have henselian rings now. That should help.

Johan Commelin (Oct 05 2021 at 15:04):

Otherwise, no progress that I know of

Random Issue Bot (Sep 26 2022 at 14:33):

Today I chose issue 2553 for discussion!

Quadratic forms over Q_p
Created by @Johan Commelin (@jcommelin) on 2020-04-28
Labels: feature-request

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

Last updated: Dec 20 2023 at 11:08 UTC