Commit 2022-03-12 18:01 e4ea2bca

feat(topology/algebra/continuous_monoid_hom): Define the Pontryagin dual (#12602) This PR adds the definition of the Pontryagin dual. We're still missing the locally compact instance. I thought I could get it from closed_embedding (to_continuous_map : continuous_monoid_hom A B → C(A, B)), but actually C(A, B) is almost never locally compact.