doc-next-gen

Mathlib.Algebra.Order.Ring.Int

Module docstring

{"# 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. ","### Miscellaneous lemmas "}
Int.instIsStrictOrderedRing instance
: IsStrictOrderedRing ℤ
Full source 
instance instIsStrictOrderedRing : IsStrictOrderedRing ℤ := .of_mul_pos @Int.mul_pos
The Integers as a Strict Ordered Ring
Informal description
The integers $\mathbb{Z}$ form a strict ordered ring, meaning: 1. Addition is strictly monotone (if $a < b$ then $a + c < b + c$ for all $c$) 2. Multiplication by positive elements is strictly monotone (if $0 < a$ and $b < c$ then $a \cdot b < a \cdot c$) 3. The ring is nontrivial ($0 \neq 1$) and satisfies $0 \leq 1$
Int.isCompl_even_odd theorem
: IsCompl {n : ℤ | Even n} {n | Odd n}
Full source 
lemma isCompl_even_odd : IsCompl { n : ℤ | Even n } { n | Odd n } := by
  simp [← not_even_iff_odd, ← Set.compl_setOf, isCompl_compl]
Complementarity of Even and Odd Integer Sets in $\mathbb{Z}$
Informal description
The sets of even integers $\{n \in \mathbb{Z} \mid \text{Even } n\}$ and odd integers $\{n \in \mathbb{Z} \mid \text{Odd } n\}$ are complementary in the Boolean algebra of subsets of $\mathbb{Z}$. That is, their union is the entire set of integers $\mathbb{Z}$ and their intersection is the empty set.
Nat.cast_natAbs theorem
{α : Type*} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = |n|
Full source 
lemma _root_.Nat.cast_natAbs {α : Type*} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = |n| := by
  rw [← natCast_natAbs, Int.cast_natCast]
Embedding of Natural Absolute Value Equals Integer Absolute Value in Additive Group with One
Informal description
For any integer $n$ and any type $\alpha$ equipped with an additive group structure with one, the canonical embedding of the natural absolute value of $n$ into $\alpha$ equals the absolute value of $n$ in $\alpha$, i.e., $(\text{natAbs}(n) : \alpha) = |n|$.
Int.two_le_iff_pos_of_even theorem
{m : ℤ} (even : Even m) : 2 ≤ m ↔ 0 < m
Full source 
lemma two_le_iff_pos_of_even {m : ℤ} (even : Even m) : 2 ≤ m ↔ 0 < m :=
  le_iff_pos_of_dvd (by decide) even.two_dvd
Even Integer Positivity Criterion: $2 \leq m \leftrightarrow 0 < m$ for even $m$
Informal description
For any integer $m$ that is even, the inequality $2 \leq m$ holds if and only if $0 < m$.
Int.add_two_le_iff_lt_of_even_sub theorem
{m n : ℤ} (even : Even (n - m)) : m + 2 ≤ n ↔ m < n
Full source 
lemma add_two_le_iff_lt_of_even_sub {m n : ℤ} (even : Even (n - m)) : m + 2 ≤ n ↔ m < n := by
  rw [add_comm]; exact le_add_iff_lt_of_dvd_sub (by decide) even.two_dvd
Even Difference Inequality: $m + 2 \leq n \leftrightarrow m < n$ when $n - m$ is even
Informal description
For any integers $m$ and $n$ such that $n - m$ is even, the inequality $m + 2 \leq n$ holds if and only if $m < n$.