Cast of integers into fields #
This file concerns the canonical homomorphism ℤ → F
, where F
is a field.
Main results #
int.cast_div
: ifn
dividesm
, then↑(m / n) = ↑m / ↑n
data.int.cast_field
This file concerns the canonical homomorphism ℤ → F
, where F
is a field.
int.cast_div
: if n
divides m
, then ↑(m / n) = ↑m / ↑n