Theorem QuotientRing.isOpenQuotientMap_mk

Modification history

2024-10-03 16:01
Mathlib/Topology/Algebra/Ring/Ideal.lean
feat(Topology/Group): drop an unneeded assumption (#16551) …
Added QuotientRing.isOpenQuotientMap_mkView on Github →