## Stream: maths

### Topic: polynomial

#### Patrick Massot (Jul 19 2018 at 09:16):

What's happening with polynomials? I see ce990c59d authored by Chris and merged by Johannes but PR171 is still open and active

#### Mario Carneiro (Jul 19 2018 at 09:17):

I think Johannes is currently working on merging the Mason Stothers work with Chris's

#### Patrick Massot (Jul 19 2018 at 09:24):

That's really nice

#### Patrick Massot (Jul 19 2018 at 09:26):

It's really important part of elementary maths that was missing.

#### Patrick Massot (Jul 19 2018 at 09:27):

It makes me think of my normed space work again. Do you think I should PR https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/norms.lean (after removing the type class inference nightmare at the end). Would it help in getting more motivation to fix the issues?

#### Mario Carneiro (Jul 19 2018 at 09:28):

I think that's a good idea. I know Johannes has his own plans for this stuff, but I think a mathlib PR is the best place to coordinate

#### Patrick Massot (Jul 19 2018 at 09:31):

Ok, I'll try to do that today

#### Patrick Massot (Jul 19 2018 at 15:47):

https://github.com/leanprover/mathlib/pull/208

#### Nicholas Scheel (Jul 19 2018 at 16:22):

@Patrick Massot I’m curious if you could just define norm as dist 0? seems like you spend a lot of time converting between the two ...

#### Patrick Massot (Jul 19 2018 at 16:24):

I don't think you would get the expected properties

#### Nicholas Scheel (Jul 19 2018 at 16:26):

how so? you have lemma norm_dist { g : G} : dist g 0 = ∥g∥ already ... (plus commutativity gets you my definition)

#### Patrick Massot (Jul 19 2018 at 16:27):

I mean: there are distances on groups such that dist 0 is not a norm

#### Patrick Massot (Jul 19 2018 at 16:28):

Think of the trivial distance for instance

#### Patrick Massot (Jul 19 2018 at 16:28):

maybe this is not a good example actually

#### Nicholas Scheel (Jul 19 2018 at 16:29):

I think you need dist x y = dist 0 (x - y), as the equivalent of the property you already have, but I think norm adds nothing to the definition – it must be equal to dist 0

#### Patrick Massot (Jul 19 2018 at 16:29):

yes, somthing like this is needed

Last updated: May 11 2021 at 17:39 UTC