Reference · Non-negative rationals

rainbow.math.rational.nnrat.distribute-right

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

Right-distributivity of nonnegative-rational multiplication over addition, carrying ONLY that law. nnrat/multiply-distributes-add-right : (a + b) * m ~ a*m + b*m This is a verbatim copy of the spec in `rainbow.math.rational.nnrat.distributive`, split out so that consumers can take the distributive law WITHOUT also taking that module's `nnrat/multiply-one-left`. Both `nnrat-distributive` and `nnrat-identities` declare `nnrat/multiply-one-left` with different proof terms, so chaining the two is a kernel alias conflict -- which in turn made the nnrat rearrangement toolkit (needing distributivity) and the signed limit / Lagrangian stack (needing identities, via signed-limit-uniqueness) mutually exclusive. Because the spec here is character-identical to the original, it elaborates to the same content id, so chaining this module alongside `nnrat-distributive` is also safe. Native and axiom-free; chains rainbow.math.nat.ring on D63.

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