Commit 2024-10-26 17:00 2834fd21

View on Github →

refactor(RingTheory/Unramified): Switch official definition to allow general universes (#15135) Under this new definition, Algebra.FormallySmooth is only defined for commutative rings.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Etale/Basic.lean

Modified Mathlib/RingTheory/Etale/Field.lean

Modified Mathlib/RingTheory/Unramified/Basic.lean

added theorem Algebra.FormallyUnramified.comp_injective

modified theorem Algebra.FormallyUnramified.ext'

added theorem Algebra.FormallyUnramified.iff_comp_injective

modified theorem Algebra.FormallyUnramified.lift_unique'

modified theorem Algebra.FormallyUnramified.lift_unique

modified theorem Algebra.FormallyUnramified.lift_unique_of_ringHom

Deleted Mathlib/RingTheory/Unramified/Derivations.lean

deleted theorem Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential

Modified Mathlib/RingTheory/Unramified/Field.lean

modified theorem Algebra.FormallyUnramified.iff_isSeparable

Modified Mathlib/RingTheory/Unramified/Finite.lean

Modified Mathlib/RingTheory/Unramified/Pi.lean