mathlib3
73402033 - feat(information_theory/hamming): add Hamming distance and norm (#14739)

Commit
3 years ago
feat(information_theory/hamming): add Hamming distance and norm (#14739) Add the Hamming distance, Hamming norm, and a `hamming` type synonym equipped with a normed group instance using the Hamming norm. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>
Parents
Loading