Reference · Non-negative rationals

rainbow.math.rational.nnrat.multiply-commute

Non-negative rationalssrc/rainbow/math/rational/nnrat/multiply_commute.clj0 definitions, 1 theorems

Standalone provider of nnrat/multiply-commutative (a*b ~ b*a), extracted so it can be chained WITHOUT nnrat_commutative's bundled nnrat/add-commutative, which alias-conflicts with nnrat_add_monotone's (different proof/sha). The proof is the same one as in nnrat_commutative: unfold to the cross product and reorder numerator and denominator with the native nat commutativity lemmas. Depends only on the d63 base (nnrat accessors, nat/multiply-commutative, nat congruence and transitivity). Native and axiom-free.

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