Zulip Chat Archive
Stream: maths
Topic: Second-to-Leading Coefficient
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.
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.
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?
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?
Johan Commelin (Jul 13 2020 at 18:45):
@Aaron Anderson I don't think that such a generalisation will make it easier to use.
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?)
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.
Johan Commelin (Jul 13 2020 at 18:57):
Ok, that's another example. Thanks!
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
Jalex Stark (Jul 13 2020 at 19:00):
how do I link to code on a branch of mathlib that is not a PR?
Johan Commelin (Jul 13 2020 at 19:00):
From the main page, you can select a branch in some dropdown menu
Johan Commelin (Jul 13 2020 at 19:01):
Johan Commelin (Jul 13 2020 at 19:01):
In the top left of that screen shot
Jalex Stark (Jul 13 2020 at 19:04):
we prove the lemma reid talks about here as monic.next_coeff_mul
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)
Aaron Anderson (Jul 14 2020 at 16:48):
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.)
Jalex Stark (Jul 14 2020 at 17:57):
splitting the file data/polynomial.lean?
Johan Commelin (Jul 14 2020 at 17:59):
Starting the new files before the refactor will make the split a lot harder
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
Jalex Stark (Jul 14 2020 at 18:00):
okay, i will switch over to that
Johan Commelin (Jul 14 2020 at 18:00):
I know that it is a lot less exciting than new stuff...
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.
Scott Morrison (Jul 15 2020 at 00:40):
And I agree that splitting the file first, then making changes, will be easier overall.
Scott Morrison (Jul 15 2020 at 00:40):
So I love the idea of someone trying to do that. :-)
Last updated: Dec 20 2023 at 11:08 UTC