Commit 2025-05-28 12:51 730d9984

View on Github →

feat(RingHom): define RingHom.Smooth (#25107)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RingHom/Smooth.lean

added theorem RingHom.FormallySmooth.holdsForLocalizationAway

added theorem RingHom.FormallySmooth.isStableUnderBaseChange

added theorem RingHom.FormallySmooth.localizationPreserves

added theorem RingHom.FormallySmooth.respectsIso

added theorem RingHom.FormallySmooth.stableUnderComposition

added theorem RingHom.FormallySmooth.toAlgebra

added def RingHom.FormallySmooth

added theorem RingHom.Smooth.comp

added theorem RingHom.Smooth.holdsForLocalizationAway

added theorem RingHom.Smooth.id

added theorem RingHom.Smooth.isStableUnderBaseChange

added theorem RingHom.Smooth.ofLocalizationSpanTarget

added theorem RingHom.Smooth.propertyIsLocal

added theorem RingHom.Smooth.stableUnderComposition

added theorem RingHom.Smooth.toAlgebra

added def RingHom.Smooth

added theorem RingHom.formallySmooth_algebraMap

added theorem RingHom.smooth_algebraMap

added theorem RingHom.smooth_def

Modified Mathlib/RingTheory/Smooth/Basic.lean