Mathlib.Algebra.Order.Group.Unbundled.Int

Module docstring

{"# 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. ","### Miscellaneous lemmas ","#### / ","#### mod ","### properties of / and % "}

Int.natCast_strictMono theorem

: StrictMono (· : ℕ → ℤ)

Full source

theorem natCast_strictMono : StrictMono (· : ℕ → ℤ) := fun _ _ ↦ Int.ofNat_lt.2

Strict Monotonicity of the Natural Number to Integer Embedding

Informal description

The canonical embedding from the natural numbers to the integers, given by the coercion function `(· : ℕ → ℤ)`, is strictly monotone. That is, for any natural numbers $n$ and $m$, if $n < m$, then $(n : ℤ) < (m : ℤ)$.

Int.abs_eq_natAbs theorem

: ∀ a : ℤ, |a| = natAbs a

Full source

theorem abs_eq_natAbs : ∀ a : ℤ, |a| = natAbs a
  | (n : ℕ) => abs_of_nonneg <| ofNat_zero_le _
  | -[_+1] => abs_of_nonpos <| le_of_lt <| negSucc_lt_zero _

Absolute Value Equals Natural Absolute Value for Integers

Informal description

For any integer $a$, the absolute value of $a$ is equal to the natural number obtained by taking the absolute value of $a$ (denoted as $\text{natAbs}(a)$), i.e., $|a| = \text{natAbs}(a)$.

Int.natCast_natAbs theorem

(n : ℤ) : (n.natAbs : ℤ) = |n|

Full source

@[simp, norm_cast] lemma natCast_natAbs (n : ℤ) : (n.natAbs : ℤ) = |n| := n.abs_eq_natAbs.symm

Embedding of Natural Absolute Value Equals Integer Absolute Value

Informal description

For any integer $n$, the canonical embedding of its natural absolute value into the integers equals the absolute value of $n$, i.e., $(\text{natAbs}(n) : \mathbb{Z}) = |n|$.

Int.natAbs_abs theorem

(a : ℤ) : natAbs |a| = natAbs a

Full source

theorem natAbs_abs (a : ℤ) : natAbs |a| = natAbs a := by rw [abs_eq_natAbs]; rfl

Natural Absolute Value Preserved by Absolute Value Operation

Informal description

For any integer $a$, the natural absolute value of $|a|$ is equal to the natural absolute value of $a$, i.e., $\text{natAbs}(|a|) = \text{natAbs}(a)$.

Int.sign_mul_abs theorem

(a : ℤ) : sign a * |a| = a

Full source

theorem sign_mul_abs (a : ℤ) : sign a * |a| = a := by
  rw [abs_eq_natAbs, sign_mul_natAbs a]

Sign-Absolute Value Product Identity: $\text{sign}(a) \cdot |a| = a$

Informal description

For any integer $a$, the product of the sign of $a$ and its absolute value equals $a$ itself, i.e., $\text{sign}(a) \cdot |a| = a$.

Int.sign_mul_self_eq_abs theorem

(a : ℤ) : sign a * a = |a|

Full source

theorem sign_mul_self_eq_abs (a : ℤ) : sign a * a = |a| := by
  rw [abs_eq_natAbs, sign_mul_self_eq_natAbs]

Sign-Absolute Value Identity: $\text{sign}(a) \cdot a = |a|$

Informal description

For any integer $a$, the product of its sign and itself equals its absolute value, i.e., $\text{sign}(a) \cdot a = |a|$.

Int.natAbs_le_self_sq theorem

(a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2

Full source

lemma natAbs_le_self_sq (a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2 := by
  rw [← Int.natAbs_sq a, sq]
  norm_cast
  apply Nat.le_mul_self

Natural Absolute Value Bound by Square: $|a|_{\mathbb{N}} \leq a^2$

Informal description

For any integer $a$, the absolute value of $a$ (as a natural number) is less than or equal to $a^2$ when viewed as an integer, i.e., $|a|_{\mathbb{N}} \leq a^2$.

Int.le_self_sq theorem

(b : ℤ) : b ≤ b ^ 2

Full source

lemma le_self_sq (b : ℤ) : b ≤ b ^ 2 := le_trans le_natAbs (natAbs_le_self_sq _)

Integer Self-Square Inequality: $b \leq b^2$

Informal description

For any integer $b$, it holds that $b \leq b^2$.

Int.abs_natCast theorem

(n : ℕ) : |(n : ℤ)| = n

Full source

@[norm_cast] lemma abs_natCast (n : ℕ) : |(n : ℤ)| = n := abs_of_nonneg (natCast_nonneg n)

Absolute Value of Natural Number Cast to Integers: $|n| = n$

Informal description

For any natural number $n$, the absolute value of the integer cast of $n$ is equal to $n$, i.e., $|(n : \mathbb{Z})| = n$.

Int.natAbs_sub_pos_iff theorem

{i j : ℤ} : 0 < natAbs (i - j) ↔ i ≠ j

Full source

theorem natAbs_sub_pos_iff {i j : ℤ} : 0 < natAbs (i - j) ↔ i ≠ j := by
  rw [natAbs_pos, ne_eq, sub_eq_zero]

Positivity of Natural Absolute Difference for Integers: $0 < |i-j|_{\mathbb{N}} \leftrightarrow i \neq j$

Informal description

For any integers $i$ and $j$, the natural absolute value of their difference is positive if and only if $i$ is not equal to $j$, i.e., $0 < |i - j|_{\mathbb{N}} \leftrightarrow i \neq j$.

Int.natAbs_sub_ne_zero_iff theorem

{i j : ℤ} : natAbs (i - j) ≠ 0 ↔ i ≠ j

Full source

theorem natAbs_sub_ne_zero_iff {i j : ℤ} : natAbsnatAbs (i - j) ≠ 0natAbs (i - j) ≠ 0 ↔ i ≠ j :=
  Nat.ne_zero_iff_zero_lt.trans natAbs_sub_pos_iff

Nonzero Natural Absolute Difference for Integers: $|i-j|_{\mathbb{N}} \neq 0 \leftrightarrow i \neq j$

Informal description

For any integers $i$ and $j$, the natural absolute value of their difference is nonzero if and only if $i$ is not equal to $j$, i.e., $|i - j|_{\mathbb{N}} \neq 0 \leftrightarrow i \neq j$.

Int.abs_lt_one_iff theorem

{a : ℤ} : |a| < 1 ↔ a = 0

Full source

@[simp]
theorem abs_lt_one_iff {a : ℤ} : |a||a| < 1 ↔ a = 0 := by
  rw [← zero_add 1, lt_add_one_iff, abs_nonpos_iff]

Characterization of Zero via Absolute Value: $|a| < 1 \leftrightarrow a = 0$

Informal description

For any integer $a$, the absolute value of $a$ is less than 1 if and only if $a$ is equal to 0, i.e., $|a| < 1 \leftrightarrow a = 0$.

Int.abs_le_one_iff theorem

{a : ℤ} : |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1

Full source

theorem abs_le_one_iff {a : ℤ} : |a||a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1 := by
  rw [le_iff_lt_or_eq, abs_lt_one_iff]
  match a with
  | (n : ℕ) => simp [abs_eq_natAbs]
  | -[n+1] =>
      simp only [negSucc_ne_zero, abs_eq_natAbs, natAbs_negSucc, succ_eq_add_one,
        Int.natCast_add, cast_ofNat_Int, add_eq_right, natCast_eq_zero, false_or, reduceNeg]
      rw [negSucc_eq]
      omega

Characterization of Small Integers via Absolute Value: $|a| \leq 1 \leftrightarrow a \in \{0, 1, -1\}$

Informal description

For any integer $a$, the absolute value of $a$ is less than or equal to 1 if and only if $a$ is equal to 0, 1, or $-1$, i.e., $|a| \leq 1 \leftrightarrow (a = 0 \lor a = 1 \lor a = -1)$.

Int.one_le_abs theorem

{z : ℤ} (h₀ : z ≠ 0) : 1 ≤ |z|

Full source

theorem one_le_abs {z : ℤ} (h₀ : z ≠ 0) : 1 ≤ |z| :=
  add_one_le_iff.mpr (abs_pos.mpr h₀)

Lower bound on absolute value of nonzero integers: $1 \leq |z|$ for $z \neq 0$

Informal description

For any nonzero integer $z$, the absolute value of $z$ is at least 1, i.e., $1 \leq |z|$.

Int.abs_sub_lt_of_lt_lt theorem

{m a b : ℕ} (ha : a < m) (hb : b < m) : |(b : ℤ) - a| < m

Full source

lemma abs_sub_lt_of_lt_lt {m a b : ℕ} (ha : a < m) (hb : b < m) : |(b : ℤ) - a| < m := by
  rw [abs_lt]; omega

Absolute Difference Bound for Natural Numbers Embedded in Integers

Informal description

For any natural numbers $a$, $b$, and $m$ such that $a < m$ and $b < m$, the absolute difference between the integers $b$ and $a$ is strictly less than $m$, i.e., $|b - a| < m$.

Int.ediv_eq_zero_of_lt_abs theorem

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

Full source

theorem ediv_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < |b|) : a / b = 0 :=
  match b, |b|, abs_eq_natAbs b, H2 with
  | (n : ℕ), _, rfl, H2 => ediv_eq_zero_of_lt H1 H2
  | -[n+1], _, rfl, H2 => neg_injective <| by rw [← Int.ediv_neg]; exact ediv_eq_zero_of_lt H1 H2

Integer Division by Larger Absolute Value Yields Zero

Informal description

For any integers $a$ and $b$ such that $0 \leq a$ and $a < |b|$, the integer division of $a$ by $b$ equals zero, i.e., $a / b = 0$.

Int.emod_abs theorem

(a b : ℤ) : a % |b| = a % b

Full source

@[simp]
theorem emod_abs (a b : ℤ) : a % |b| = a % b :=
  abs_by_cases (fun i => a % i = a % b) rfl (emod_neg _ _)

Modulo by Absolute Value Equals Modulo

Informal description

For any integers $a$ and $b$, the remainder of $a$ divided by the absolute value of $b$ is equal to the remainder of $a$ divided by $b$, i.e., $a \% |b| = a \% b$.

Int.emod_lt_abs theorem

(a : ℤ) {b : ℤ} (H : b ≠ 0) : a % b < |b|

Full source

theorem emod_lt_abs (a : ℤ) {b : ℤ} (H : b ≠ 0) : a % b < |b| := by
  rw [← emod_abs]; exact emod_lt_of_pos _ (abs_pos.2 H)

Bound on Integer Remainder: $a \% b < |b|$ for $b \neq 0$

Informal description

For any integer $a$ and any nonzero integer $b$, the remainder of $a$ divided by $b$ is strictly less than the absolute value of $b$, i.e., $a \% b < |b|$.

Int.abs_ediv_le_abs theorem

: ∀ a b : ℤ, |a / b| ≤ |a|

Full source

theorem abs_ediv_le_abs : ∀ a b : ℤ, |a / b| ≤ |a| :=
  suffices ∀ (a : ℤ) (n : ℕ), |a / n| ≤ |a| from fun a b =>
    match b, Int.eq_nat_or_neg b with
    | _, ⟨n, Or.inl rfl⟩ => this _ _
    | _, ⟨n, Or.inr rfl⟩ => by rw [Int.ediv_neg, abs_neg]; apply this
  fun a n => by
  rw [abs_eq_natAbs, abs_eq_natAbs];
  exact ofNat_le_ofNat_of_le
    (match a, n with
      | (m : ℕ), n => Nat.div_le_self _ _
      | -[m+1], 0 => Nat.zero_le _
      | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))

Absolute Value Bound for Integer Division: $|a / b| \leq |a|$

Informal description

For any integers $a$ and $b$, the absolute value of the integer division $a / b$ is less than or equal to the absolute value of $a$, i.e., $|a / b| \leq |a|$.

Int.abs_sign_of_nonzero theorem

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

Full source

theorem abs_sign_of_nonzero {z : ℤ} (hz : z ≠ 0) : |z.sign| = 1 := by
  rw [abs_eq_natAbs, natAbs_sign_of_ne_zero hz, Int.ofNat_one]

Absolute Value of Sign of Nonzero Integer is One

Informal description

For any nonzero integer $z$, the absolute value of the sign of $z$ is equal to $1$, i.e., $|\text{sign}(z)| = 1$.

Int.sign_eq_ediv_abs' theorem

(a : ℤ) : sign a = a / |a|

Full source

protected theorem sign_eq_ediv_abs' (a : ℤ) : sign a = a / |a| :=
  if az : a = 0 then by simp [az]
  else (Int.ediv_eq_of_eq_mul_left (mt abs_eq_zero.1 az) (sign_mul_abs _).symm).symm

Sign as Integer Division by Absolute Value: $\text{sign}(a) = a / |a|$

Informal description

For any integer $a$, the sign of $a$ is equal to the integer division of $a$ by its absolute value, i.e., $\text{sign}(a) = a / |a|$.

Int.sign_eq_abs_ediv theorem

(a : ℤ) : sign a = |a| / a

Full source

protected theorem sign_eq_abs_ediv (a : ℤ) : sign a = |a| / a :=
  if az : a = 0 then by simp [az]
  else (Int.ediv_eq_of_eq_mul_left az (sign_mul_self_eq_abs _).symm).symm

Sign as Absolute Value Divided by Integer: $\text{sign}(a) = |a| / a$

Informal description

For any integer $a$, the sign of $a$ is equal to the absolute value of $a$ divided by $a$, i.e., $\text{sign}(a) = |a| / a$.

zpow_abs_eq_one theorem

(a : G) (n : ℤ) : a ^ |n| = 1 ↔ a ^ n = 1

Full source

@[to_additive (attr := simp) abs_zsmul_eq_zero]
lemma zpow_abs_eq_one (a : G) (n : ℤ) : a ^ |n| = 1 ↔ a ^ n = 1 := by
  rw [← Int.natCast_natAbs, zpow_natCast, pow_natAbs_eq_one]

Power Identity: $a^{|n|} = 1 \leftrightarrow a^n = 1$

Informal description

For any element $a$ in a group $G$ and any integer $n$, the element $a$ raised to the absolute value of $n$ equals the identity element if and only if $a$ raised to the power of $n$ equals the identity element. In other words, $a^{|n|} = 1 \leftrightarrow a^n = 1$.