Commit 2024-04-08 18:56 d991fe8f

View on Github →

chore(RingTheory/Etale): split in multiple folders and files (#12017) Splits RingTheory/Etale.lean into 3 new separate folders for étale (resp. unramified, resp. smooth) morphisms.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Etale/Basic.lean

added theorem Algebra.FormallyEtale.comp

added theorem Algebra.FormallyEtale.iff_unramified_and_smooth

added theorem Algebra.FormallyEtale.localization_base

added theorem Algebra.FormallyEtale.localization_map

added theorem Algebra.FormallyEtale.of_equiv

added theorem Algebra.FormallyEtale.of_isLocalization

added theorem Algebra.FormallyEtale.of_unramified_and_smooth

Renamed Mathlib/RingTheory/Etale.lean to Mathlib/RingTheory/Smooth/Basic.lean

deleted theorem Algebra.FormallyEtale.comp

deleted theorem Algebra.FormallyEtale.iff_unramified_and_smooth

deleted theorem Algebra.FormallyEtale.localization_base

deleted theorem Algebra.FormallyEtale.localization_map

deleted theorem Algebra.FormallyEtale.of_equiv

deleted theorem Algebra.FormallyEtale.of_isLocalization

deleted theorem Algebra.FormallyEtale.of_unramified_and_smooth

deleted theorem Algebra.FormallyUnramified.comp

deleted theorem Algebra.FormallyUnramified.ext'

deleted theorem Algebra.FormallyUnramified.ext

deleted theorem Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential

deleted theorem Algebra.FormallyUnramified.lift_unique'

deleted theorem Algebra.FormallyUnramified.lift_unique

deleted theorem Algebra.FormallyUnramified.lift_unique_of_ringHom

deleted theorem Algebra.FormallyUnramified.localization_base

deleted theorem Algebra.FormallyUnramified.localization_map

deleted theorem Algebra.FormallyUnramified.of_comp

deleted theorem Algebra.FormallyUnramified.of_equiv

deleted theorem Algebra.FormallyUnramified.of_isLocalization

Created Mathlib/RingTheory/Unramified/Basic.lean

added theorem Algebra.FormallyUnramified.comp

added theorem Algebra.FormallyUnramified.ext'

added theorem Algebra.FormallyUnramified.ext

added theorem Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential

added theorem Algebra.FormallyUnramified.lift_unique'

added theorem Algebra.FormallyUnramified.lift_unique

added theorem Algebra.FormallyUnramified.lift_unique_of_ringHom

added theorem Algebra.FormallyUnramified.localization_base

added theorem Algebra.FormallyUnramified.localization_map

added theorem Algebra.FormallyUnramified.of_comp

added theorem Algebra.FormallyUnramified.of_equiv

added theorem Algebra.FormallyUnramified.of_isLocalization