feat(MvPolynomial/Symmetric): the fundamental theorem

[alreadydone]

Proves that in a polynomial ring in n variables over a commutative ring, the subalgebra of symmetric polynomials is freely generated by the first n elementary symmetric polynomials. This is expressed as an isomorphism with the symmetric subalgebra with the polynomials in n variables, MvPolynomial.equiv_symmetricSubalgebra.

Moves Symmetric.lean (renamed to Defs.lean), NewtonIdentities.lean to a new Symmetric folder where the new FundamentalTheorem.lean file also lives.

---

• [x] depends on: #6625
• [ ] depends on: #7173
• [x] depends on: #7229

diff

[alreadydone]

Thanks but note that generalized maxDegree API is almost ready at https://github.com/leanprover-community/mathlib4/compare/supDegree_LinearOrder

[alreadydone]

~~Because the diff from #7229 is large, maybe it's not a good time to review ...~~ #7229 is now merged!

[Ruben-VandeVelde]

I'll push a fix for the build errors in a bit

[alreadydone]

Thanks! However, I was distracted by other projects and didn't finish the proposed change to the prerequisite PR #7173, so I'm not sure that fixing build errors at this time is particularly useful ...

[github-actions[bot]]

PR summary 1255f543dc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.MvPolynomial.NewtonIdentities	-918
Mathlib.RingTheory.MvPolynomial.Symmetric	-917
Mathlib.RingTheory.MvPolynomial.Symmetric.Defs	917
Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities	918
Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem	936

---

Declarations diff

+ IsSymmetric.antitone_supDegree + accumulate + accumulate_injective + accumulate_invAccumulate + accumulate_last + accumulate_rec + esymmAlgEquiv + esymmAlgHom + esymmAlgHomMonomial + esymmAlgHomMonomial_add + esymmAlgHomMonomial_single + esymmAlgHomMonomial_single_one + esymmAlgHom_apply + esymmAlgHom_fin_bijective + esymmAlgHom_fin_injective + esymmAlgHom_fin_surjective + esymmAlgHom_injective + esymmAlgHom_surjective + esymmAlgHom_zero + invAccumulate + isSymmetric_esymmAlgHomMonomial + leadingCoeff_esymmAlgHomMonomial + monic_esymm + rename_esymmAlgHom + supDegree_esymm + supDegree_esymmAlgHomMonomial

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#6625~~
• ~~leanprover-community/mathlib4#7173~~
• ~~leanprover-community/mathlib4#7229~~
• ~~leanprover-community/mathlib4#16630~~ By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks :tada:

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style