Reference · Rationals

rainbow.math.rational.division

Rationalssrc/rainbow/math/rational/division.clj2 definitions, 3 theorems

Exact division of nonnegative rationals. The reciprocal of p/(q+1) is (q+1)/p; division is multiplication by the reciprocal. For a positive rational (numerator a successor), dividing it by itself is equivalent to one -- the cancellation law that underlies Newton steps, secant ratios, and normalization. Division by zero is total but junk (the reciprocal of 0 is not a genuine inverse), so the cancellation law is stated only for positive numerators.

nnrat/reciprocal :
  (x₁ : ℚ≥0)
  → ℚ≥0

nnrat/divide :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

nnrat/reciprocal-unfold :
  (value : ℚ≥0)
  → nnrat/reciprocal value = nnrat/make (nnrat/denominator value) (nat/predecessor (nnrat/numerator value))

nnrat/divide-unfold :
  (left right : ℚ≥0)
  → nnrat/divide left right = left · nnrat/reciprocal right

nnrat/divide-self-positive :
  (p q : ℕ)
  → nnrat/divide (nnrat/make (data/succ p) q) (nnrat/make (data/succ p) q) = 1