Commit 2025-11-17 16:19 8da6dc5e

View on Github →

feat(RingTheory): miscellaneous lemmas about etale (#30857)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

Modified Mathlib/RingTheory/Etale/Basic.lean

added theorem Algebra.FormallyEtale.Algebra.FormallyEtale.iff_of_surjective

added theorem Algebra.FormallyEtale.Algebra.FormallyEtale.of_restrictScalars

modified theorem Algebra.FormallyEtale.comp

Modified Mathlib/RingTheory/RingHom/Unramified.lean

Modified Mathlib/RingTheory/Smooth/Basic.lean

added theorem Algebra.Extension.Algebra.FormallySmooth.iff_of_surjective

added theorem Algebra.Extension.Algebra.FormallySmooth.of_restrictScalars

Modified Mathlib/RingTheory/Unramified/Basic.lean

deleted theorem Algebra.FormallyUnramified.of_comp

added theorem Algebra.FormallyUnramified.of_restrictScalars

Modified Mathlib/RingTheory/Unramified/Field.lean

Modified Mathlib/RingTheory/Unramified/LocalRing.lean

Modified Mathlib/RingTheory/Unramified/Locus.lean