Commit 2025-02-05 09:23 0636ded8

View on Github →

chore(Topology/Algebra/ContinuousMonoidHom): do not depend on ContinuousLinearMap (#21443) The dependency should go in the other direction.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

deleted def ContinuousMonoidHom.compLeft

deleted def ContinuousMonoidHom.compRight

deleted theorem ContinuousMonoidHom.continuous_comp

deleted theorem ContinuousMonoidHom.continuous_comp_left

deleted theorem ContinuousMonoidHom.continuous_comp_right

deleted theorem ContinuousMonoidHom.continuous_of_continuous_uncurry

deleted theorem ContinuousMonoidHom.isClosedEmbedding_toContinuousMap

deleted theorem ContinuousMonoidHom.isEmbedding_toContinuousMap

deleted theorem ContinuousMonoidHom.isInducing_toContinuousMap

deleted theorem ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt

deleted theorem ContinuousMonoidHom.locallyCompactSpace_of_hasBasis

deleted theorem ContinuousMonoidHom.range_toContinuousMap

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

added def ContinuousMonoidHom.compLeft

added def ContinuousMonoidHom.compRight

added theorem ContinuousMonoidHom.continuous_comp

added theorem ContinuousMonoidHom.continuous_comp_left

added theorem ContinuousMonoidHom.continuous_comp_right

added theorem ContinuousMonoidHom.continuous_of_continuous_uncurry

added theorem ContinuousMonoidHom.isClosedEmbedding_toContinuousMap

added theorem ContinuousMonoidHom.isEmbedding_toContinuousMap

added theorem ContinuousMonoidHom.isInducing_toContinuousMap

added theorem ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt

added theorem ContinuousMonoidHom.locallyCompactSpace_of_hasBasis

added theorem ContinuousMonoidHom.range_toContinuousMap

Modified Mathlib/Topology/Algebra/PontryaginDual.lean