Reference · Signed rationals

rainbow.math.rational.signed.negate-additive

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

Signed negation distributes over addition up to signed equivalence. -(a + b) ~ (-a) + (-b) Both sides reduce to the same Grothendieck pair: negation swaps the positive and negative sums, while adding the two negated inputs builds those same sums. Signed equivalence reflexivity therefore supplies the proof.

signed/negate-additive :
  (left right : ℚ)
  → signed/negate (left + right) = signed/negate left + signed/negate right