Reference · Non-negative rationals

rainbow.math.rational.nnrat.square-positive

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

nnrat/square-positive : positive k -> positive (k*k). One step up the magnitude route to signed no-zero-divisors: nnrat/positive p reduces to strict-below 0 (numerator p), and numerator(k*k) is defeq numerator k * numerator k, so this is exactly nat/multiply-positive on the numerator.

Depends onmath.nat.multiply-positivemath.rational.nnrat.positive-monotone

nnrat/square-positive :
  (k : ℚ≥0) (hk : nnrat/positive k)
  → nnrat/positive (k · k)