Reference · Signed rationals

rainbow.math.rational.signed.square-of-sum

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

The four-term expansion of a squared sum over signed rationals -- a reusable step for square convexity (the variance inequality) and other quadratic identities. signed/square-of-sum : (a+b)*(a+b) ~ ((a*a) + (a*b)) + ((b*a) + (b*b)) One right-distribution then two left-distributions. (a*b and b*a are kept distinct since the caller decides when to commute.) Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.distributivemath.linear.matrix.action-scalemath.rational.signed.map-sum-algebramath.rational.signed.equivalence-laws

signed/square-of-sum :
  (a b : ℚ)
  → (a + b) · (a + b) = a · a + a · b + (b · a + b · b)