Cast of naturals into fields #

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

Main results #

@[simp]

theorem nat.cast_div {α : Type u_1} [field α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : ↑n ≠ 0) :

theorem nat.cast_div_le {α : Type u_1} [linear_ordered_semifield α] {m n : ℕ} :

Natural division is always less than division in the field.

theorem nat.inv_pos_of_nat {α : Type u_1} [linear_ordered_semifield α] {n : ℕ} :

theorem nat.one_div_pos_of_nat {α : Type u_1} [linear_ordered_semifield α] {n : ℕ} :

0 < 1 / (↑n + 1)

theorem nat.one_div_le_one_div {α : Type u_1} [linear_ordered_semifield α] {n m : ℕ} (h : n ≤ m) :

1 / (↑m + 1) ≤ 1 / (↑n + 1)

theorem nat.one_div_lt_one_div {α : Type u_1} [linear_ordered_semifield α] {n m : ℕ} (h : n < m) :

1 / (↑m + 1) < 1 / (↑n + 1)