Theorem QuotientRing.isOpenMap_coe

Modification history

2024-10-03 16:01
Mathlib/Topology/Algebra/Ring/Ideal.lean
feat(Topology/Group): drop an unneeded assumption (#16551) …
Modified QuotientRing.isOpenMap_coeView on Github →
2023-03-09 18:34
Mathlib/Topology/Algebra/Ring/Ideal.lean
feat: port Topology.Algebra.Ring.Ideal (#2754)
Added QuotientRing.isOpenMap_coeView on Github →