Reference · Non-negative rationals

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

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

The nnrat AM-GM discriminant, ordered case: nnrat/square-difference-zero-ordered : N<=P -> (P*P + N*N ~ P*N + N*P) -> P ~ N. Let m = P monus N, so (m+N) ~ P (monus-add-cancel). Transport the hypothesis to the (m+N) form; the ring identity (m+N)^2 + N^2 ~ ((m+N)N + N(m+N)) + m*m then exhibits m*m as the gap, and cancelling it (add-cancel-to-zero) gives m*m ~ 0, hence m ~ 0 (nnrat/square-zero), hence P ~ N. The unordered version wraps this with at-most-total.

Depends onmath.rational.nnrat.square-zeromath.rational.nnrat.identitiesmath.rational.nnrat.monusmath.rational.nnrat.add-cancel-zeromath.rational.nnrat.order-totalmath.rational.nnrat.ring

nnrat/square-difference-zero-ordered :
  (p n : ℚ≥0)
  (hle : n ≤ p)
  (h : p · p + n · n = p · n + n · p)
  → p = n

nnrat/square-difference-zero :
  (p n : ℚ≥0)
  (h : p · p + n · n = p · n + n · p)
  → p = n