Reference · Non-negative rationals

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

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

nnrat/multiply-zero-split : m1*m2 ~ 0 -> (m1 ~ 0) or (m2 ~ 0). nnrat-equivalent x 0 unfolds to (num x)*1 = 0, and num(m1*m2) = (num m1)*(num m2), so the hypothesis strips to (num m1)*(num m2) = 0; nat/multiply-zero-split splits it, and each nat disjunct is rebuilt into an nnrat equivalence by the same substitution nnrat/square-zero uses. Generalizes nnrat/square-zero to distinct factors.

Depends onmath.nat.multiply-zero-splitmath.nat.semiring

nnrat/multiply-zero-split :
  (m1 m2 : ℚ≥0)
  (h : m1 · m2 = 0)
  → proposition/disjunction (m1 = 0) (m2 = 0)