Reference · Non-negative rationals

rainbow.math.rational.nnrat.product-reassociation

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

Associativity and factor reassociation for native nonnegative rationals.

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

nnrat/multiply-swap-right :
  (a b c : ℚ≥0)
  → a · b · c = a · c · b

nnrat/multiply-four-reorder :
  (a b c d : ℚ≥0)
  → a · b · (c · d) = a · c · (b · d)