Reference · Natural numbers

rainbow.math.nat.square-zero

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

nat/square-zero-implies-zero : a*a = 0 -> a = 0. Nat.rec on a: base 0 is reflexivity; the successor case makes a*a a successor, so a*a=0 is succ(..)=0, refuted by zero-not-successor. Sub-brick (1) of the nnrat AM-GM discriminant for signed no-zero-divisors.

Depends onmath.nat.infinitemath.nat.semiring

nat/square-zero-implies-zero :
  (a : ℕ)
  (h : nat/multiply a a = 0)
  → a = 0