Commit 2025-08-04 10:55 6dad0cda
View on Github →fix(Data/BitVec): remove a SMul instance diamond (#27581)
When the Nat- and Int-action typeclasses and their instances were upstreamed, they changed to a different (and worse) defeq.
This removes the mathlib instances and proves the old defeq still holds propositionally.
Also move some theorems out of the BitVec file that are not about BitVec at all, and are about Fin.