Commit 2024-10-03 16:01 e58fb43f

View on Github →

feat(Topology/Group): drop an unneeded assumption (#16551)

prove that the quotient map G → G ⧸ N is an open quotient map;
use recently added lemmas to drop a [LocallyCompactSpace G] assumption in QuotientGroup.continuousSMul (now called QuotientGroup.instContinuousSMul).

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

added theorem MulAction.isOpenQuotientMap_quotientMk

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem QuotientGroup.continuous_mk

modified theorem QuotientGroup.isOpenMap_coe

added theorem QuotientGroup.isOpenQuotientMap_mk

Modified Mathlib/Topology/Algebra/Group/Compact.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

modified theorem Submodule.isOpenMap_mkQ

added theorem Submodule.isOpenQuotientMap_mkQ

Modified Mathlib/Topology/Algebra/ProperAction.lean

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

modified theorem QuotientRing.isOpenMap_coe

added theorem QuotientRing.isOpenQuotientMap_mk

Modified Mathlib/Topology/Maps/OpenQuotient.lean

added theorem IsOpenQuotientMap.dense_preimage_iff