Commit 2021-02-02 14:43 fc7daa36

View on Github →

feat(data/nat/parity): addition/subtraction of even/odd nats (#5934) Added various theorems pertaining to the addition and subtraction of even and odd natural numbers.

Estimated changes

Modified src/analysis/convex/specific_functions.lean

Modified src/data/nat/parity.lean

deleted theorem nat.even.add

added theorem nat.even.add_even

added theorem nat.even.add_odd

deleted theorem nat.even.sub

added theorem nat.even.sub_even

added theorem nat.even.sub_odd

added theorem nat.even_add'

modified theorem nat.even_div

added theorem nat.even_sub'

modified theorem nat.neg_one_pow_eq_one_iff_even

added theorem nat.odd.add_even

added theorem nat.odd.add_odd

added theorem nat.odd.sub_even

added theorem nat.odd.sub_odd

added theorem nat.odd_add'

added theorem nat.odd_add

added theorem nat.odd_sub'

added theorem nat.odd_sub

modified theorem nat.two_not_dvd_two_mul_add_one

modified theorem nat.two_not_dvd_two_mul_sub_one