Commit 2022-12-24 11:23 ece04ecb

View on Github →

feat: port Algebra.CharZero.Lemmas (#1164) There are some bit0 lemmas here which I'm not sure if I should delete or not.

Estimated changes

added theorem Nat.cast_div_charZero
added theorem Nat.cast_pow_eq_one
added theorem RingHom.charZero
added theorem RingHom.charZero_iff
added theorem RingHom.injective_nat
added theorem add_halves'
added theorem add_self_eq_zero
added theorem bit0_eq_bit0
added theorem bit0_eq_zero
added theorem bit0_injective
added theorem bit0_ne_zero
added theorem bit1_eq_bit1
added theorem bit1_eq_one
added theorem bit1_injective
added theorem eq_neg_self_iff
added theorem half_add_self
added theorem half_sub
added theorem nat_mul_inj'
added theorem nat_mul_inj
added theorem neg_eq_self_iff
added theorem one_eq_bit1
added theorem sub_half
added theorem zero_eq_bit0
added theorem zero_ne_bit0