Skip to content

Commit

Permalink
Update src/Init/Data/BitVec/Lemmas.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Luisa Cicolini <[email protected]>
Co-authored-by: Siddharth <[email protected]>
  • Loading branch information
3 people committed Feb 26, 2025
1 parent c1f2af3 commit b42e538
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Data/BitVec/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3718,7 +3718,7 @@ theorem toNat_twoPow_of_le {i w : Nat} (h : w ≤ i) : (twoPow w i).toNat = 0 :=
apply Nat.mod_eq_zero_of_dvd
exact Nat.pow_dvd_pow_iff_le_right'.mpr h

theorem toNat_twoPow_of_lt {i w : Nat} (h : i < w ): (twoPow w i).toNat = 2^i := by
theorem toNat_twoPow_of_lt {i w : Nat} (h : i < w ) : (twoPow w i).toNat = 2^i := by
rw [toNat_twoPow]
apply Nat.mod_eq_of_lt
apply Nat.pow_lt_pow_of_lt (by omega) (by omega)
Expand Down

0 comments on commit b42e538

Please sign in to comment.