Reference · Signed rationals

rainbow.math.rational.signed.inverse-unique

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

B6f lever (replaces the awkward multiply-right-cancel): uniqueness of multiplicative inverse. signed/inverse-unique : u * w ~ 1 -> v * w ~ 1 -> u ~ v Pure field algebra, no positivity hypothesis: u ~ u*1 ~ u*(w*v) ~ (u*w)*v ~ 1*v ~ v. Signed rationals have no strict order in the corpus, so a strict multiply-right-cancel (a*c<=b*c, 0<c -> a<=b) is awkward to state and needs antisymmetry + equivalence-cancel; inverse-unique is the clean substitute the limit-reciprocal assembly actually needs: |1/(s n)|*|s n| ~ 1 (absolute-reciprocal-times-self) and reciprocal|s n|*|s n| ~ 1 (multiply-reciprocal-self) give |1/(s n)| ~ reciprocal|s n|, then reciprocal-antitone supplies the constant bound |1/(s n)| <= reciprocal(|L|/2) = 2/|L|. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.multiply-ringmath.rational.signed.multiply-associativemath.rational.signed.unit-lawsmath.rational.signed.equivalence-laws

signed/inverse-unique :
  (u v w : ℚ)
  (hu : u · w = 1)
  (hv : v · w = 1)
  → u = v