Commit 2025-07-03 00:36 38947713

View on Github →

feat(RingTheory/RingHom): etale ring homomorphisms (#26635)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RingHom/Etale.lean

added theorem RingHom.Etale.eq_formallyUnramified_and_smooth

added theorem RingHom.Etale.isStableUnderBaseChange

added theorem RingHom.Etale.ofLocalizationSpan

added theorem RingHom.Etale.ofLocalizationSpanTarget

added theorem RingHom.Etale.propertyIsLocal

added theorem RingHom.Etale.respectsIso

added theorem RingHom.Etale.stableUnderComposition

added theorem RingHom.Etale.toAlgebra

added def RingHom.Etale

added theorem RingHom.etale_algebraMap

added theorem RingHom.etale_iff_formallyUnramified_and_smooth