Mathlib.Data.Nat.Cast.Order.Field

Nat.cast_inv_le_one theorem

: ∀ n : ℕ, (n⁻¹ : α) ≤ 1

Full source

lemma cast_inv_le_one : ∀ n : ℕ, (n⁻¹ : α) ≤ 1
  | 0 => by simp
  | n + 1 => inv_le_one_of_one_le₀ <| by simp [Nat.cast_nonneg]

Inverse of Natural Number Embedding is Bounded by One in Ordered Semifields

Informal description

For any natural number $n$ and any ordered semifield $\alpha$, the inverse of the canonical embedding of $n$ in $\alpha$ is less than or equal to $1$, i.e., $(n^{-1} : \alpha) \leq 1$.

Nat.cast_div_le theorem

{m n : ℕ} : ((m / n : ℕ) : α) ≤ m / n

Full source

/-- Natural division is always less than division in the field. -/
theorem cast_div_le {m n : ℕ} : ((m / n : ℕ) : α) ≤ m / n := by
  cases n
  · rw [cast_zero, div_zero, Nat.div_zero, cast_zero]
  rw [le_div_iff₀, ← Nat.cast_mul, @Nat.cast_le]
  · exact Nat.div_mul_le_self m _
  · exact Nat.cast_pos.2 (Nat.succ_pos _)

Natural Division Embedding Inequality: $\lceil m / n \rceil \leq m / n$ in Ordered Semifields

Informal description

For any natural numbers $m$ and $n$, and any ordered semifield $\alpha$, the canonical embedding of the natural division $m / n$ into $\alpha$ is less than or equal to the division of the embeddings of $m$ and $n$ in $\alpha$, i.e., $\lceil m / n \rceil \leq m / n$ where $\lceil \cdot \rceil$ denotes the canonical embedding from $\mathbb{N}$ to $\alpha$.

Nat.inv_pos_of_nat theorem

{n : ℕ} : 0 < ((n : α) + 1)⁻¹

Full source

theorem inv_pos_of_nat {n : ℕ} : 0 < ((n : α) + 1)⁻¹ :=
  inv_pos.2 <| add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one

Positivity of Inverse of Successor in Ordered Semifields

Informal description

For any natural number $n$ and any ordered semifield $\alpha$, the inverse of $(n + 1)$ in $\alpha$ is positive, i.e., $0 < (n + 1)^{-1}$.

Nat.one_div_pos_of_nat theorem

{n : ℕ} : 0 < 1 / ((n : α) + 1)

Full source

theorem one_div_pos_of_nat {n : ℕ} : 0 < 1 / ((n : α) + 1) := by
  rw [one_div]
  exact inv_pos_of_nat

Positivity of Reciprocal of Shifted Natural Number Cast in Ordered Semifields

Informal description

For any natural number $n$ and any ordered semifield $\alpha$, the reciprocal of $(n : \alpha) + 1$ is positive, i.e., $0 < \frac{1}{(n : \alpha) + 1}$.

Nat.one_div_le_one_div theorem

{n m : ℕ} (h : n ≤ m) : 1 / ((m : α) + 1) ≤ 1 / ((n : α) + 1)

Full source

theorem one_div_le_one_div {n m : ℕ} (h : n ≤ m) : 1 / ((m : α) + 1) ≤ 1 / ((n : α) + 1) := by
  refine one_div_le_one_div_of_le ?_ ?_
  · exact Nat.cast_add_one_pos _
  · simpa

Monotonicity of Reciprocal Function for Shifted Natural Number Casts

Informal description

For any natural numbers $n$ and $m$ with $n \leq m$, and for any ordered semifield $\alpha$, the inequality $\frac{1}{(m : \alpha) + 1} \leq \frac{1}{(n : \alpha) + 1}$ holds.

Nat.one_div_lt_one_div theorem

{n m : ℕ} (h : n < m) : 1 / ((m : α) + 1) < 1 / ((n : α) + 1)

Full source

theorem one_div_lt_one_div {n m : ℕ} (h : n < m) : 1 / ((m : α) + 1) < 1 / ((n : α) + 1) := by
  refine one_div_lt_one_div_of_lt ?_ ?_
  · exact Nat.cast_add_one_pos _
  · simpa

Strict Monotonicity of Reciprocals of Cast Natural Numbers in Ordered Semifields

Informal description

For any natural numbers $n$ and $m$ such that $n < m$, and for any ordered semifield $\alpha$, the reciprocal of $(m : \alpha) + 1$ is strictly less than the reciprocal of $(n : \alpha) + 1$, i.e., $\frac{1}{(m : \alpha) + 1} < \frac{1}{(n : \alpha) + 1}$.

Nat.one_div_cast_pos theorem

{n : ℕ} (hn : n ≠ 0) : 0 < 1 / (n : α)

Full source

theorem one_div_cast_pos {n : ℕ} (hn : n ≠ 0) : 0 < 1 / (n : α) :=
  one_div_pos.mpr (cast_pos.mpr (Nat.pos_of_ne_zero hn))

Positivity of Reciprocal of Nonzero Natural Number Cast in Ordered Semifield

Informal description

For any nonzero natural number $n$ (i.e., $n \neq 0$) and any ordered semifield $\alpha$, the reciprocal of the cast of $n$ into $\alpha$ is positive, i.e., $0 < \frac{1}{(n : \alpha)}$.

Nat.one_div_cast_nonneg theorem

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

Full source

theorem one_div_cast_nonneg (n : ℕ) : 0 ≤ 1 / (n : α) := one_div_nonneg.mpr (cast_nonneg' n)

Nonnegativity of Reciprocal of Natural Number Cast in Ordered Semifield

Informal description

For any natural number $n$ and any ordered semifield $\alpha$, the reciprocal of the canonical embedding of $n$ into $\alpha$ is nonnegative, i.e., $0 \leq \frac{1}{(n : \alpha)}$.

Nat.one_div_cast_ne_zero theorem

{n : ℕ} (hn : n ≠ 0) : 1 / (n : α) ≠ 0

Full source

theorem one_div_cast_ne_zero {n : ℕ} (hn : n ≠ 0) : 1 / (n : α) ≠ 0 :=
  _root_.ne_of_gt (one_div_cast_pos hn)

Nonzero Reciprocal of Nonzero Natural Number Cast in Ordered Semifield

Informal description

For any nonzero natural number $n$ (i.e., $n \neq 0$) and any ordered semifield $\alpha$, the reciprocal of the canonical embedding of $n$ into $\alpha$ is nonzero, i.e., $\frac{1}{(n : \alpha)} \neq 0$.

Main results