Commit 2024-10-17 02:58 b33faadf

View on Github →

chore(Topology/Group): move QuotientGroup to a new file (#17473)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

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

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

deleted theorem QuotientGroup.continuous_mk

deleted theorem QuotientGroup.continuous_smul₁

deleted theorem QuotientGroup.dense_image_mk

deleted theorem QuotientGroup.dense_preimage_mk

deleted theorem QuotientGroup.isClosedMap_coe

deleted theorem QuotientGroup.isOpenMap_coe

deleted theorem QuotientGroup.isOpenQuotientMap_mk

deleted theorem QuotientGroup.nhds_eq

deleted theorem QuotientGroup.nhds_one_isCountablyGenerated

deleted theorem QuotientGroup.quotientMap_mk

deleted theorem topologicalGroup_quotient

Created Mathlib/Topology/Algebra/Group/Quotient.lean

added theorem QuotientGroup.continuous_mk

added theorem QuotientGroup.continuous_smul₁

added theorem QuotientGroup.dense_image_mk

added theorem QuotientGroup.dense_preimage_mk

added theorem QuotientGroup.isClosedMap_coe

added theorem QuotientGroup.isOpenMap_coe

added theorem QuotientGroup.isOpenQuotientMap_mk

added theorem QuotientGroup.nhds_eq

added theorem QuotientGroup.nhds_one_isCountablyGenerated

added theorem QuotientGroup.quotientMap_mk

added theorem topologicalGroup_quotient

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

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

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

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

Modified Mathlib/Topology/Algebra/UniformGroup.lean

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

added theorem IsOpenQuotientMap.locallyCompactSpace

added theorem IsOpenQuotientMap.weaklyLocallyCompactSpace