Documentation

Mathlib.Data.Nat.Cast.Order.Field

Cast of naturals into ordered fields #

This file concerns the canonical homomorphism ℕ → F, where F is a LinearOrderedSemifield.

Main results #

source
theorem Nat.cast_inv_le_one {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (n : ℕ) :
(↑n)⁻¹ ≤ 1
source
theorem Nat.cast_div_le {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {m n : ℕ} :
↑(m / n) ≤ ↑m / ↑n

Natural division is always less than division in the field.

source
theorem Nat.inv_pos_of_nat {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℕ} :
0 < (↑n + 1)⁻¹
source
theorem Nat.one_div_pos_of_nat {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℕ} :
0 < 1 / (↑n + 1)
source
theorem Nat.one_div_le_one_div {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n m : ℕ} (h : n ≤ m) :
1 / (↑m + 1) ≤ 1 / (↑n + 1)
source
theorem Nat.one_div_lt_one_div {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n m : ℕ} (h : n < m) :
1 / (↑m + 1) < 1 / (↑n + 1)
source
theorem Nat.one_div_cast_pos {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℕ} (hn : n ≠ 0) :
0 < 1 / ↑n
source
theorem Nat.one_div_cast_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (n : ℕ) :
0 ≤ 1 / ↑n
source
theorem Nat.one_div_cast_ne_zero {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℕ} (hn : n ≠ 0) :
1 / ↑n ≠ 0
source
theorem Nat.one_sub_one_div_cast_nonneg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [AddRightMono α] (n : ℕ) :
0 ≤ 1 - 1 / ↑n
source
theorem Nat.one_sub_one_div_cast_le_one {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [AddLeftMono α] (n : ℕ) :
1 - 1 / ↑n ≤ 1