Reference · Signed rationals

rainbow.math.rational.signed.scale-composition

Signed rationalssrc/rainbow/math/rational/signed/scale_composition.clj0 definitions, 1 theorems

Composition of nonnegative scaling on signed rationals. scale outer (scale inner value) ~ scale (outer * inner) value The two Grothendieck components differ only by nnrat multiplication association. The verified nnrat ring normalizer emits the proof term.

signed/scale-composition :
  (outer inner : ℚ≥0) (value : ℚ)
  → signed/scale outer (signed/scale inner value) = signed/scale (outer · inner) value