Zulip Chat Archive

Stream: maths

Topic: polynomial


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 09:17):

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

view this post on Zulip Patrick Massot (Jul 19 2018 at 09:24):

That's really nice

view this post on Zulip Patrick Massot (Jul 19 2018 at 09:26):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 19 2018 at 09:31):

Ok, I'll try to do that today

view this post on Zulip Patrick Massot (Jul 19 2018 at 15:47):

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

view this post on Zulip 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 ...

view this post on Zulip Patrick Massot (Jul 19 2018 at 16:24):

I don't think you would get the expected properties

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Jul 19 2018 at 16:27):

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

view this post on Zulip Patrick Massot (Jul 19 2018 at 16:28):

Think of the trivial distance for instance

view this post on Zulip Patrick Massot (Jul 19 2018 at 16:28):

maybe this is not a good example actually

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 19 2018 at 16:29):

yes, somthing like this is needed


Last updated: May 11 2021 at 17:39 UTC