Zulip Chat Archive
Stream: maths
Topic: symmetric polynomials
Johan Commelin (Jun 25 2020 at 09:37):
I have a draft of homogeneous and symmetric polynomials on the symm-poly branch. I have almost no time for lean at the moment :sad: :cry: :sad:
If someone likes this and doesn't know what to do... feel free to work on it. I'll open it as a draft PR right now.
Johan Commelin (Jun 25 2020 at 09:39):
Aaron Anderson (Jun 26 2020 at 23:39):
I'm cleaning up a few loose ends, but I'm not sure if I'll finish it
Aaron Anderson (Jun 27 2020 at 00:04):
mmm probably not finishing it, but I closed a few sorries and I'll think for a little bit as to whether this lets us state and prove all of Vieta's formulas
Scott Morrison (Jun 27 2020 at 00:11):
Can it be split into two PRs?
Johan Commelin (Jun 27 2020 at 05:15):
@Aaron Anderson We usually try to keep PRs around < ~250 lines, and ~500 lines is a big PR. So I think homogeneous could allready be a standalone PR, and the symmetric file will probably be 3 PRs once it's ready.
Johan Commelin (Jun 27 2020 at 05:19):
By the way, thanks for looking at these!
Johan Commelin (Jun 27 2020 at 05:24):
My main goals was to show that every symmetric polynomial is a polynomial in the elementary symmetric polynomials.
Aaron Anderson (Jun 27 2020 at 05:24):
The first >900 lines of symmetric.lean are sorry-free, so probably some of those sub-PRs could start happening
Johan Commelin (Jun 27 2020 at 05:25):
Everything marked with --move this could be a "prerequisites" PR of ~ 100 lines to something like 5 existing files in mathlib
Johan Commelin (Jun 27 2020 at 05:26):
Reviewing 10 small changes to 10 files is often a lot easier if you are not responsible for also reviewing a 500 line new file
Aaron Anderson (Jun 27 2020 at 05:39):
I think I can fix one more sorry tomorrow, but other than that I’m in over my head
Johan Commelin (Jun 29 2020 at 06:51):
@Aaron Anderson I PR'd homogeneous polynomials #3223
Last updated: Dec 20 2023 at 11:08 UTC