Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-17 08:18 9d7a6645

View on Github →

feat(algebra/parity + *): generalize lemmas about parity (#12761) I moved more even/odd lemmas from nat/int to general semirings/rings. Some files that explicitly used the nat/int namespace were changed along the way.

Estimated changes

added theorem add_monoid_hom.even
modified theorem even.add_even
modified theorem even.add_odd
added theorem even.mul_left
added theorem even.mul_right
added theorem even.pow_of_ne_zero
added theorem even.sub_even
added theorem even.sub_odd
added theorem even_neg_two
added theorem even_two
added theorem even_two_mul
added theorem even_zero
modified theorem odd.add_even
modified theorem odd.add_odd
added theorem odd.mul_odd
added theorem odd.pow
added theorem odd.sub_even
added theorem odd.sub_odd
added theorem odd_neg_one
added theorem odd_one
added theorem odd_two_mul_add_one
added theorem ring_hom.odd
deleted theorem int.even.mul_left
deleted theorem int.even.mul_right
deleted theorem int.even.sub_even
deleted theorem int.even.sub_odd
deleted theorem int.even_bit0
deleted theorem int.even_zero
deleted theorem int.odd.mul
deleted theorem int.odd.sub_even
deleted theorem int.odd.sub_odd
deleted theorem nat.even.mul_left
deleted theorem nat.even.mul_right
deleted theorem nat.even_bit0
deleted theorem nat.even_zero
deleted theorem nat.odd.mul