Reference · Signed rationals

rainbow.math.rational.signed.absolute-multiply

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

Brick 3 of limit-product: |a * b| ~ |a| * |b| over signed rationals. signed/absolute-multiply : seqv (|a*b|) (|a|*|b|), by a four-way sign case-split (nested Bool.rec on decide-at-most 0 a and 0 b). In each quadrant the sign of a*b is fixed by the multiply-sign lemmas (multiply-nonnegative / -nonnegative-nonpositive / -nonpositive), |a*b| collapses via absolute-of-nonnegative/-nonpositive, and |a|*|b| is rewritten to the same normal form using absolute-of-sign + multiply-negate. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.multiply-ordermath.rational.signed.absolute-signmath.rational.signed.multiply-ringmath.linear.vector.dot-negate

signed/absolute-multiply :
  (a b : ℚ)
  → signed/absolute (a · b) = signed/absolute a · signed/absolute b