Cast of naturals into fields

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

Main results

• Nat.cast_div: if n divides m, then ↑(m / n) = ↑m / ↑n

@[simp]

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

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