feat: show basic properties of BitVec multiplication

[alexkeizer]

Show that multiplication of bitvectors is associative and commutative, and show that it has 1#w as identity (both on the left and right).

[alexkeizer]

awaiting-review

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 263629d140c42be6d553091a17b584ce766d9645 --onto 8b8e001794e6a8b481d37f24fa77bb07797682a1. (2024-02-21 21:42:02)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6e821de11abd3c16dbbeb15cbfe315e2abbef10a --onto 6719af350fde9339354f28d091458df39a4af9d4. (2024-02-21 22:17:51)

[alexkeizer]

@joehendrix I'd like your opinion on this PR: we're proving commutativity and associativity of bitvector multiplication by appealing to these properties of Fin multiplication. But, not in a way that relies on the definition of BitVec.mul being Fin.mul. Instead, we use the toFin_mul lemma, so this proof still works after #3430.

Is this an acceptable level of coupling between BitVec and Fin, since it's just an implementation detail of the proof, or would you prefer we stay away from Fin entirely?

[joehendrix]

@alexkeizer Looks good to me. I have no concerns with relying on Fin in lemmas when it is useful.