Cast of naturals into ordered fields #
This file concerns the canonical homomorphism ℕ → F
, where F
is a LinearOrderedSemifield
.
Main results #
Nat.cast_div_le
: in all cases,↑(m / n) ≤ ↑m / ↑ n
This file concerns the canonical homomorphism ℕ → F
, where F
is a LinearOrderedSemifield
.
Nat.cast_div_le
: in all cases, ↑(m / n) ≤ ↑m / ↑ n