Reference · Natural numbers

rainbow.math.nat.multiply-zero-split

Natural numberssrc/rainbow/math/nat/multiply_zero_split.clj0 definitions, 1 theorems

nat/multiply-zero-split : a*b = 0 -> (a = 0) or (b = 0). Nested Nat.rec: a=0 gives the left disjunct; a=succ p with b=0 gives the right disjunct; a=succ p, b=succ q makes (succ p)*(succ q) a successor, so =0 is refuted. The general nat no-zero-divisors -- foundation for the general nnrat/signed no-zero-divisors that strict convexity needs (generalizes nat/square-zero-implies-zero).

Depends onmath.nat.infinitemath.nat.semiring

nat/multiply-zero-split :
  (a b : ℕ)
  (h : nat/multiply a b = 0)
  → proposition/disjunction (a = 0) (b = 0)