Why do we use prime numbers in applications of `mixHash`?

Stream: general

[l1mey]

Searching for the uses of mixHash I find that chained mixHash calls use prime numbers to distinguish each enum case. Why is that? It this a choice due to the underlying implementation of mixHash ?

-- Lean/Meta/LazyDiscrTree.lean
/-- Hash function -/
protected def hash : Key → UInt64
  | .const n a   => mixHash 5237 $ mixHash n.hash (hash a)
  | .fvar n a    => mixHash 3541 $ mixHash (hash n) (hash a)
  | .lit v       => mixHash 1879 $ hash v
  | .star        => 7883
  | .other       => 2411
  | .arrow       => 17
  | .proj s i a  =>  mixHash (hash a) $ mixHash (hash s) (hash i)

-- Lean/Expr.lean
  ...
with
  @[computed_field, extern "lean_expr_data"]
  data : @& Expr → Data
    | .const n lvls => mkData (mixHash 5 <| mixHash (hash n) (hash lvls)) 0 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
    | .bvar idx => mkData (mixHash 7 <| hash idx) (idx+1)
    | .sort lvl => mkData (mixHash 11 <| hash lvl) 0 0 false false lvl.hasMVar lvl.hasParam
    | .fvar fvarId => mkData (mixHash 13 <| hash fvarId) 0 0 true
    | .mvar fvarId => mkData (mixHash 17 <| hash fvarId) 0 0 false true
    | .mdata _m e =>

[Aaron Liu]

maybe because the prime numbers are all coprime to each other

[Aaron Liu]

or maybe it's arbitrary

[Aaron Liu]

I think I found the mixhash function at https://github.com/leanprover/lean4/blob/7d55c033e1f0ad8cb7c2b9ab72e5db40ce192222/src/runtime/object.cpp#L1714-L1716

[Damiano Testa]

This may be completely unrelated, but googling hash and prime numbers yields

https://www.designgurus.io/answers/detail/why-should-hash-functions-use-a-prime-number-modulus

that superficially looks relevant!