Reference · Non-negative rationals

rainbow.math.rational.nnrat.square-zero

Non-negative rationalssrc/rainbow/math/rational/nnrat/square_zero.clj0 definitions, 1 theorems

nnrat/square-zero : m*m ~ 0 -> m ~ 0. Sub-brick (2) of the AM-GM. nnrat-equivalent a zero unfolds to a nat equality (num a)*(den zero) = 0 with den zero = succ zero, so it is (num a)*1; strip the *1 (multiply-one-right), apply nat/square-zero-implies-zero to (num m)^2, then rebuild m ~ 0 by substituting num m = 0.

Depends onmath.nat.square-zeromath.nat.semiring

nnrat/square-zero :
  (m : ℚ≥0)
  (h : m · m = 0)
  → m = 0