Mathlib.Data.Nat.Cast.Order.Ring

Nat.cast_nonneg theorem

{α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (n : ℕ) : 0 ≤ (n : α)

Full source

/-- Specialisation of `Nat.cast_nonneg'`, which seems to be easier for Lean to use. -/
@[simp]
theorem cast_nonneg {α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (n : ℕ) : 0 ≤ (n : α) :=
  cast_nonneg' n

Nonnegativity of Natural Number Cast in Ordered Semirings

Informal description

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

Nat.ofNat_nonneg theorem

{α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (n : ℕ) [n.AtLeastTwo] : 0 ≤ (ofNat(n) : α)

Full source

/-- Specialisation of `Nat.ofNat_nonneg'`, which seems to be easier for Lean to use. -/
@[simp]
theorem ofNat_nonneg {α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (n : ℕ) [n.AtLeastTwo] :
    0 ≤ (ofNat(n) : α) :=
  ofNat_nonneg' n

Nonnegativity of Canonical Embedding for $n \geq 2$ in Ordered Semirings

Informal description

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

Nat.cast_min theorem

{α} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ) : (↑(min m n : ℕ) : α) = min (m : α) n

Full source

@[simp, norm_cast]
theorem cast_min {α} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ) :
    (↑(min m n : ℕ) : α) = min (m : α) n :=
  (@mono_cast α _).map_min

Embedding Preserves Minimum of Natural Numbers

Informal description

Let $\alpha$ be a semiring with a linear order and a strictly ordered ring structure. For any natural numbers $m$ and $n$, the canonical embedding of $\min(m, n)$ into $\alpha$ equals the minimum of the embeddings of $m$ and $n$ in $\alpha$, i.e., $\min(m, n) = \min(m, n)$.

Nat.cast_max theorem

{α} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ) : (↑(max m n : ℕ) : α) = max (m : α) n

Full source

@[simp, norm_cast]
theorem cast_max {α} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ) :
    (↑(max m n : ℕ) : α) = max (m : α) n :=
  (@mono_cast α _).map_max

Maximum Preservation under Natural Number Cast

Informal description

Let $\alpha$ be a semiring with a linear order and a strictly ordered ring structure. For any natural numbers $m$ and $n$, the canonical embedding of $\max(m, n)$ into $\alpha$ is equal to the maximum of the embeddings of $m$ and $n$ in $\alpha$, i.e., $\max(m, n) = \max(m, n)$.

Nat.cast_pos theorem

{α} [Semiring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] {n : ℕ} : (0 : α) < n ↔ 0 < n

Full source

/-- Specialisation of `Nat.cast_pos'`, which seems to be easier for Lean to use. -/
@[simp]
theorem cast_pos {α} [Semiring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] {n : ℕ} :
    (0 : α) < n ↔ 0 < n := cast_pos'

Positivity of Natural Number Cast in Ordered Semiring

Informal description

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

Nat.ofNat_pos' theorem

{n : ℕ} [n.AtLeastTwo] : 0 < (ofNat(n) : α)

Full source

/-- See also `Nat.ofNat_pos`, specialised for an `OrderedSemiring`. -/
@[simp low]
theorem ofNat_pos' {n : ℕ} [n.AtLeastTwo] : 0 < (ofNat(n) : α) :=
  cast_pos'.mpr (NeZero.pos n)

Positivity of Canonical Embedding for Natural Numbers $\geq 2$ in Ordered Semirings

Informal description

For any natural number $n \geq 2$ and any ordered semiring $\alpha$, the canonical embedding of $n$ into $\alpha$ is positive, i.e., $0 < (n : \alpha)$.

Nat.ofNat_pos theorem

{α} [Semiring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] {n : ℕ} [n.AtLeastTwo] : 0 < (ofNat(n) : α)

Full source

/-- Specialisation of `Nat.ofNat_pos'`, which seems to be easier for Lean to use. -/
@[simp]
theorem ofNat_pos {α} [Semiring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α]
    {n : ℕ} [n.AtLeastTwo] :
    0 < (ofNat(n) : α) :=
  ofNat_pos'

Positivity of Canonical Embedding for Natural Numbers $\geq 2$ in Nontrivial Ordered Semirings

Informal description

For any ordered semiring $\alpha$ that is nontrivial and any natural number $n \geq 2$, the canonical embedding of $n$ into $\alpha$ is positive, i.e., $0 < n$ in $\alpha$.

Nat.cast_tsub theorem

 [CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α]
  [AddLeftReflectLE α] (m n : ℕ) : ↑(m - n) = (m - n : α)

Full source

/-- A version of `Nat.cast_sub` that works for `ℝ≥0` and `ℚ≥0`. Note that this proof doesn't work
for `ℕ∞` and `ℝ≥0∞`, so we use type-specific lemmas for these types. -/
@[simp, norm_cast]
theorem cast_tsub [CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α]
    [Sub α] [OrderedSub α] [AddLeftReflectLE α] (m n : ℕ) : ↑(m - n) = (m - n : α) := by
  rcases le_total m n with h | h
  · rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]
    exact mono_cast h
  · rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩
    rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]

Embedding Preserves Subtraction in Canonically Ordered Semirings

Informal description

Let $\alpha$ be a commutative semiring with a partial order, which is an ordered ring and a canonically ordered additive monoid. Suppose $\alpha$ has subtraction and satisfies the ordered subtraction property, and addition reflects the order relation (i.e., $a + c \leq b + c$ implies $a \leq b$). Then for any natural numbers $m$ and $n$, the canonical embedding of $m - n$ into $\alpha$ equals the subtraction of the embeddings, i.e., $(m - n : \alpha) = (m : \alpha) - (n : \alpha)$.

Nat.abs_cast theorem

(n : ℕ) : |(n : R)| = n

Full source

@[simp, norm_cast]
theorem abs_cast (n : ℕ) : |(n : R)| = n := abs_of_nonneg n.cast_nonneg

Absolute Value of Natural Number Cast in Ordered Semirings

Informal description

For any natural number $n$ and any ordered semiring $R$, the absolute value of the canonical embedding of $n$ into $R$ equals $n$, i.e., $|(n : R)| = n$.

Nat.abs_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : |(ofNat(n) : R)| = ofNat(n)

Full source

@[simp]
theorem abs_ofNat (n : ℕ) [n.AtLeastTwo] : |(ofNat(n) : R)| = ofNat(n) := abs_cast n

Absolute Value of Canonical Embedding for Natural Numbers $\geq 2$

Informal description

For any natural number $n$ (with $n \geq 2$) and any ordered semiring $R$, the absolute value of the canonical embedding of $n$ into $R$ equals $n$, i.e., $|(n : R)| = n$.

Nat.neg_cast_eq_cast theorem

: (-m : R) = n ↔ m = 0 ∧ n = 0

Full source

@[simp, norm_cast] lemma neg_cast_eq_cast : (-m : R) = n ↔ m = 0 ∧ n = 0 := by
  simp [neg_eq_iff_add_eq_zero, ← cast_add]

Negation of Natural Number Cast Equals Zero Condition

Informal description

For any natural number $m$ and element $n$ in an ordered semiring $R$, the negation of the cast of $m$ equals $n$ if and only if both $m$ and $n$ are zero, i.e., $-m = n \leftrightarrow m = 0 \land n = 0$.

Nat.cast_eq_neg_cast theorem

: (m : R) = -n ↔ m = 0 ∧ n = 0

Full source

@[simp, norm_cast] lemma cast_eq_neg_cast : (m : R) = -n ↔ m = 0 ∧ n = 0 := by
  simp [eq_neg_iff_add_eq_zero, ← cast_add]

Equality of Natural Number Cast and its Negation: $(m : R) = -n \leftrightarrow m = n = 0$

Informal description

For any natural numbers $m$ and $n$, and any ordered semiring $R$, the cast of $m$ in $R$ equals the negation of the cast of $n$ if and only if both $m$ and $n$ are zero, i.e., $(m : R) = -n \leftrightarrow m = 0 \land n = 0$.

Nat.mul_le_pow theorem

{a : ℕ} (ha : a ≠ 1) (b : ℕ) : a * b ≤ a ^ b

Full source

lemma mul_le_pow {a : ℕ} (ha : a ≠ 1) (b : ℕ) :
    a * b ≤ a ^ b := by
  induction b generalizing a with
  | zero => simp
  | succ b hb =>
    rw [mul_add_one, pow_succ]
    rcases a with (_|_|a)
    · simp
    · simp at ha
    · rw [mul_add_one, mul_add_one, add_comm (_ * a), add_assoc _ (_ * a)]
      rcases b with (_|b)
      · simp [add_assoc, add_comm]
      refine add_le_add (hb (by simp)) ?_
      rw [pow_succ']
      refine (le_add_left ?_ ?_).trans' ?_
      exact le_mul_of_one_le_right' (one_le_pow _ _ (by simp))

Inequality between product and power: $a \cdot b \leq a^b$ for $a \neq 1$

Informal description

For any natural numbers $a \neq 1$ and $b$, the product $a \cdot b$ is less than or equal to $a^b$.

Nat.two_mul_sq_add_one_le_two_pow_two_mul theorem

(k : ℕ) : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Full source

lemma two_mul_sq_add_one_le_two_pow_two_mul (k : ℕ) : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k) := by
  induction k with
  | zero => simp
  | succ k hk =>
    rw [add_pow_two, one_pow, mul_one, add_assoc, mul_add, add_right_comm]
    refine (add_le_add_right hk _).trans ?_
    rw [mul_add 2 k, pow_add, mul_one, pow_two, ← mul_assoc, mul_two, mul_two, add_assoc]
    gcongr
    rw [← two_mul, ← pow_succ']
    exact le_add_of_le_right (mul_le_pow (by simp) _)

Inequality: $2k^2 + 1 \leq 2^{2k}$ for natural numbers $k$

Informal description

For any natural number $k$, the inequality $2k^2 + 1 \leq 2^{2k}$ holds.