Theorem RingHom.FormallySmooth.holdsForLocalizationAway

Modification history

2025-05-28 12:51
Mathlib/RingTheory/RingHom/Smooth.lean
feat(RingHom): define `RingHom.Smooth` (#25107)
Added RingHom.FormallySmooth.holdsForLocalizationAwayView on Github →