Commit 2026-01-23 08:04 294c3b30

View on Github →

feat(RingTheory): standard smooth = etale over mvpolynomial (#33555)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

added theorem MvPolynomial.iterToSum_sumToIter

added theorem MvPolynomial.sumToIter_iterToSum

Modified Mathlib/Algebra/MvPolynomial/PDeriv.lean

added theorem MvPolynomial.pderiv_sumToIter

Modified Mathlib/RingTheory/RingHom/StandardSmooth.lean

added theorem Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial

added theorem RingHom.IsStandardSmooth.exists_etale_mvPolynomial

added theorem RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial