Reference · Signed rationals

rainbow.math.rational.signed.add-associative

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

Associativity of signed-rational addition up to Grothendieck equivalence. (a + b) + c ~ a + (b + c) The unfolded signed equivalence is an equality, up to nnrat equivalence, of two six-summand cross sums. The verified nnrat ring normalizer constructs the proof from existing additive laws; the kernel checks the resulting term and the module introduces no axioms.

Depends onmath.rational.nnrat.ring

signed/add-associative :
  (a b c : ℚ)
  → a + b + c = a + (b + c)