-rw-r--r-- 287 leangoppa-20230726/Goppadecoding/hamming.lean raw
import Mathlib.Tactic
import Mathlib.Data.Finset.Basic

namespace Goppadecoding

section hamming

variable {k: Type _} [Field k] [DecidableEq k]
variable {U: Type _} [DecidableEq U]

def hamming_weight (α: U → k) (S: Finset U) :=
  (S.filter (fun s ↦ α s ≠ 0)).card

end hamming