Reference · Signed rationals

rainbow.math.rational.signed.scale-order

Signed rationalssrc/rainbow/math/rational/signed/scale_order.clj0 definitions, 1 theorems

Nonnegative-rational scaling preserves signed order. a <= b -> scale c a <= scale c b Signed order compares the two Grothendieck cross sums. Scaling turns each into the corresponding cross sum multiplied by c; the verified nnrat ring normalizer supplies those distributive equivalences and native nnrat multiplication monotonicity supplies the central inequality.

signed/scale-monotone :
  (rate : ℚ≥0) (left right : ℚ)
  (ordered : left ≤ right)
  → signed/scale rate left ≤ signed/scale rate right