Theorem ContinuousMonoidHom.locallyCompactSpace_of_hasBasis

Modification history

2025-02-05 09:23

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

chore(Topology/Algebra/ContinuousMonoidHom): do not depend on `ContinuousLinearMap` (#21443) …

Modified ContinuousMonoidHom.locallyCompactSpace_of_hasBasis View on Github →

2024-07-22 07:17

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

feat(Topology/Algebra/PontryaginDual): Local Compactness of the Pontryagin Dual (#11335) …

Added ContinuousMonoidHom.locallyCompactSpace_of_hasBasis View on Github →