Commit 2025-05-23 05:27 b27d4790

View on Github →

feat: a discrete monoid has compact Pontryagin dual (#23923) From LeanAPAP

Estimated changes

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

added theorem ContinuousMonoidHom.isClosedEmbedding_coe

Modified Mathlib/Topology/Algebra/PontryaginDual.lean

Modified Mathlib/Topology/CompactOpen.lean

added theorem ContinuousMap.coe_homeoFnOfDiscrete

added def ContinuousMap.homeoFnOfDiscrete

added theorem ContinuousMap.homeoFnOfDiscrete_symm_apply

added theorem ContinuousMap.isHomeomorph_coe

Modified Mathlib/Topology/ContinuousMap/Basic.lean

added theorem ContinuousMap.coe_equivFnOfDiscrete

modified def ContinuousMap.equivFnOfDiscrete

added theorem ContinuousMap.equivFnOfDiscrete_symm_apply

Modified Mathlib/Topology/Separation/NotNormal.lean