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 #

theorem Nat.cast_inv_le_one {α : Type u_1} [LinearOrderedSemifield α] (n : ) :
(n)⁻¹ 1
theorem Nat.cast_div_le {α : Type u_1} [LinearOrderedSemifield α] {m : } {n : } :
(m / n) m / n

Natural division is always less than division in the field.

theorem Nat.inv_pos_of_nat {α : Type u_1} [LinearOrderedSemifield α] {n : } :
0 < (n + 1)⁻¹
theorem Nat.one_div_pos_of_nat {α : Type u_1} [LinearOrderedSemifield α] {n : } :
0 < 1 / (n + 1)
theorem Nat.one_div_le_one_div {α : Type u_1} [LinearOrderedSemifield α] {n : } {m : } (h : n m) :
1 / (m + 1) 1 / (n + 1)
theorem Nat.one_div_lt_one_div {α : Type u_1} [LinearOrderedSemifield α] {n : } {m : } (h : n < m) :
1 / (m + 1) < 1 / (n + 1)