Reference · Non-negative rationals

rainbow.math.rational.nnrat.commutative

Non-negative rationalssrc/rainbow/math/rational/nnrat/commutative.clj0 definitions, 3 theorems

Native commutativity of nonnegative-rational addition and multiplication, up to cross-multiplication equivalence. These make the exact-rational base a commutative structure and are the first general (non-worked-instance) rational algebra laws, assembled from the native nat commutativity lemmas. They let later signed and operations-research proofs reorder sums and products.

nnrat/add-commutative :
  (a b : ℚ≥0)
  → a + b = b + a

nnrat/multiply-commutative :
  (a b : ℚ≥0)
  → a · b = b · a

signed/add-commutative :
  (a b : ℚ)
  → a + b = b + a