toBitVec_intCast — Mathlib

English

The bit-vector of an integer cast to USize equals the integer itself represented as a bit-vector.

Русский

Битовый вектор целого, приведённого к USize, равен самому целому, представленному как битовый вектор.

LaTeX

$$$\forall z\in\mathbb{Z},\; (z:\mathrm{USize}).\operatorname{toBitVec} = z$$$

Lean4

@[simp, int_toBitVec]
protected theorem toBitVec_intCast (z : ℤ) : (z : USize).toBitVec = z :=
  by
  obtain ⟨z, rfl | rfl⟩ := z.eq_nat_or_neg
  · erw [intCast_ofNat]; rfl
  · rw [intCast_neg, toBitVec_neg]
    erw [intCast_ofNat]
    simp

Похожие утверждения