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 Nat.cast_natAbs {α : Type u_1} [AddGroupWithOne α] (n : ℤ) : ↑(Int.natAbs n) = ↑|n|

theorem Int.sign_add_eq_of_sign_eq {m : ℤ} {n : ℤ} : Int.sign m = Int.sign n → Int.sign (m + n) = Int.sign 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

properties of / and %

theorem Int.emod_two_eq_zero_or_one (n : ℤ) : n % 2 = 0 ∨ n % 2 = 1

dvd

theorem Int.exists_lt_and_lt_iff_not_dvd (m : ℤ) {n : ℤ} (hn : 0 < n) : (∃ (k : ℤ), n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m

If n > 0 then m is not divisible by n iff it is between n * k and n * (k + 1) for some k.

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