Reference · Signed rationals

rainbow.math.rational.signed.square-nonzero

Signed rationalssrc/rainbow/math/rational/signed/square_nonzero.clj0 definitions, 2 theorems

signed/square-nonzero : not(d ~ 0) -> not(d*d ~ 0). The signed pair unfolds d*d ~ 0 to pos(d*d) ~ neg(d*d), i.e. (Pd*Pd + Nd*Nd) ~ (Pd*Nd + Nd*Pd) (modulo add-zero), which is exactly nnrat/square-difference-zero's input, giving Pd ~ Nd, i.e. d ~ 0 -- contradicting the premise. Core of signed no-zero-divisors for the square case (what strict convexity needs).

Depends onmath.rational.nnrat.square-difference-zeromath.rational.nnrat.identitiesmath.linear.matrix.action-scalemath.rational.signed.strict-ordermath.rational.signed.multiply-ordermath.rational.signed.equivalence-lawsmath.linear.vector.norm-nonnegative

signed/square-nonzero :
  (d : ℚ) (hd : proposition/negation (d = 0))
  → proposition/negation (d · d = 0)

signed/square-positive :
  (d : ℚ) (hd : proposition/negation (d = 0))
  → 0 < d · d