Commit 2026-02-10 16:30 672ea226

View on Github →

feat(RingTheory): local structure of unramified algebras (#35023)

Estimated changes

Modified Mathlib/RingTheory/Localization/Away/AdjoinRoot.lean

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

added theorem Localization.awayMap_bijective_of_dvd

added theorem Localization.awayMap_injective_of_dvd

added theorem Localization.awayMap_surjective_of_dvd

Modified Mathlib/RingTheory/Unramified/LocalStructure.lean

added theorem Algebra.IsUnramifiedAt.IsEtaleAt.exists_isStandardEtale

added theorem Algebra.IsUnramifiedAt.IsSmoothAt.exists_isStandardEtale_mvPolynomial

deleted theorem Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionAt_of_finite

added theorem Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn

deleted theorem Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top