local fields

Stream: maths

[Kevin Buzzard]

I'm staring at Serre's "Local Fields" and am wondering if I can persuade some MSc or PhD students here to formalise bits of it. But it would be nice to start them off with a definition. We have all of these facts about norms in the perfectoid project. But the key definition right at the start of Serre's book is $v : K \to \mathbb{Z}\cup\{\infty\}.$ Do you think it's wise to bite the bullet and just formalise things like this? It's additive not multiplicative notation, and there's infinity. @Johan Commelin do you have an opinion?

[Johan Commelin]

Translating Serre to multiplicative notation on the fly should be trivial. A good mathematician wouldn't even see the difference. It would allow reusing 1500 lines of code from the perfectoid project (-;

[Johan Commelin]

Note that with #1687 we now have no excuse anymore to not work on local fields (-;

[Kevin Buzzard]

Hmm. But we don't have to_multiplicative :-/

[Kevin Buzzard]

Which monoid should I use?

[Sebastien Gouezel]

Note that with #1687 we now have no excuse anymore to not work on local fields (-;

Wait a second, this PR is only done aiming at partitions of unity on manifolds modelled on finite-dimensional real vector spaces. You don't have the right to use it for local fields! :)

[Johan Commelin]

@Sebastien Gouezel Too bad... you should have used a different license.

[Johan Commelin]

@Kevin Buzzard I guess the monoid with_zero (multiplicative int). But maybe just using nnreal is even better. And then add a is_discrete predicate on top of it.