Commit 2024-11-11 09:44 f3098a35

feat: Pontryagin duality for finite abelian groups (#15999) Prove Pontryagin duality in case of finite abelian groups. This states that any finite abelian group is canonically isomorphic to its double dual (the space of complex-valued characters of its space of complex-valued characters). We first prove it for ZMod n and then extend to all finite abelian groups using the Structure Theorem. From LeanAPAP Co-authored-by Bhavik Mehta bhavikmehta8@gmail.com