[WIP] feat(linear_algebra/univariate_polynomial) Create univariate_po…

[ChrisHughes24]

Mostly finished theory of univariate polynomials, including division algorithm.
@johoelzl I know you were planning on doing this. Would you rather use this or do it yourself?
If you want to use this, then I'll neaten it up.

[ChrisHughes24]

There are a couple of points for discussion. Basically, what's the best definition of degree and the Euclidean valuation. I used the standard degree definition, and my euclidean valuation was 0 for p = 0 and degree p + 1 for p ≠ 0. The main downside to the definition of degree is that when doing induction on degree, the base case is much harder to prove. I may well go back and use euclid_val_poly instead of degree for the division algorithm to simplify the proofs.

[semorrison]

Looks good! I wouldn't have filed this under "linear_algebra", however. "algebra" perhaps? A whole folder dedicated to various types of polynomials?

…

On Fri, Jun 29, 2018 at 3:04 AM Chris Hughes ***@***.***> wrote: There are a couple of points for discussion. Basically, what's the best definition of degree and the Euclidean valuation. I used the standard degree definition, and my euclidean valuation was 0 for p = 0 and degree p + 1 for p ≠ 0. The main downside to the definition of degree is that when doing induction on degree, the base case is much harder to prove. I may well go back and use euclid_val_poly instead of degree for the division algorithm to simplify the proofs. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#171 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBOYzvdL4H1FeVpAK1oUrpmLjhUfHks5uBQx5gaJpZM4U7nK8> .

[ChrisHughes24]

I think ring_theory probably makes the most sense.

[jcommelin]

I think you should just use degree for your euclidean valuation. Currently the definition of euclidean domain is wrong: https://github.com/leanprover/mathlib/blob/master/algebra/euclidean_domain.lean#L20 should assume that remainder is nonzero, before demanding the inequality.

[digama0]

I agree that degree should be consistent with valuation, but another option is with_bot nat, which makes it possible to set the degree to minus infinity while still being able to do addition and compare etc.

[ChrisHughes24]

I think with_bot nat makes the most sense. If anyone ever wants to induct on degree, then they'll have zero as the base case instead of constants, which is quite a lot easier, and they'll need the full range of inequality lemmas in order to do so.

[ChrisHughes24]

I changed it to make degree with_bot nat. This still requires a change in the definition of a Euclidean domain, probably to take an arbitrary well founded relation. I think the definition nat_degree, which has degree 0 = (0 : nat) is still needed however, and I'm not sure whether to prove every lemma about degree for nat_degree as well.

[johoelzl]

@dorhinj I will use your theory and merge it with Jens and my development.

[johoelzl]

Hm, the merge went quiet wrong in your recent commits, there are a lot of merge conflict markers: >>>>> ==== <<<< etc.

Do you want to continue this PR, or start a new one to prove that polynomials form an Euclidean domain? Also, note: I removed monomial, to put the focus on X and C.

[ChrisHughes24]

I'll definitely start a new one for that. I am going to have to think about how to change the definition of Euclidean domain to work.