Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-06 12:41 99e308d3

View on Github →

chore(parity): even and odd in semiring (#4473) Replaces the ad-hoc nat.even, nat.odd, int.even and int.odd by definitions that make sense in semirings and get that odd can be rintros/rcases'ed. This requires almost no change except that even is not longer usable as a dot notation (which I see as a feature since I find even n to be more readable than n.even).

Estimated changes

added def even
added theorem even_iff_two_dvd
added def odd
modified theorem convex_on_pow_of_even
modified theorem int_prod_range_nonneg
deleted def int.even
modified theorem int.even_add
modified theorem int.even_bit0
modified theorem int.even_coe_nat
modified theorem int.even_iff
modified theorem int.even_mul
modified theorem int.even_neg
modified theorem int.even_pow
modified theorem int.even_sub
modified theorem int.even_zero
modified theorem int.mod_two_ne_one
modified theorem int.mod_two_ne_zero
modified theorem int.not_even_bit1
modified theorem int.not_even_one
deleted def int.odd
deleted theorem int.odd_def
added theorem int.odd_iff
added theorem int.odd_iff_not_even
modified theorem int.two_dvd_ne_zero
modified theorem nat.even.add
modified theorem nat.even.sub
deleted def nat.even
modified theorem nat.even_add
modified theorem nat.even_bit0
modified theorem nat.even_iff
modified theorem nat.even_mul
modified theorem nat.even_pow
modified theorem nat.even_sub
modified theorem nat.even_succ
modified theorem nat.mod_two_ne_one
modified theorem nat.mod_two_ne_zero
modified theorem nat.not_even_bit1
deleted def nat.odd
deleted theorem nat.odd_def
added theorem nat.odd_iff
added theorem nat.odd_iff_not_even