The integers form a linear ordered ring

This file contains:

• instances on ℤ. The stronger one is Int.instLinearOrderedCommRing.
• basic lemmas about integers that involve order properties.

Recursors

• Int.rec: Sign disjunction. Something is true/defined on ℤ if it's true/defined for nonnegative and for negative values. (Defined in core Lean 3)
• Int.inductionOn: Simple growing induction on positive numbers, plus simple decreasing induction on negative numbers. Note that this recursor is currently only Prop-valued.
• Int.inductionOn': Simple growing induction for numbers greater than b, plus simple decreasing induction on numbers less than b.

instance Int.instLinearOrderedCommRing : LinearOrderedCommRing ℤ

Equations

• Int.instLinearOrderedCommRing = let __spread.0 := Int.instCommRing; let __spread.1 := Int.instLinearOrder; LinearOrderedCommRing.mk ⋯

Extra instances to short-circuit type class resolution

These also prevent non-computable instances being used to construct these instances non-computably.

instance Int.instOrderedCommRing : OrderedCommRing ℤ

Equations

• Int.instOrderedCommRing = StrictOrderedCommRing.toOrderedCommRing'

instance Int.instOrderedRing : OrderedRing ℤ

Equations

• Int.instOrderedRing = StrictOrderedRing.toOrderedRing'

Miscellaneous lemmas

theorem Int.isCompl_even_odd : IsCompl {n : ℤ | Even n} {n : ℤ | Odd n}

theorem Nat.cast_natAbs {α : Type u_1} [AddGroupWithOne α] (n : ℤ) : ↑n.natAbs = ↑|n|

theorem Int.cast_mul_eq_zsmul_cast {α : Type u_1} [AddCommGroupWithOne α] (m : ℤ) (n : ℤ) : ↑(m * n) = m • ↑n

Note this holds in marginally more generality than Int.cast_mul

theorem Int.two_le_iff_pos_of_even {m : ℤ} (even : Even m) : 2 ≤ m ↔ 0 < m

theorem Int.add_two_le_iff_lt_of_even_sub {m : ℤ} {n : ℤ} (even : Even (n - m)) : m + 2 ≤ n ↔ m < n

theorem bit0_mul {R : Type u_1} [NonUnitalNonAssocRing R] (n : R) (r : R) : bit0 n * r = 2 • (n * r)

theorem mul_bit0 {R : Type u_1} [NonUnitalNonAssocRing R] (n : R) (r : R) : r * bit0 n = 2 • (r * n)

theorem bit1_mul {R : Type u_1} [NonAssocRing R] (n : R) (r : R) : bit1 n * r = 2 • (n * r) + r

theorem mul_bit1 {R : Type u_1} [NonAssocRing R] {n : R} {r : R} : r * bit1 n = 2 • (r * n) + r