mathlib documentation

data.int.cast.field

Cast of integers into fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

@[norm_cast]
theorem int.cast_neg_nat_cast {R : Type u_1} [field R] (n : ) :

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

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

@[simp]
theorem int.cast_div {α : Type u_1} [field α] {m n : } (n_dvd : n m) (n_nonzero : n 0) :
(m / n) = m / n