Theorem: UInt.toNat_of_length_eq_zero (Algdata/Classes/UInt.lean)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
h : length α = 0
a : α
⊢ toNat a = toNat (OfNat.ofNat (toNat a))
Tactic:
rw [UInt.ofNat_toNat]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
h : length α = 0
a : α
⊢ toNat a % 2 ^ length α = toNat a % 1
Tactic:
rw [h, Nat.pow_zero]
State after:
no goals