Theorem Marketplace

Theorem Details

import Mathlib

-- https://mathoverflow.net/questions/339137/why-do-polynomials-with-coefficients-0-1-like-to-have-only-factors-with-0-1
theorem polynomial_coeff_zero_one_of_mul (p q : Polynomial ℝ) (h : ∀ i, (p * q).coeff i = 0 ∨ (p * q).coeff i = 1) : 
    ∀ i, p.coeff i = 0 ∨ p.coeff i = 1 := 
  sorry

Bounty: 0.0004 ETH

Status: Open

Submit Your Proof

Back to Bounties