Mathlib.Data.Nat.Cast.Order.Basic

Nat.mono_cast theorem

: Monotone (Nat.cast : ℕ → α)

Full source

@[mono]
theorem mono_cast : Monotone (Nat.cast : ℕ → α) :=
  monotone_nat_of_le_succ fun n ↦ by
    rw [Nat.cast_succ]; exact le_add_of_nonneg_right zero_le_one

Monotonicity of Natural Number Cast

Informal description

The canonical embedding from the natural numbers $\mathbb{N}$ to a type $\alpha$ is monotone. That is, for any natural numbers $n \leq m$, the corresponding elements in $\alpha$ satisfy $(n : \alpha) \leq (m : \alpha)$.

GCongr.natCast_le_natCast theorem

{a b : ℕ} (h : a ≤ b) : (a : α) ≤ b

Full source

@[gcongr]
theorem _root_.GCongr.natCast_le_natCast {a b : ℕ} (h : a ≤ b) : (a : α) ≤ b := mono_cast h

Monotonicity of Natural Number Embedding: $a \leq b \Rightarrow (a : \alpha) \leq (b : \alpha)$

Informal description

For any natural numbers $a$ and $b$ such that $a \leq b$, the canonical embedding into $\alpha$ satisfies $(a : \alpha) \leq (b : \alpha)$.

Nat.cast_nonneg' theorem

(n : ℕ) : 0 ≤ (n : α)

Full source

/-- See also `Nat.cast_nonneg`, specialised for an `OrderedSemiring`. -/
@[simp low]
theorem cast_nonneg' (n : ℕ) : 0 ≤ (n : α) :=
  @Nat.cast_zero α _ ▸ mono_cast (Nat.zero_le n)

Nonnegativity of Natural Number Cast: $0 \leq (n : \alpha)$

Informal description

For any natural number $n$, the canonical embedding of $n$ into a type $\alpha$ is nonnegative, i.e., $0 \leq (n : \alpha)$.

Nat.ofNat_nonneg' theorem

(n : ℕ) [n.AtLeastTwo] : 0 ≤ (ofNat(n) : α)

Full source

/-- See also `Nat.ofNat_nonneg`, specialised for an `OrderedSemiring`. -/
@[simp low]
theorem ofNat_nonneg' (n : ℕ) [n.AtLeastTwo] : 0 ≤ (ofNat(n) : α) := cast_nonneg' n

Nonnegativity of Canonical Embedding for $n \geq 2$: $0 \leq (n : \alpha)$

Informal description

For any natural number $n$ (with $n \geq 2$), the canonical embedding of $n$ into a type $\alpha$ is nonnegative, i.e., $0 \leq (n : \alpha)$.

Nat.cast_add_one_pos theorem

(n : ℕ) : 0 < (n : α) + 1

Full source

theorem cast_add_one_pos (n : ℕ) : 0 < (n : α) + 1 := by
  apply zero_lt_one.trans_le
  convert (@mono_cast α _).imp (?_ : 1 ≤ n + 1)
  <;> simp

Positivity of Successor in Ordered Semiring: $0 < (n : \alpha) + 1$

Informal description

For any natural number $n$ and any ordered semiring $\alpha$, the element $(n : \alpha) + 1$ is positive, i.e., $0 < (n : \alpha) + 1$.

Nat.cast_pos' theorem

{n : ℕ} : (0 : α) < n ↔ 0 < n

Full source

/-- See also `Nat.cast_pos`, specialised for an `OrderedSemiring`. -/
@[simp low]
theorem cast_pos' {n : ℕ} : (0 : α) < n ↔ 0 < n := by cases n <;> simp [cast_add_one_pos]

Positivity of Natural Number Cast in Ordered Semiring

Informal description

For any natural number $n$ and any ordered semiring $\alpha$, the cast of $n$ into $\alpha$ is positive if and only if $n$ is positive, i.e., $0 < (n : \alpha) \leftrightarrow 0 < n$.

Nat.strictMono_cast theorem

: StrictMono (Nat.cast : ℕ → α)

Full source

theorem strictMono_cast : StrictMono (Nat.cast : ℕ → α) :=
  mono_cast.strictMono_of_injective cast_injective

Strict Monotonicity of Natural Number Cast

Informal description

The canonical embedding from the natural numbers $\mathbb{N}$ to a type $\alpha$ is strictly monotone. That is, for any natural numbers $n < m$, the corresponding elements in $\alpha$ satisfy $(n : \alpha) < (m : \alpha)$.

GCongr.natCast_lt_natCast theorem

{a b : ℕ} (h : a < b) : (a : α) < b

Full source

@[gcongr]
lemma _root_.GCongr.natCast_lt_natCast {a b : ℕ} (h : a < b) : (a : α) < b := strictMono_cast h

Strict Inequality Preservation under Natural Number Cast

Informal description

For any natural numbers $a$ and $b$ such that $a < b$, the canonical embedding of $a$ into a type $\alpha$ is strictly less than the canonical embedding of $b$ into $\alpha$, i.e., $(a : \alpha) < (b : \alpha)$.

Nat.castOrderEmbedding definition

: ℕ ↪o α

Full source

/-- `Nat.cast : ℕ → α` as an `OrderEmbedding` -/
@[simps! -fullyApplied]
def castOrderEmbedding : ℕℕ ↪o α :=
  OrderEmbedding.ofStrictMono Nat.cast Nat.strictMono_cast

Order embedding of natural numbers into $\alpha$

Informal description

The canonical embedding of natural numbers into a type $\alpha$ as an order embedding. That is, the map $\text{Nat.cast} : \mathbb{N} \to \alpha$ preserves the order structure, meaning for any natural numbers $n$ and $m$, $n \leq m$ if and only if $(n : \alpha) \leq (m : \alpha)$.

Nat.cast_le theorem

: (m : α) ≤ n ↔ m ≤ n

Full source

@[simp, norm_cast]
theorem cast_le : (m : α) ≤ n ↔ m ≤ n :=
  strictMono_cast.le_iff_le

Preservation of Non-Strict Order under Natural Number Cast: $(m : \alpha) \leq (n : \alpha) \leftrightarrow m \leq n$

Informal description

For any natural numbers $m$ and $n$, and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of $m$ into $\alpha$ is less than or equal to the embedding of $n$ if and only if $m \leq n$ holds in the natural numbers. In other words, $(m : \alpha) \leq (n : \alpha) \leftrightarrow m \leq n$.

Nat.cast_lt theorem

: (m : α) < n ↔ m < n

Full source

@[simp, norm_cast, mono]
theorem cast_lt : (m : α) < n ↔ m < n :=
  strictMono_cast.lt_iff_lt

Preservation of Strict Order under Natural Number Cast: $(m : \alpha) < (n : \alpha) \leftrightarrow m < n$

Informal description

For any natural numbers $m$ and $n$, and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of $m$ into $\alpha$ is less than the embedding of $n$ if and only if $m < n$ holds in the natural numbers. In other words, $(m : \alpha) < (n : \alpha) \leftrightarrow m < n$.

Nat.one_lt_cast theorem

: 1 < (n : α) ↔ 1 < n

Full source

@[simp, norm_cast]
theorem one_lt_cast : 1 < (n : α) ↔ 1 < n := by rw [← cast_one, cast_lt]

Preservation of Strict Inequality for One under Natural Number Cast: $1 < (n : \alpha) \leftrightarrow 1 < n$

Informal description

For any natural number $n$ and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of $1$ into $\alpha$ is less than the embedding of $n$ if and only if $1 < n$ holds in the natural numbers. In other words, $1 < (n : \alpha) \leftrightarrow 1 < n$.

Nat.one_le_cast theorem

: 1 ≤ (n : α) ↔ 1 ≤ n

Full source

@[simp, norm_cast]
theorem one_le_cast : 1 ≤ (n : α) ↔ 1 ≤ n := by rw [← cast_one, cast_le]

Preservation of $1 \leq n$ under Natural Number Cast: $(1 : \alpha) \leq (n : \alpha) \leftrightarrow 1 \leq n$

Informal description

For any natural number $n$ and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of $1$ into $\alpha$ is less than or equal to the embedding of $n$ if and only if $1 \leq n$ holds in the natural numbers. In other words, $(1 : \alpha) \leq (n : \alpha) \leftrightarrow 1 \leq n$.

Nat.cast_lt_one theorem

: (n : α) < 1 ↔ n = 0

Full source

@[simp, norm_cast]
theorem cast_lt_one : (n : α) < 1 ↔ n = 0 := by
  rw [← cast_one, cast_lt, Nat.lt_succ_iff, le_zero]

Characterization of Natural Number Cast Less Than One: $(n : \alpha) < 1 \leftrightarrow n = 0$

Informal description

For any natural number $n$ and any additive monoid with one $\alpha$ of characteristic zero, the cast of $n$ in $\alpha$ is less than $1$ if and only if $n = 0$.

Nat.cast_le_one theorem

: (n : α) ≤ 1 ↔ n ≤ 1

Full source

@[simp, norm_cast]
theorem cast_le_one : (n : α) ≤ 1 ↔ n ≤ 1 := by rw [← cast_one, cast_le]

Preservation of Non-Strict Order at One under Natural Number Cast: $(n : \alpha) \leq 1 \leftrightarrow n \leq 1$

Informal description

For any natural number $n$ and any additive monoid with one $\alpha$ of characteristic zero, the cast of $n$ in $\alpha$ is less than or equal to $1$ if and only if $n \leq 1$ holds in the natural numbers.

Nat.cast_nonpos theorem

: (n : α) ≤ 0 ↔ n = 0

Full source

@[simp] lemma cast_nonpos : (n : α) ≤ 0 ↔ n = 0 := by norm_cast; omega

Nonpositivity of Natural Number Cast in Characteristic Zero Monoids

Informal description

For any natural number $n$ and any additive monoid with one $\alpha$ of characteristic zero, the cast of $n$ in $\alpha$ is less than or equal to zero if and only if $n$ is equal to zero. In other words, $n \leq 0$ in $\alpha$ holds precisely when $n = 0$ in $\mathbb{N}$.

Nat.ofNat_le_cast theorem

: (ofNat(m) : α) ≤ n ↔ (OfNat.ofNat m : ℕ) ≤ n

Full source

@[simp]
theorem ofNat_le_cast : (ofNat(m) : α) ≤ n ↔ (OfNat.ofNat m : ℕ) ≤ n :=
  cast_le

Order Preservation of Natural Number Cast in Characteristic Zero Monoids: $(m : \alpha) \leq n \leftrightarrow m \leq n$

Informal description

For any natural number $m$ and any element $n$ in a characteristic zero monoid $\alpha$, the cast of $m$ in $\alpha$ is less than or equal to $n$ if and only if $m$ is less than or equal to the natural number corresponding to $n$. In other words, $(m : \alpha) \leq n \leftrightarrow m \leq n$ where $n$ is interpreted as a natural number via the canonical embedding.

Nat.ofNat_lt_cast theorem

: (ofNat(m) : α) < n ↔ (OfNat.ofNat m : ℕ) < n

Full source

@[simp]
theorem ofNat_lt_cast : (ofNat(m) : α) < n ↔ (OfNat.ofNat m : ℕ) < n :=
  cast_lt

Preservation of Strict Inequality for Numeric Literals under Natural Number Cast: $(m : \alpha) < n \leftrightarrow m < n$

Informal description

For any natural number $m$ and any type $\alpha$ with a characteristic zero monoid structure, the cast of the literal $m$ in $\alpha$ is less than $n$ if and only if $m$ is less than $n$ in the natural numbers. In other words, $(m : \alpha) < n \leftrightarrow m < n$.

Nat.cast_le_ofNat theorem

: (m : α) ≤ (ofNat(n) : α) ↔ m ≤ OfNat.ofNat n

Full source

@[simp]
theorem cast_le_ofNat : (m : α) ≤ (ofNat(n) : α) ↔ m ≤ OfNat.ofNat n :=
  cast_le

Preservation of Non-Strict Order under Natural Number Cast with Literals: $(m : \alpha) \leq (n : \alpha) \leftrightarrow m \leq n$

Informal description

For any natural numbers $m$ and $n$, and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of $m$ into $\alpha$ is less than or equal to the embedding of the literal $n$ (as `OfNat.ofNat n`) if and only if $m \leq n$ holds in the natural numbers. In other words, $(m : \alpha) \leq (n : \alpha) \leftrightarrow m \leq n$.

Nat.cast_lt_ofNat theorem

: (m : α) < (ofNat(n) : α) ↔ m < OfNat.ofNat n

Full source

@[simp]
theorem cast_lt_ofNat : (m : α) < (ofNat(n) : α) ↔ m < OfNat.ofNat n :=
  cast_lt

Preservation of Strict Order under Natural Number Cast with Literals: $(m : \alpha) < n \leftrightarrow m < n$

Informal description

For any natural numbers $m$ and $n$, and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of $m$ into $\alpha$ is less than the embedding of the literal $n$ (as an element of $\alpha$) if and only if $m$ is less than $n$ in the natural numbers. In other words, $(m : \alpha) < (n : \alpha) \leftrightarrow m < n$.

Nat.one_lt_ofNat theorem

: 1 < (ofNat(n) : α)

Full source

@[simp]
theorem one_lt_ofNat : 1 < (ofNat(n) : α) :=
  one_lt_cast.mpr AtLeastTwo.one_lt

Embedding of Natural Numbers Preserves One Less Than: $1 < (n : \alpha)$

Informal description

For any natural number $n$ and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of the natural number $1$ into $\alpha$ is strictly less than the embedding of $n$ (as `OfNat.ofNat n`), i.e., $1 < (n : \alpha)$.

Nat.one_le_ofNat theorem

: 1 ≤ (ofNat(n) : α)

Full source

@[simp]
theorem one_le_ofNat : 1 ≤ (ofNat(n) : α) :=
  one_le_cast.mpr NeZero.one_le

Embedding of Natural Numbers Preserves One Less Than or Equal: $1 \leq (n : \alpha)$

Informal description

For any natural number $n \geq 1$ and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of $n$ into $\alpha$ satisfies $1 \leq (n : \alpha)$.

Nat.not_ofNat_le_one theorem

: ¬(ofNat(n) : α) ≤ 1

Full source

@[simp]
theorem not_ofNat_le_one : ¬(ofNat(n) : α) ≤ 1 :=
  (cast_le_one.not.trans not_le).mpr AtLeastTwo.one_lt

Negation of Cast Natural Number Being Less Than or Equal to One: $\neg(n : \alpha) \leq 1$

Informal description

For any natural number $n$ and any additive monoid with one $\alpha$ of characteristic zero, it is not the case that the cast of $n$ in $\alpha$ is less than or equal to $1$.

Nat.not_ofNat_lt_one theorem

: ¬(ofNat(n) : α) < 1

Full source

@[simp]
theorem not_ofNat_lt_one : ¬(ofNat(n) : α) < 1 :=
  mt le_of_lt not_ofNat_le_one

Negation of Cast Natural Number Being Strictly Less Than One: $\neg(n : \alpha) < 1$

Informal description

For any natural number $n$ and any additive monoid with one $\alpha$ of characteristic zero, it is not the case that the cast of $n$ in $\alpha$ is strictly less than $1$.

Nat.ofNat_le theorem

: (ofNat(m) : α) ≤ (ofNat(n) : α) ↔ (OfNat.ofNat m : ℕ) ≤ OfNat.ofNat n

Full source

theorem ofNat_le :
    (ofNat(m) : α) ≤ (ofNat(n) : α) ↔ (OfNat.ofNat m : ℕ) ≤ OfNat.ofNat n :=
  cast_le

Preservation of Non-Strict Order under Natural Number Cast: $(m : \alpha) \leq (n : \alpha) \leftrightarrow m \leq n$

Informal description

For any natural numbers $m$ and $n$, and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of $m$ into $\alpha$ is less than or equal to the embedding of $n$ if and only if $m \leq n$ holds in the natural numbers. In other words, $(m : \alpha) \leq (n : \alpha) \leftrightarrow m \leq n$.

Nat.ofNat_lt theorem

: (ofNat(m) : α) < (ofNat(n) : α) ↔ (OfNat.ofNat m : ℕ) < OfNat.ofNat n

Full source

theorem ofNat_lt :
    (ofNat(m) : α) < (ofNat(n) : α) ↔ (OfNat.ofNat m : ℕ) < OfNat.ofNat n :=
  cast_lt

Preservation of Strict Order under Natural Number Cast: $(m : \alpha) < (n : \alpha) \leftrightarrow m < n$

Informal description

For any natural numbers $m$ and $n$, and any type $\alpha$ with a characteristic zero monoid structure, the canonical embedding of $m$ into $\alpha$ is less than the embedding of $n$ if and only if $m < n$ holds in the natural numbers. In other words, $(m : \alpha) < (n : \alpha) \leftrightarrow m < n$.

instNontrivialOfCharZero instance

[AddMonoidWithOne α] [CharZero α] : Nontrivial α

Full source

instance [AddMonoidWithOne α] [CharZero α] : Nontrivial α where exists_pair_ne :=
  ⟨1, 0, (Nat.cast_one (R := α) ▸ Nat.cast_ne_zero.2 (by decide))⟩

Nontriviality of Characteristic Zero Monoids

Informal description

Every additive monoid with one $\alpha$ of characteristic zero is nontrivial.

NeZero.nat_of_injective theorem

{n : ℕ} [NeZero (n : R)] [RingHomClass F R S] {f : F} (hf : Function.Injective f) : NeZero (n : S)

Full source

theorem NeZero.nat_of_injective {n : ℕ} [NeZero (n : R)] [RingHomClass F R S] {f : F}
    (hf : Function.Injective f) : NeZero (n : S) :=
  ⟨fun h ↦ NeZero.natCast_ne n R <| hf <| by simpa only [map_natCast, map_zero f]⟩

Non-zero natural numbers remain non-zero under injective ring homomorphisms

Informal description

Let $R$ and $S$ be rings, and let $F$ be a ring homomorphism class from $R$ to $S$. Suppose $n$ is a natural number such that the image of $n$ in $R$ is non-zero (i.e., $n \neq 0$ in $R$). If $f : F$ is an injective ring homomorphism, then the image of $n$ in $S$ is also non-zero (i.e., $n \neq 0$ in $S$).