[Merged by Bors] - feat(RingTheory/Smooth/Basic): add Generators.mvPolynomial#39708

justus-springer wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

justus-springer:justus/Generators.mvPolynomialjustus-springer/mathlib4:justus/Generators.mvPolynomialCopy head branch name to clipboard