Commit 2023-03-09 18:34 057deeb6

View on Github →

feat: port Topology.Algebra.Ring.Ideal (#2754)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Ring/Ideal.lean

added theorem Ideal.closure_eq_of_isClosed

added theorem Ideal.coe_closure

added theorem QuotientRing.isOpenMap_coe

added theorem QuotientRing.quotientMap_coe_coe