Commit 2026-06-14 04:43 0c977638

feat(Topology/Algebra/PontryaginDual): prove compact monoids have discrete duals (#38669) Proves that the Pontryagin dual of a compact monoid is discrete. As a consequence, it also adds the corresponding finite-type instances for compact discrete monoids. This upstreams a result first added downstream in YaelDillies/APAP, where this fact was needed to close a sorry. The proof separates the trivial character from all the others using the right half of the circle and adds a few reusable Circle helper lemmas near the existing related API. The original APAP proof was AI-assisted and then reviewed/rewritten during downstream review. For this PR, I used Codex to help adapt the APAP proof to mathlib and to refactor the supporting lemmas.