Reference · Signed rationals

rainbow.math.rational.signed.multiply-nonzero

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

General signed no-zero-divisors: signed/multiply-zero-split : (a*b ~ 0) -> (a ~ 0) or (b ~ 0) signed/multiply-nonzero : not(a ~ 0) -> not(b ~ 0) -> not(a*b ~ 0). The signed pair unfolds a*b ~ 0 to (Pa*Pb + Na*Nb) ~ (Pa*Nb + Na*Pb), which is exactly the hypothesis of nnrat/multiply-difference-zero, giving Pa~Na or Pb~Nb, i.e. a~0 or b~0. This is the general no-zero-divisors that strict convexity needs for the weight product (generalizes signed/square-nonzero to distinct factors).

Depends onmath.rational.nnrat.multiply-difference-zeromath.rational.nnrat.identitiesmath.linear.matrix.action-scalemath.rational.signed.equivalence-laws

signed/multiply-zero-split :
  (a b : ℚ)
  (hab : a · b = 0)
  → proposition/disjunction (a = 0) (b = 0)

signed/multiply-nonzero :
  (a b : ℚ) (ha : proposition/negation (a = 0)) (hb : proposition/negation (b = 0))
  → proposition/negation (a · b = 0)