Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-13 16:25 0eea0d9f

View on Github →

feat(data/{nat,int}/parity): the 'even' predicate on nat and int (#1219)

  • feat(data/{nat,int}/parity): the 'even' predicate on nat and int
  • fix(data/{nat,int}/parity): shorten proof
  • delete extra comma

Estimated changes

added def int.even
added theorem int.even_add
added theorem int.even_bit0
added theorem int.even_coe_nat
added theorem int.even_iff
added theorem int.even_mul
added theorem int.even_pow
added theorem int.even_sub
added theorem int.even_zero
added theorem int.mod_two_ne_one
added theorem int.mod_two_ne_zero
added theorem int.not_even_bit1
added theorem int.not_even_one
added def nat.even
added theorem nat.even_add
added theorem nat.even_bit0
added theorem nat.even_iff
added theorem nat.even_mul
added theorem nat.even_pow
added theorem nat.even_sub
added theorem nat.even_succ
added theorem nat.even_zero
added theorem nat.mod_two_ne_one
added theorem nat.mod_two_ne_zero
added theorem nat.not_even_bit1
added theorem nat.not_even_one