Basic parity lemmas for the ring ℤ
#
See note [foundational algebra order theory].
Parity #
Equations
- x.instDecidablePredOdd = decidable_of_iff (¬Even x) ⋯
Alias of the reverse direction of Int.natAbs_even
.
Alias of the reverse direction of Int.natAbs_odd
.
@[simp]