Cast of integers into fields

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

Main results

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

theorem Int.cast_neg_natCast {R : Type u_2} [DivisionRing R] (n : ℕ) : ↑(-↑n) = -↑n

Auxiliary lemma for norm_cast to move the cast -↑n upwards to ↑-↑n.

(The restriction to DivisionRing is necessary, otherwise this would also apply in the case where R = ℤ and cause nontermination.)

@[simp]

theorem Int.cast_div {α : Type u_1} [DivisionRing α] {m : ℤ} {n : ℤ} (n_dvd : n ∣ m) (n_nonzero : ↑n ≠ 0) : ↑(m / n) = ↑m / ↑n