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.

Injectivity

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

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

Scalar Multiplication and Powers

Having instance of SMul ℕ, SMul ℤ and Pow are prerequisites for a CommRing instance

instance BitVec.instSMulNat {w : ℕ} : SMul ℕ (BitVec w)

Equations

• BitVec.instSMulNat = { smul := fun (x : ℕ) (y : BitVec w) => { toFin := x • y.toFin } }

instance BitVec.instSMulInt {w : ℕ} : SMul ℤ (BitVec w)

Equations

• BitVec.instSMulInt = { smul := fun (x : ℤ) (y : BitVec w) => { toFin := x • y.toFin } }

instance BitVec.instPowNat_mathlib {w : ℕ} : Pow (BitVec w) ℕ

Equations

• BitVec.instPowNat_mathlib = { pow := fun (x : BitVec w) (n : ℕ) => { toFin := x.toFin ^ n } }

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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯