Theorem Algebra.IsUnramifiedAt.IsSmoothAt.exists_isStandardEtale_mvPolynomial

Modification history

2026-02-10 16:30
Mathlib/RingTheory/Unramified/LocalStructure.lean
feat(RingTheory): local structure of unramified algebras (#35023)
Added Algebra.IsUnramifiedAt.IsSmoothAt.exists_isStandardEtale_mvPolynomialView on Github →