Reference · Non-negative rationals

rainbow.math.rational.nnrat.distributive

Non-negative rationalssrc/rainbow/math/rational/nnrat/distributive.clj0 definitions, 2 theorems

Right-distributivity of nonnegative-rational multiplication over addition, up to nnrat equivalence: multiply-distributes-add-right : (a + b) * m ~ a*m + b*m (all a b m) This is the last algebra brick for the convex-combination bound. The proof is the first real payoff of the nat-ring tactic (rainbow.math.nat.ring): nnrat/equivalent unfolds to a nat cross-product equality numL*denR = numR*denL whose two sides are degree-7 monomial sums that agree only after full semiring reordering. We 1. transport the packed product-denominators succ(combine ..) to product form (da*dm etc.) with the nnrat/denominator-combine law + congruence, 2. discharge the resulting pure product/sum identity with nat-ring/prove-nat-eq (which normalizes both sides to a canonical sum of monomials), 3. transport the denominators back on the other side. Native and axiom-free; chains rainbow.math.nat.ring and nonnegative-rational (d63).

nnrat/multiply-distributes-add-right :
  (a b m : ℚ≥0)
  → (a + b) · m = a · m + b · m

nnrat/multiply-one-left :
  (x : ℚ≥0)
  → 1 · x = x