Basic Theorems About Bitvectors

This file contains theorems about bitvectors which can only be stated in Mathlib or downstream because they refer to other notions defined in Mathlib.

Please do not extend this file further: material about BitVec needed in downstream projects can either be PR'd to Lean, or kept downstream if it also relies on Mathlib.

theorem BitVec.ofFin_intCast {w : ℕ} (z : ℤ) : { toFin := ↑z } = ↑z

@[simp]

theorem BitVec.toFin_intCast {w : ℕ} (z : ℤ) : (↑z).toFin = ↑z

Injectivity

theorem BitVec.toNat_injective {n : ℕ} : Function.Injective BitVec.toNat

theorem BitVec.toFin_injective {n : ℕ} : Function.Injective toFin

Scalar Multiplication and Powers

theorem BitVec.toFin_nsmul {w : ℕ} (n : ℕ) (x : BitVec w) : (n • x).toFin = n • x.toFin

theorem BitVec.toFin_zsmul {w : ℕ} (z : ℤ) (x : BitVec w) : (z • x).toFin = z • x.toFin

theorem BitVec.toFin_pow {w : ℕ} (x : BitVec w) (n : ℕ) : (x ^ n).toFin = x.toFin ^ n

Ring

instance BitVec.instCommSemiring {w : ℕ} : CommSemiring (BitVec w)

Equations

• BitVec.instCommSemiring = Function.Injective.commSemiring BitVec.toFin ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance BitVec.instCommRing {w : ℕ} : CommRing (BitVec w)

Equations

• BitVec.instCommRing = Function.Injective.commRing BitVec.toFin ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def BitVec.equivFin {m : ℕ} : BitVec m ≃+* Fin (2 ^ m)

The ring BitVec m is isomorphic to Fin (2 ^ m).

Equations

• BitVec.equivFin = { toFun := fun (a : BitVec m) => a.toFin, invFun := fun (a : Fin (2 ^ m)) => { toFin := a }, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem BitVec.equivFin_apply {m : ℕ} (a : BitVec m) : equivFin a = a.toFin

@[simp]

theorem BitVec.equivFin_symm_apply_toFin {m : ℕ} (a : Fin (2 ^ m)) : (equivFin.symm a).toFin = a