Mathlib.Algebra.Order.Ring.Cast

Int.cast_mono theorem

: Monotone (Int.cast : ℤ → R)

Full source

lemma cast_mono : Monotone (Int.cast : ℤ → R) := by
  intro m n h
  rw [← sub_nonneg] at h
  lift n - m to ℕ using h with k hk
  rw [← sub_nonneg, ← cast_sub, ← hk, cast_natCast]
  exact k.cast_nonneg'

Monotonicity of Integer Cast

Informal description

The canonical homomorphism from the integers $\mathbb{Z}$ to a type $R$ (equipped with a partial order) is monotone. That is, for any integers $m, n \in \mathbb{Z}$ such that $m \leq n$, the inequality $(m : R) \leq (n : R)$ holds.

Int.GCongr.intCast_mono theorem

{m n : ℤ} (hmn : m ≤ n) : (m : R) ≤ n

Full source

@[gcongr] protected lemma GCongr.intCast_mono {m n : ℤ} (hmn : m ≤ n) : (m : R) ≤ n := cast_mono hmn

Monotonicity of Integer Cast: $m \leq n$ implies $(m : R) \leq (n : R)$

Informal description

For any integers $m, n \in \mathbb{Z}$ such that $m \leq n$, the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies $(m : R) \leq (n : R)$.

Int.cast_nonneg theorem

: ∀ {n : ℤ}, (0 : R) ≤ n ↔ 0 ≤ n

Full source

@[simp] lemma cast_nonneg : ∀ {n : ℤ}, (0 : R) ≤ n ↔ 0 ≤ n
  | (n : ℕ) => by simp
  | -[n+1] => by
    have : -(n : R) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
    simpa [(negSucc_lt_zero n).not_le, ← sub_eq_add_neg, le_neg] using this.not_le

Nonnegativity Preservation under Integer Cast: $0 \leq n$ iff $0 \leq \text{cast}(n)$

Informal description

For any integer $n$ and any ordered ring $R$, the canonical homomorphism $\mathbb{Z} \to R$ satisfies $0 \leq n$ in $R$ if and only if $0 \leq n$ in $\mathbb{Z}$.

Int.cast_le theorem

: (m : R) ≤ n ↔ m ≤ n

Full source

@[simp, norm_cast] lemma cast_le : (m : R) ≤ n ↔ m ≤ n := by
  rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]

Preservation of Order under Integer Cast: $(m : R) \leq (n : R) \leftrightarrow m \leq n$

Informal description

For any integers $m, n \in \mathbb{Z}$ and any ordered ring $R$, the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies $(m : R) \leq (n : R)$ if and only if $m \leq n$ in $\mathbb{Z}$.

Int.cast_strictMono theorem

: StrictMono (fun x : ℤ => (x : R))

Full source

lemma cast_strictMono : StrictMono (fun x : ℤ => (x : R)) :=
  strictMono_of_le_iff_le fun _ _ => cast_le.symm

Strict Monotonicity of Integer Cast: $m < n \Rightarrow (m : R) < (n : R)$

Informal description

The canonical homomorphism from the integers $\mathbb{Z}$ to an ordered ring $R$, given by $x \mapsto (x : R)$, is strictly monotone. That is, for any integers $m, n \in \mathbb{Z}$, if $m < n$ then $(m : R) < (n : R)$.

Int.cast_lt theorem

: (m : R) < n ↔ m < n

Full source

@[simp, norm_cast] lemma cast_lt : (m : R) < n ↔ m < n := cast_strictMono.lt_iff_lt

Preservation of Strict Order under Integer Cast: $(m : R) < (n : R) \leftrightarrow m < n$

Informal description

For any integers $m, n \in \mathbb{Z}$ and any ordered ring $R$, the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies $(m : R) < (n : R)$ if and only if $m < n$ in $\mathbb{Z}$.

Int.cast_nonpos theorem

: (n : R) ≤ 0 ↔ n ≤ 0

Full source

@[simp] lemma cast_nonpos : (n : R) ≤ 0 ↔ n ≤ 0 := by rw [← cast_zero, cast_le]

Nonpositivity Preservation under Integer Cast: $(n : R) \leq 0 \leftrightarrow n \leq 0$

Informal description

For any integer $n \in \mathbb{Z}$ and any ordered ring $R$, the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies $(n : R) \leq 0$ if and only if $n \leq 0$ in $\mathbb{Z}$.

Int.cast_pos theorem

: (0 : R) < n ↔ 0 < n

Full source

@[simp] lemma cast_pos : (0 : R) < n ↔ 0 < n := by rw [← cast_zero, cast_lt]

Positivity Preservation under Integer Cast: $(0 : R) < n \leftrightarrow 0 < n$

Informal description

For any integer $n \in \mathbb{Z}$ and any ordered ring $R$, the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies $(0 : R) < (n : R)$ if and only if $0 < n$ in $\mathbb{Z}$.

Int.cast_lt_zero theorem

: (n : R) < 0 ↔ n < 0

Full source

@[simp] lemma cast_lt_zero : (n : R) < 0 ↔ n < 0 := by rw [← cast_zero, cast_lt]

Negative Integer Preservation under Cast: $(n : R) < 0 \leftrightarrow n < 0$

Informal description

For any integer $n \in \mathbb{Z}$ and any ordered ring $R$, the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies $(n : R) < 0$ if and only if $n < 0$ in $\mathbb{Z}$.

Int.cast_min theorem

: ↑(min a b) = (min a b : R)

Full source

@[simp, norm_cast]
lemma cast_min : ↑(min a b) = (min a b : R) := Monotone.map_min cast_mono

Preservation of Minimum under Integer Cast

Informal description

For any integers $a, b \in \mathbb{Z}$, the canonical homomorphism from $\mathbb{Z}$ to $R$ preserves the minimum operation, i.e., $\min(a, b) = \min((a : R), (b : R))$.

Int.cast_max theorem

: (↑(max a b) : R) = max (a : R) (b : R)

Full source

@[simp, norm_cast]
lemma cast_max : (↑(max a b) : R) = max (a : R) (b : R) := Monotone.map_max cast_mono

Preservation of Maximum under Integer Cast

Informal description

For any integers $a, b \in \mathbb{Z}$ and any type $R$ with a partial order, the canonical homomorphism from $\mathbb{Z}$ to $R$ preserves the maximum operation. That is, the image of $\max(a, b)$ under the homomorphism is equal to the maximum of the images of $a$ and $b$ in $R$: \[ \text{cast}(\max(a, b)) = \max(\text{cast}(a), \text{cast}(b)) \]

Int.cast_abs theorem

: (↑|a| : R) = |(a : R)|

Full source

@[simp, norm_cast]
lemma cast_abs : (↑|a| : R) = |(a : R)| := by simp [abs_eq_max_neg]

Preservation of Absolute Value under Integer Cast

Informal description

For any integer $a$ and any ordered additive group $R$, the canonical homomorphism from $\mathbb{Z}$ to $R$ preserves the absolute value operation. That is, the image of $|a|$ under the homomorphism is equal to the absolute value of the image of $a$ in $R$: \[ \text{cast}(|a|) = |\text{cast}(a)| \]

Int.cast_one_le_of_pos theorem

(h : 0 < a) : (1 : R) ≤ a

Full source

lemma cast_one_le_of_pos (h : 0 < a) : (1 : R) ≤ a := mod_cast Int.add_one_le_of_lt h

Positivity implies one is less than or equal to integer cast in ordered groups

Informal description

For any integer $a$ and any ordered additive group with one $R$, if $a$ is positive (i.e., $0 < a$), then the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies $1 \leq a$ in $R$.

Int.cast_le_neg_one_of_neg theorem

(h : a < 0) : (a : R) ≤ -1

Full source

lemma cast_le_neg_one_of_neg (h : a < 0) : (a : R) ≤ -1 := by
  rw [← Int.cast_one, ← Int.cast_neg, cast_le]
  exact Int.le_sub_one_of_lt h

Negative Integers Cast to Ordered Groups are Bounded by Negative One

Informal description

For any integer $a$ and any ordered additive group with one $R$, if $a$ is negative (i.e., $a < 0$), then the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies $(a : R) \leq -1$.

Int.cast_le_neg_one_or_one_le_cast_of_ne_zero theorem

(hn : n ≠ 0) : (n : R) ≤ -1 ∨ 1 ≤ (n : R)

Full source

lemma cast_le_neg_one_or_one_le_cast_of_ne_zero (hn : n ≠ 0) : (n : R) ≤ -1 ∨ 1 ≤ (n : R) :=
  hn.lt_or_lt.imp cast_le_neg_one_of_neg cast_one_le_of_pos

Nonzero Integer Cast is Bounded by $-1$ or $1$ in Ordered Groups

Informal description

For any integer $n \neq 0$ and any ordered additive group with one $R$, the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies either $(n : R) \leq -1$ or $1 \leq (n : R)$.

Int.nneg_mul_add_sq_of_abs_le_one theorem

(n : ℤ) (hx : |x| ≤ 1) : (0 : R) ≤ n * x + n * n

Full source

lemma nneg_mul_add_sq_of_abs_le_one (n : ℤ) (hx : |x| ≤ 1) : (0 : R) ≤ n * x + n * n := by
  have hnx : 0 < n → 0 ≤ x + n := fun hn => by
    have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
    rwa [neg_add_cancel] at this
  have hnx' : n < 0 → x + n ≤ 0 := fun hn => by
    have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
    rwa [add_neg_cancel] at this
  rw [← mul_add, mul_nonneg_iff]
  rcases lt_trichotomy n 0 with (h | rfl | h)
  · exact Or.inr ⟨mod_cast h.le, hnx' h⟩
  · simp [le_total 0 x]
  · exact Or.inl ⟨mod_cast h.le, hnx h⟩

Nonnegativity of $n x + n^2$ for $|x| \leq 1$ and integer $n$

Informal description

For any integer $n$ and any real number $x$ with $|x| \leq 1$, the expression $n \cdot x + n^2$ is nonnegative, i.e., $0 \leq n x + n^2$.

Int.cast_natAbs theorem

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

Full source

lemma cast_natAbs : (n.natAbs : R) = |n| := by
  cases n
  · simp
  · rw [abs_eq_natAbs, natAbs_negSucc, cast_succ, cast_natCast, cast_succ]

Natural Absolute Value Preserved Under Canonical Homomorphism: $(|n|_{\mathbb{N}} : R) = |n|_R$

Informal description

For any integer $n$ and any additive group with one $R$, the canonical homomorphism from $\mathbb{N}$ to $R$ applied to the natural absolute value of $n$ equals the absolute value of $n$ in $R$, i.e., $(|n|_{\mathbb{N}} : R) = |n|_R$.

OrderDual.instIntCast instance

[IntCast R] : IntCast Rᵒᵈ

Full source

instance instIntCast [IntCast R] : IntCast Rᵒᵈ := ‹_›

Integer Cast on Order Dual

Informal description

For any type $R$ with a canonical homomorphism from the integers, the order dual $R^{\text{op}}$ also has a canonical homomorphism from the integers.

OrderDual.instAddGroupWithOne instance

[AddGroupWithOne R] : AddGroupWithOne Rᵒᵈ

Full source

instance instAddGroupWithOne [AddGroupWithOne R] : AddGroupWithOne Rᵒᵈ := ‹_›

Order Dual of an Additive Group with One is an Additive Group with One

Informal description

For any additive group with one $R$, the order dual $R^{\text{op}}$ is also an additive group with one.

OrderDual.instAddCommGroupWithOne instance

[AddCommGroupWithOne R] : AddCommGroupWithOne Rᵒᵈ

Full source

instance instAddCommGroupWithOne [AddCommGroupWithOne R] : AddCommGroupWithOne Rᵒᵈ := ‹_›

Order Dual of an Additive Commutative Group with One

Informal description

For any additive commutative group with one $R$, the order dual $R^{\text{op}}$ is also an additive commutative group with one.

toDual_intCast theorem

[IntCast R] (n : ℤ) : toDual (n : R) = n

Full source

@[simp] lemma toDual_intCast [IntCast R] (n : ℤ) : toDual (n : R) = n := rfl

Preservation of Integer Casts under Order Dual Embedding

Informal description

For any type $R$ with a canonical homomorphism from the integers, and for any integer $n \in \mathbb{Z}$, the image of $n$ under the canonical homomorphism to the order dual $R^{\text{op}}$ is equal to the image of $n$ in $R$ under the order dual embedding. In other words, the order dual embedding preserves integer casts.

ofDual_intCast theorem

[IntCast R] (n : ℤ) : (ofDual n : R) = n

Full source

@[simp] lemma ofDual_intCast [IntCast R] (n : ℤ) : (ofDual n : R) = n := rfl

Preservation of Integer Casts under Order Dual Projection

Informal description

For any type $R$ with a canonical homomorphism from the integers, and for any integer $n \in \mathbb{Z}$, the image of $n$ under the order dual embedding `ofDual` is equal to the image of $n$ under the canonical homomorphism in $R$. That is, $\text{ofDual}(n) = n$ in $R$.

Lex.instIntCast instance

[IntCast R] : IntCast (Lex R)

Full source

instance instIntCast [IntCast R] : IntCast (Lex R) := ‹_›

Integer Casting in Lexicographic Order

Informal description

For any type $R$ with an integer casting operation, the lexicographic order on $R$ also inherits an integer casting operation.

Lex.instAddGroupWithOne instance

[AddGroupWithOne R] : AddGroupWithOne (Lex R)

Full source

instance instAddGroupWithOne [AddGroupWithOne R] : AddGroupWithOne (Lex R) := ‹_›

Additive Group with One Structure on Lexicographic Order

Informal description

For any type $R$ with an additive group structure with one, the lexicographic order on $R$ also inherits an additive group with one structure.

Lex.instAddCommGroupWithOne instance

[AddCommGroupWithOne R] : AddCommGroupWithOne (Lex R)

Full source

instance instAddCommGroupWithOne [AddCommGroupWithOne R] : AddCommGroupWithOne (Lex R) := ‹_›

Additive Commutative Group with One Structure on Lexicographic Order

Informal description

For any type $R$ with an additive commutative group structure with one, the lexicographic order on $R$ also inherits an additive commutative group structure with one.

toLex_intCast theorem

[IntCast R] (n : ℤ) : toLex (n : R) = n

Full source

@[simp] lemma toLex_intCast [IntCast R] (n : ℤ) : toLex (n : R) = n := rfl

Integer Cast Preservation Under Lexicographic Order Embedding

Informal description

For any type $R$ with an integer casting operation and for any integer $n \in \mathbb{Z}$, the operation `toLex` applied to the integer cast of $n$ in $R$ equals the integer cast of $n$ in the lexicographic order of $R$, i.e., $\text{toLex}(n) = n$ where $n$ is interpreted in $\text{Lex}(R)$.

ofLex_intCast theorem

[IntCast R] (n : ℤ) : (ofLex n : R) = n

Full source

@[simp] lemma ofLex_intCast [IntCast R] (n : ℤ) : (ofLex n : R) = n := rfl

Integer Cast Preservation Under Lexicographic Order Projection

Informal description

For any type $R$ with an integer casting operation and for any integer $n \in \mathbb{Z}$, the operation `ofLex` applied to the integer cast of $n$ in the lexicographic order of $R$ equals the integer cast of $n$ in $R$, i.e., $\text{ofLex}(n) = n$ where $n$ is interpreted in $R$.

TODO