@[simp]

theorem BitVec.ofFin_neg : ∀ {a : ℕ} {x : Fin (2 ^ a)}, { toFin := -x } = -{ toFin := x }

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

@[simp]

theorem BitVec.ofFin_natCast {w : ℕ} (n : ℕ) : { toFin := ↑n } = ↑n

theorem BitVec.toFin_natCast {w : ℕ} (n : ℕ) : (↑n).toFin = ↑n

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

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

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

Equations

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

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

Equations

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

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

Equations

• BitVec.instPowNat_sSA = { 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

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

Equations

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