polynomial

Stream: maths

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

That's really nice

[Patrick Massot]

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

[Patrick Massot]

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]

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]

Ok, I'll try to do that today

[Patrick Massot]

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

[Nicholas Scheel]

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

I don't think you would get the expected properties

[Nicholas Scheel]

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

[Patrick Massot]

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

[Patrick Massot]

Think of the trivial distance for instance

[Patrick Massot]

maybe this is not a good example actually

[Nicholas Scheel]

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]

yes, somthing like this is needed