mathlib3

e4ea2bca - feat(topology/algebra/continuous_monoid_hom): Define the Pontryagin dual (#12602)

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.