Cast of naturals into fields

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

Main results

• Nat.cast_div: if n divides m, then ↑(m / n) = ↑m / ↑n↑(m / n) = ↑m / ↑n↑m / ↑n↑n
• Nat.cast_div_le: in all cases, ↑(m / n) ≤ ↑m / ↑ n↑(m / n) ≤ ↑m / ↑ n≤ ↑m / ↑ n↑m / ↑ n↑ n

ink

@[simp]

theorem Nat.cast_div {α : Type u_1} [inst : DivisionSemiring α] {m : ℕ} {n : ℕ} (n_dvd : n ∣ m) (n_nonzero : ↑n ≠ 0) : ↑(m / n) = ↑m / ↑n

ink

theorem Nat.cast_div_div_div_cancel_right {α : Type u_1} [inst : DivisionSemiring α] [inst : CharZero α] {m : ℕ} {n : ℕ} {d : ℕ} (hn : d ∣ n) (hm : d ∣ m) : ↑(m / d) / ↑(n / d) = ↑m / ↑n

ink

theorem Nat.cast_div_le {α : Type u_1} [inst : LinearOrderedSemifield α] {m : ℕ} {n : ℕ} : ↑(m / n) ≤ ↑m / ↑n

Natural division is always less than division in the field.

ink

theorem Nat.inv_pos_of_nat {α : Type u_1} [inst : LinearOrderedSemifield α] {n : ℕ} : 0 < (↑n + 1)⁻¹

ink

theorem Nat.one_div_pos_of_nat {α : Type u_1} [inst : LinearOrderedSemifield α] {n : ℕ} : 0 < 1 / (↑n + 1)

ink

theorem Nat.one_div_le_one_div {α : Type u_1} [inst : LinearOrderedSemifield α] {n : ℕ} {m : ℕ} (h : n ≤ m) : 1 / (↑m + 1) ≤ 1 / (↑n + 1)

ink

theorem Nat.one_div_lt_one_div {α : Type u_1} [inst : LinearOrderedSemifield α] {n : ℕ} {m : ℕ} (h : n < m) : 1 / (↑m + 1) < 1 / (↑n + 1)