Commit 2026-02-10 18:25 280b4e38

View on Github →

feat(RingTheory): etale local structure of quasi-finite algebras (#35036)

Estimated changes

Modified Mathlib/RingTheory/Etale/Basic.lean

Modified Mathlib/RingTheory/Etale/QuasiFinite.lean

modified theorem Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq

added theorem Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux

added theorem Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂

added theorem Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver

Modified Mathlib/RingTheory/Ideal/Over.lean

Modified Mathlib/RingTheory/Ideal/Prime.lean

added theorem Ideal.notMem_of_isUnit

Modified Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

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

added theorem IsLocalization.Away.algebraMap_surjective_of_isIdempotentElem

modified theorem IsLocalization.away_of_isIdempotentElem_of_mul

added theorem Localization.awayMap_awayMap_surjective