Cast of naturals into fields #
This file concerns the canonical homomorphism ℕ → F→ F
, where F
is a field.
Main results #
Nat.cast_div
: ifn
dividesm
, then↑(m / n) = ↑m / ↑n↑(m / n) = ↑m / ↑n↑m / ↑n↑n
Nat.cast_div_le
: in all cases,↑(m / n) ≤ ↑m / ↑ n↑(m / n) ≤ ↑m / ↑ n≤ ↑m / ↑ n↑m / ↑ n↑ n
Natural division is always less than division in the field.