Theorem RingHom.Etale.eq_formallyUnramified_and_smooth

Modification history

2025-07-03 00:36
Mathlib/RingTheory/RingHom/Etale.lean
feat(RingTheory/RingHom): etale ring homomorphisms (#26635)
Added RingHom.Etale.eq_formallyUnramified_and_smoothView on Github →