Commit 2024-07-13 02:04 edcb1f98

View on Github →

chore: remove unused lemmas about bit0/1 (#14678)

Estimated changes

deleted theorem bit0_eq_bit0
deleted theorem bit0_injective
deleted theorem bit1_eq_bit1
deleted theorem bit1_eq_one
deleted theorem bit1_injective
deleted theorem one_eq_bit1
deleted theorem Fin.mk_bit0
deleted theorem Fin.mk_bit1
deleted theorem Fin.val_bit0
deleted theorem Fin.val_bit1