instance PontryaginDual.instDiscreteTopologyOfCompactSpace_leanAPAP {M : Type u_1} [Monoid M] [TopologicalSpace M] [CompactSpace M] : DiscreteTopology (PontryaginDual M)

A compact monoid has discrete Pontryagin dual.

instance PontryaginDual.instFiniteOfDiscreteTopologyOfCompactSpace_leanAPAP {M : Type u_1} [Monoid M] [TopologicalSpace M] [DiscreteTopology M] [CompactSpace M] : Finite (PontryaginDual M)

noncomputable instance PontryaginDual.instFintypeOfDiscreteTopologyOfCompactSpace_leanAPAP {M : Type u_1} [Monoid M] [TopologicalSpace M] [DiscreteTopology M] [CompactSpace M] : Fintype (PontryaginDual M)

Equations

• PontryaginDual.instFintypeOfDiscreteTopologyOfCompactSpace_leanAPAP = Fintype.ofFinite (PontryaginDual M)