Commit 2024-10-24 16:27 201aff36

View on Github →

feat(Algebra/CharP/Two): more lemmas on char two (#17483)

Estimated changes

Modified Mathlib/Algebra/CharP/Two.lean

added theorem CharTwo.add_eq_iff_eq_add

added theorem CharTwo.eq_add_iff_add_eq

added theorem CharTwo.of_one_ne_zero_of_two_eq_zero

modified theorem CharTwo.sub_eq_add'

modified theorem CharTwo.two_eq_zero

Modified Mathlib/Algebra/Ring/Parity.lean

added theorem Nat.odd_add_one

added theorem natCast_eq_one_of_odd_of_two_eq_zero

added theorem natCast_eq_zero_of_even_of_two_eq_zero

added theorem natCast_eq_zero_or_one_of_two_eq_zero