Measurable space instance for additive characters

This file endows AddChar A M with the discrete measurable space structure whenever A and M are themselves discrete measurable spaces.

TODO

Give the definition in the correct generality.

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

Equations

• AddChar.instMeasurableSpace = ⊤

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

Equations

• ⋯ = ⋯