Reference · Signed rationals

rainbow.math.rational.signed.equivalence-laws

Signed rationalssrc/rainbow/math/rational/signed/equivalence_laws.clj0 definitions, 2 theorems

Symmetry and negation transport for Grothendieck-pair signed equivalence.

signed/equivalent-symmetric :
  (left right : ℚ)
  (same : left = right)
  → right = left

signed/negate-respects-equivalence :
  (left right : ℚ)
  (same : left = right)
  → signed/negate left = signed/negate right