feat: expand relationship with BitVec and toFin

[tobiasgrosser]

No description provided.

[tobiasgrosser]

This is an ongoing branch to upstream https://github.com/opencompl/lean-mlir/blob/main/SSA/Projects/InstCombine/ForMathlib.lean to unblock #5323, which would benefit from a CommRing instance for BitVec in mathlib:

instance : CommRing (BitVec w) :=
  toFin_injective.commRing _
    toFin_zero toFin_one toFin_add toFin_mul toFin_neg toFin_sub
    toFin_nsmul toFin_zsmul toFin_pow toFin_natCast toFin_intCast

I am now off for weekend tasks, but started this already a bit.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-10-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-10-13 05:20:23)