rainbow.math.sums.boolean-predicate

The converse of the existing zero/one polynomial lemma, for predicate adapters.

signed/boolean-cases-implies-polynomial

TheoremFor all inputsNo axiomsSource

signed/boolean-cases-implies-polynomial :
  (x : ℚ) (binary : proposition/disjunction (x = 0) (x = 1))
  → x · (1 + signed/negate x) = 0

+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRational