mathlib

1b42ac37 - refactor(information_theory/hamming): Separate Hamming norm and dist definitions. (#15820)

refactor(information_theory/hamming): Separate Hamming norm and dist definitions. (#15820) In practice, the current definition of the Hamming norm in terms of the dist leads to having to repeatedly invoke `pi.zero_apply`. This PR separates the two definitions and then proves their compatibility. We also improve a few style aspects to proofs while here, and add some simp lemmas. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>