feat: BitVec.signExtend.{toNat, toInt}

[mhk119]

This PR adds toNat and toInt theorems for BitVec.signExtend.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6038 has successfully built against this PR. (2024-11-11 19:30:53) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 91c14c7ee912d3d9b86ad8655098bac67e919df7 --onto 4600bb16fcded0356d20ae232e7f8580c56a5955. (2024-11-19 20:42:10)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9cf83706e743debb47f3b1a48e1b92210c1c0720 --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-21 16:01:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 27cc0c80399f9f5ecebfdff65169d217a3045eea --onto 6d495586a1836da3e12efb4fbf9946bd9088ac5f. (2024-11-29 13:21:48)

[hargoniX]

Some minor remarks, I got two additional ones:

1. Could you rebase your branch on leanprover master? The test task IO flipper should be gone there.
2. Did you check that your theorem statements are in simp normal form?

[hargoniX]

The PR now just seems to consist of a change to code that is fine according to the style guide? What is the motivation here?

[mhk119]

The PR now just seems to consist of a change to code that is fine according to the style guide? What is the motivation here?

My bad, I didn't see that the theorems got merged into main in the meantime. Closing this :).

[tobiasgrosser]

It seems these got added in #6155 and #6157. In the future, we should cross-reference commits when someone decides to split them. Thank you @mhk119 for getting this in.