Theorem RingHom.Etale.ofLocalizationSpanTarget

Modification history

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