Commit 2025-12-12 15:51 d0f64470

View on Github →

feat(RingTheory): the etale locus of an algebra (#32529)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Etale/Locus.lean

added theorem Algebra.IsEtaleAt.comp

added theorem Algebra.basicOpen_subset_etaleLocus_iff

added theorem Algebra.basicOpen_subset_etaleLocus_iff_etale

added def Algebra.etaleLocus

added theorem Algebra.etaleLocus_eq_compl_support

added theorem Algebra.etaleLocus_eq_univ_iff

added theorem Algebra.etaleLocus_eq_univ_iff_etale

added theorem Algebra.etaleLocus_eq_unramfiedLocus_inter_smoothLocus

added theorem Algebra.exists_etale_of_isEtaleAt

added theorem Algebra.isOpen_etaleLocus

added theorem Algebra.mem_etaleLocus_iff

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

added theorem Algebra.FinitePresentation.of_isLocalizationAway

Modified Mathlib/RingTheory/Unramified/Locus.lean