Reference · Non-negative rationals

rainbow.math.rational.nnrat.multiply-difference-zero

Non-negative rationalssrc/rainbow/math/rational/nnrat/multiply_difference_zero.clj0 definitions, 2 theorems

General nnrat discriminant (both-ordered case): nnrat/multiply-difference-zero-ordered : N1<=P1 -> N2<=P2 -> (P1*P2 + N1*N2 ~ P1*N2 + N1*P2) -> (P1 ~ N1) or (P2 ~ N2). With m1 = P1 monus N1, m2 = P2 monus N2 (so mi+Ni ~ Pi), the ring identity (m1+N1)(m2+N2) + N1*N2 ~ ((m1+N1)N2 + N1(m2+N2)) + m1*m2 exhibits m1*m2 as the gap; cancelling it gives m1*m2 ~ 0, and nnrat/multiply-zero-split splits it into m1~0 or m2~0, i.e. P1~N1 or P2~N2. Generalizes nnrat/square-difference-zero to distinct factors (the general no-zero-divisors core).

Depends onmath.rational.nnrat.multiply-zero-splitmath.rational.nnrat.identitiesmath.rational.nnrat.monusmath.rational.nnrat.add-cancel-zeromath.rational.nnrat.order-totalmath.rational.nnrat.ring

nnrat/multiply-difference-zero-ordered :
  (p1 n1 p2 n2 : ℚ≥0)
  (hle1 : n1 ≤ p1)
  (hle2 : n2 ≤ p2)
  (h : p1 · p2 + n1 · n2 = p1 · n2 + n1 · p2)
  → proposition/disjunction (p1 = n1) (p2 = n2)

nnrat/multiply-difference-zero :
  (p1 n1 p2 n2 : ℚ≥0)
  (h : p1 · p2 + n1 · n2 = p1 · n2 + n1 · p2)
  → proposition/disjunction (p1 = n1) (p2 = n2)