Reference · Signed rationals

rainbow.math.rational.signed.multiply-positive

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

signed/multiply-positive : 0 < a -> 0 < b -> 0 < a*b. From 0<a extract 0<=a and not(0~a) (less-than is the reducible conjunction of the two); a*b is nonnegative (multiply-nonnegative) and nonzero (multiply-nonzero applied to the distinctness facts), so less-than-intro gives 0 < a*b. The strict-positivity payoff of the general no-zero-divisors chain -- feeds the strict-convexity capstone (0 < w0*w1*(x-y)^2).

Depends onmath.rational.signed.multiply-nonzeromath.rational.signed.multiply-ordermath.rational.signed.strict-order

signed/multiply-positive :
  (a b : ℚ)
  (ha : 0 < a)
  (hb : 0 < b)
  → 0 < a · b