Reference · Signed rationals

rainbow.math.rational.signed.square-zero

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

A signed rational whose square is zero is itself zero. signed/square-zero-reflects : x*x ~ 0 -> x ~ 0 For x=(p,n), signed multiplication exposes the two components positive(x*x) = p*p + n*n negative(x*x) = p*n + n*p. Equivalence of x*x with signed zero is therefore the quadratic equality proved by nnrat/quadratic-equality-reflects, modulo the zero padding in the Grothendieck relation. Native and axiom-free.

Depends onmath.rational.nnrat.quadratic-zero

signed/square-zero-reflects :
  (value : ℚ)
  (zero-square : value · value = 0)
  → value = 0