Reference · Signed rationals

rainbow.math.rational.signed.product-radius-nonneg

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

First sub-proof of the limit-product modulus assembly: the radius base V = (1 + |L|) + |M| is nonnegative (indeed a sum of nonnegatives), so signed/from-nnrat-magnitude applies to it. Axiom-free; additive. analysis/product-radius-nonneg : forall L M, signed/nonnegative (signed-add (signed-add one (absolute L)) (absolute M))

Depends onmath.rational.signed.absolutemath.rational.signed.unit-lawsmath.linear.vector.norm-nonnegative

analysis/product-radius-nonneg :
  (L M : ℚ)
  → signed/nonnegative (1 + signed/absolute L + signed/absolute M)