# 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)

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

## Equations

- ⋯ = ⋯