Facts about ℤ as an (unbundled) ordered group

See note [foundational algebra order theory].

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.

theorem Int.natCast_strictMono : StrictMono fun (x : ℕ) => ↑x

@[deprecated Int.natCast_strictMono (since := "2024-05-25")]

theorem Int.coe_nat_strictMono : StrictMono fun (x : ℕ) => ↑x

Alias of Int.natCast_strictMono.

Miscellaneous lemmas

theorem Int.abs_eq_natAbs (a : ℤ) : |a| = ↑a.natAbs

@[simp]

theorem Int.natCast_natAbs (n : ℤ) : ↑n.natAbs = |n|

theorem Int.natAbs_abs (a : ℤ) : |a|.natAbs = a.natAbs

theorem Int.sign_mul_abs (a : ℤ) : a.sign * |a| = a

theorem Int.sign_mul_self_eq_abs (a : ℤ) : a.sign * a = |a|

theorem Int.natAbs_le_self_sq (a : ℤ) : ↑a.natAbs ≤ a ^ 2

theorem Int.natAbs_le_self_pow_two (a : ℤ) : ↑a.natAbs ≤ a ^ 2

Alias of Int.natAbs_le_self_sq.

theorem Int.le_self_sq (b : ℤ) : b ≤ b ^ 2

theorem Int.le_self_pow_two (b : ℤ) : b ≤ b ^ 2

Alias of Int.le_self_sq.

theorem Int.abs_natCast (n : ℕ) : |↑n| = ↑n

theorem Int.natAbs_sub_pos_iff {i j : ℤ} : 0 < (i - j).natAbs ↔ i ≠ j

theorem Int.natAbs_sub_ne_zero_iff {i j : ℤ} : (i - j).natAbs ≠ 0 ↔ i ≠ j

@[simp]

theorem Int.abs_lt_one_iff {a : ℤ} : |a| < 1 ↔ a = 0

theorem Int.abs_le_one_iff {a : ℤ} : |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1

theorem Int.one_le_abs {z : ℤ} (h₀ : z ≠ 0) : 1 ≤ |z|

theorem Int.eq_zero_of_abs_lt_dvd {m x : ℤ} (h1 : m ∣ x) (h2 : |x| < m) : x = 0

theorem Int.abs_sub_lt_of_lt_lt {m a b : ℕ} (ha : a < m) (hb : b < m) : |↑b - ↑a| < ↑m

/

theorem Int.ediv_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < |b|) : a / b = 0

mod

@[simp]

theorem Int.emod_abs (a b : ℤ) : a % |b| = a % b

theorem Int.emod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a % b < |b|

properties of / and %

theorem Int.abs_ediv_le_abs (a b : ℤ) : |a / b| ≤ |a|

theorem Int.abs_sign_of_nonzero {z : ℤ} (hz : z ≠ 0) : |z.sign| = 1

theorem Int.sign_eq_ediv_abs (a : ℤ) : a.sign = a / |a|

theorem Int.sign_eq_abs_ediv (a : ℤ) : a.sign = |a| / a

@[simp]

theorem zpow_abs_eq_one {G : Type u_1} [Group G] (a : G) (n : ℤ) : a ^ |n| = 1 ↔ a ^ n = 1

@[simp]

theorem abs_zsmul_eq_zero {G : Type u_1} [AddGroup G] (a : G) (n : ℤ) : |n| • a = 0 ↔ n • a = 0