Reference · Signed rationals

rainbow.math.rational.signed.scale-additive

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

Nonnegative-rational scaling distributes over signed addition up to Grothendieck equivalence. scale c (a + b) ~ scale c a + scale c b After unfolding, both sides of signed equivalence are the same four scaled components under different addition trees. The verified nnrat ring normalizer constructs the proof; the kernel checks it without axioms.

signed/scale-additive :
  (rate : ℚ≥0) (left right : ℚ)
  → signed/scale rate (left + right) = signed/scale rate left + signed/scale rate right