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

A compact monoid has discrete Pontryagin dual.

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

@[implicit_reducible]

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

Equations

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