Theorem RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial

Modification history

2026-01-23 08:04
Mathlib/RingTheory/RingHom/StandardSmooth.lean
feat(RingTheory): standard smooth = etale over mvpolynomial (#33555)
Added RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomialView on Github →