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 {K : Type u_1} [DivisionSemiring K] {m n : ℕ} (hnm : n ∣ m) (hn : ↑n ≠ 0) : ↑(m / n) = ↑m / ↑n

@[simp]

theorem Nat.cast_div_charZero {K : Type u_1} [DivisionSemiring K] {m n : ℕ} [CharZero K] (hnm : n ∣ m) : ↑(m / n) = ↑m / ↑n

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