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 <58db46417c18ed5414020ce20e6ff4c1ce6ca8ed@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib