Commit 2024-02-20 23:51 3811e3e6

refactor: Split off the Pontryagin dual into separate file (#10620) This PR splits off the Pontryagin dual to a separate file to avoid unnecessary imports in ContinuousMonoidHom.lean. For instance, local compactness of the Pontryagin dual will require some heavy imports such as Arzela-Ascoli and the fact that the exponential map is a covering map.