## Stream: maths

### Topic: local fields

#### Kevin Buzzard (Nov 14 2019 at 19:16):

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 (Nov 14 2019 at 19:20):

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 (Nov 14 2019 at 19:32):

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

#### Kevin Buzzard (Nov 14 2019 at 19:41):

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

#### Kevin Buzzard (Nov 14 2019 at 19:41):

Which monoid should I use?

#### Sebastien Gouezel (Nov 14 2019 at 19:45):

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 (Nov 14 2019 at 19:48):

@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.