## 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.

#3169

#### 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: May 09 2021 at 10:11 UTC