Theorem StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot

Modification history

2025-11-20 14:55
Mathlib/RingTheory/Etale/StandardEtale.lean
feat(RingTheory/Etale): standard etale maps (#30867)
Added StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_botView on Github →