Zulip Chat Archive

Stream: maths

Topic: Second-to-Leading Coefficient


view this post on Zulip Aaron Anderson (Jul 13 2020 at 17:59):

In the branch mathlib:characteristic_polynomial_trace, @Jalex Stark and I have shown, among other things, that the trace of a matrix is the second-highest coefficient of the characteristic polynomial. While that exact statement is phrased in terms of the dimension of the matrix, the proof involves a function I call next_coeff.

view this post on Zulip Aaron Anderson (Jul 13 2020 at 18:01):

p.next_coeff is basically defined as p.coeff (p.nat_degree - 1), except I use ite to make it return 0 on constant polynomials.

view this post on Zulip Aaron Anderson (Jul 13 2020 at 18:02):

The whole thing seems like a reasonably common construction when doing elementary algebra with polynomials, but it's awkward to describe. Does anybody have any recommendations on how to make it more elegant?

view this post on Zulip Aaron Anderson (Jul 13 2020 at 18:03):

Perhaps it should all be done by embedding polynomials in add_monoid k Z and then using integer-indexed coefficients?

view this post on Zulip Johan Commelin (Jul 13 2020 at 18:45):

@Aaron Anderson I don't think that such a generalisation will make it easier to use.

view this post on Zulip Johan Commelin (Jul 13 2020 at 18:48):

In fact, I'm not yet convinced that we need this definition at all. The example that you've proven is a very clear use case. But apart from that, I don't know how often it will be used. Do you have other use cases in mind? (You mention "elementary algebra with polynomials" but are you thinking of something more specific?)

view this post on Zulip Reid Barton (Jul 13 2020 at 18:54):

I think it comes up reasonably frequently. For example, if you multiply monic polynomials, the next leading coefficients add. Sort of like a first derivative at infinity.

view this post on Zulip Johan Commelin (Jul 13 2020 at 18:57):

Ok, that's another example. Thanks!

view this post on Zulip Jalex Stark (Jul 13 2020 at 19:00):

I thought next_coeff was silly when Aaron showed it to me; the content of Reid's comment is what convinced me otherwise

view this post on Zulip Jalex Stark (Jul 13 2020 at 19:00):

how do I link to code on a branch of mathlib that is not a PR?

view this post on Zulip Johan Commelin (Jul 13 2020 at 19:00):

From the main page, you can select a branch in some dropdown menu

view this post on Zulip Johan Commelin (Jul 13 2020 at 19:01):

image.png

view this post on Zulip Johan Commelin (Jul 13 2020 at 19:01):

In the top left of that screen shot

view this post on Zulip Jalex Stark (Jul 13 2020 at 19:04):

we prove the lemma reid talks about here as monic.next_coeff_mul

view this post on Zulip Jalex Stark (Jul 13 2020 at 19:05):

(the proof right now is pretty terrible, this is I think the biggest reason this is not a PR yet)

view this post on Zulip Aaron Anderson (Jul 14 2020 at 16:48):

#3402

view this post on Zulip Johan Commelin (Jul 14 2020 at 17:56):

@Jalex Stark @Aaron Anderson I think it's a good idea to start a polynomial/ directory, and split the large file into pieces. You are kind of starting the new files already, without having done the split yet.
Could I ask you to also work on that refactor?
It would actually be best to do the refactor first. That way it becomes really easy to review. It should not add any new things. Only split the file into pieces, and start a bunch of new files. (It's still not completely trivial, you still need to move things around, probably.)

view this post on Zulip Jalex Stark (Jul 14 2020 at 17:57):

splitting the file data/polynomial.lean?

view this post on Zulip Johan Commelin (Jul 14 2020 at 17:59):

Starting the new files before the refactor will make the split a lot harder

view this post on Zulip Johan Commelin (Jul 14 2020 at 18:00):

Because then you need to combine the old and the new stuff. It will work, but as a reviewer it will be less trivial to see what's happening

view this post on Zulip Jalex Stark (Jul 14 2020 at 18:00):

okay, i will switch over to that

view this post on Zulip Johan Commelin (Jul 14 2020 at 18:00):

I know that it is a lot less exciting than new stuff...

view this post on Zulip Scott Morrison (Jul 15 2020 at 00:39):

I also have plans for improvements to data/polynomial.lean--- but I'm certainly not going to start until next week at least.

view this post on Zulip Scott Morrison (Jul 15 2020 at 00:40):

And I agree that splitting the file first, then making changes, will be easier overall.

view this post on Zulip Scott Morrison (Jul 15 2020 at 00:40):

So I love the idea of someone trying to do that. :-)


Last updated: May 06 2021 at 18:20 UTC