Commit 2023-07-10 04:23 888c4095

View on Github →

feat: port RingTheory.Etale (#5781)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Etale.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

added theorem Algebra.FormallySmooth.comp

added theorem Algebra.FormallySmooth.comp_lift

added theorem Algebra.FormallySmooth.comp_liftOfSurjective

added theorem Algebra.FormallySmooth.exists_lift

added theorem Algebra.FormallySmooth.iff_split_surjection

added theorem Algebra.FormallySmooth.liftOfSurjective_apply

added theorem Algebra.FormallySmooth.localization_base

added theorem Algebra.FormallySmooth.localization_map

added theorem Algebra.FormallySmooth.mk_lift

added theorem Algebra.FormallySmooth.of_equiv

added theorem Algebra.FormallySmooth.of_isLocalization

added theorem Algebra.FormallySmooth.of_split

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

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

added theorem AlgHom.ker_kerSquareLift

deleted theorem AlgHom.ker_ker_sqare_lift