Theorem RingHom.Etale.propertyIsLocal

Modification history

2025-07-03 00:36

Mathlib/RingTheory/RingHom/Etale.lean

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

Added RingHom.Etale.propertyIsLocal View on Github →