Reference · Signed rationals

rainbow.math.rational.signed.multiply-ring

Signed rationalssrc/rainbow/math/rational/signed/multiply_ring.clj0 definitions, 5 theorems

Signed multiplication is commutative and well defined on the Grothendieck quotient. signed/multiply-commutative a*b ~ b*a signed/multiply-left-respects-equivalence b~b' -> c*b ~ c*b' signed/multiply-right-respects-equivalence a~a' -> a*c ~ a'*c signed/multiply-respects-equivalence a~a' -> b~b' -> a*b ~ a'*b' signed/multiply-zero-right a*0 ~ 0 Well-definedness is the one that matters: a signed rational is a PAIR, and `signed/equivalent` is a quotient relation on pairs, so until multiplication is shown to respect it, no signed product may be rewritten under an equivalence -- which blocks every reassociation inside a weighted sum. Commutativity and the zero law are pure semiring identities on the four component products, so each is a single `rainbow.math.rational.nnrat.ring` call. The one-sided congruence is the only proof with real content: it factors the fixed factor OUT of the four component products, (Pc*Pb + Nc*Nb) + (Pc*Nb' + Nc*Pb') ~ (Pb + Nb')*Pc + (Nb + Pb')*Nc -- itself a ring identity -- at which point the hypothesis `Pb + Nb' ~ Pb' + Nb` rewrites both of those sums to the same thing. The other side of the goal factors to the identical expression, so the two meet in the middle. The right-hand and two-sided versions then follow by commutativity and `signed/equivalent-transitive`. Native and axiom-free; chains the nnrat-ring tactic and the signed finite-sum algebra (for signed equivalence transitivity) on D63.

Depends onmath.rational.nnrat.ringmath.rational.signed.map-sum-algebra

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

signed/multiply-left-respects-equivalence :
  (b bh c : ℚ)
  (same : b = bh)
  → c · b = c · bh

signed/multiply-right-respects-equivalence :
  (a ah c : ℚ)
  (same : a = ah)
  → a · c = ah · c

signed/multiply-respects-equivalence :
  (a ah b bh : ℚ)
  (same-a : a = ah)
  (same-b : b = bh)
  → a · b = ah · bh

signed/multiply-zero-right :
  (a : ℚ)
  → a · 0 = 0