Commit 2024-07-17 18:39 8e49ce39

View on Github →

chore(Init/Data/Nat/Basic): drop lemmas about bit0/bit1 (#14762) Deletions:

nat.bit0_succ_eq
nat.zero_lt_bit0
nat.zero_lt_bit1
nat.bit0_ne_zero
nat.bit1_ne_zero

Estimated changes

Modified Mathlib/Data/Nat/Bits.lean

deleted theorem Nat.bit0_mod_two

deleted theorem Nat.bit1_mod_two

deleted theorem Nat.pos_of_bit0_pos

Modified Mathlib/Data/Nat/Size.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Init/Data/Nat/Basic.lean

Modified test/solve_by_elim/basic.lean