feat(RingTheory/): MvPolynomial is standard smooth#39709

justus-springer wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

justus-springer:justus/MvPolynomial_smoothjustus-springer/mathlib4:justus/MvPolynomial_smoothCopy head branch name to clipboard