Bitwise operations on integers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
int.bit_cases_on: Parity disjunction. Something is true/defined on
ℤ if it's true/defined for
even and for odd values.
Defines a function from
ℤ conditionally, if it is defined for odd and even integers separately