Measurable space instance for additive characters

This file endows AddChar A M with the discrete measurable space structure whenever A is a finite discrete measurable space.

TODO

Give the definition in the correct generality.

instance AddChar.instMeasurableSpace {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] [MeasurableSpace A] [DiscreteMeasurableSpace A] [Finite A] : MeasurableSpace (AddChar A M)

Equations

• AddChar.instMeasurableSpace = ⊤

instance AddChar.instDiscreteMeasurableSpace {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] [MeasurableSpace A] [DiscreteMeasurableSpace A] [Finite A] : DiscreteMeasurableSpace (AddChar A M)

Equations

• ⋯ = ⋯