Reference · Non-negative rationals

rainbow.math.rational.nnrat.map-sum-scale

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

Scalar pulls through a finite nnrat sum (scalar on the right), up to nnrat equivalence (~): nnrat/map-sum-scale-right : (map-sum f is) * c ~ map-sum (\i. f i * c) is The distributivity congruence (with Fubini) that moves a per-term factor in and out of the LP double sum. Right-multiplication is used deliberately so the proof needs only the installed right-distributivity (a+b)*c ~ a*c + b*c; the nil case 0*c ~ 0 reduces to eq-nat 0 0 (nat-multiply reduces 0*X to 0 on the left) so a bare nat reflexivity closes it -- no commutativity and no identities module, hence no clash on the nnrat/add-commutative or nnrat/multiply-one-left aliases (each defined by several modules). List.rec induction; polymorphic in the element type. Native and axiom-free; chains nnrat-map-sum-additive, nnrat-distributive on d63.

Depends onmath.rational.nnrat.map-sum-additivemath.rational.nnrat.distributive

nnrat/map-sum-scale-right.{u} :
  (A : Type u) (f : A → ℚ≥0) (c : ℚ≥0) (is : List A)
  → nnrat/map-sum A f is · c = nnrat/map-sum A (fun i => f i · c) is