Parity of integers #
This file contains theorems about the Even
and Odd
predicates on the integers.
Tags #
even, odd
Equations
- x.instDecidablePredEven = decidable_of_iff (x % 2 = 0) ⋯
Equations
- x.instDecidablePredOdd = decidable_of_iff (¬Even x) ⋯
IsSquare
can be decided on ℤ
by checking against the square root.
Equations
- m.instDecidablePredIsSquare = decidable_of_iff' (m.sqrt * m.sqrt = m) ⋯
Alias of the reverse direction of Int.natAbs_even
.
Alias of the reverse direction of Int.natAbs_odd
.