Hamming spaces #
The Hamming metric counts the number of places two members of a (finite) Pi type differ. The Hamming norm is the same as the Hamming metric over additive groups, and counts the number of places a member of a (finite) Pi type differs from zero.
This is a useful notion in various applications, but in particular it is relevant in coding theory, in which it is fundamental for defining the minimum distance of a code.
Main definitions #
hammingDist x y: the Hamming distance between
y, the number of entries which differ.
hammingNorm x: the Hamming norm of
x, the number of non-zero entries.
Hamming β: a type synonym for
Π i, β iwith
normprovided by the above.
Hamming.ofHamming: functions for casting between
Π i, β i.
- the Hamming norm forms a normed group on
dist_smul with the discrete norm on
Instances inherited from normal Pi types.
API to/from the type synonym.