Formal target: Corpus.Mathoverflow339137.mathoverflow_339137

Let $P(x), Q(x) ∈ ℝ[x]$ be two monic polynomials with non-negative coefficients.

Exact formal statement

∀ (P Q R : Polynomial.{0} Real),
  Polynomial.Monic.{0} P →
    Polynomial.Monic.{0} Q →
      (∀ (c : Real), Membership.mem.{0, 0} (Polynomial.coeffs.{0} P) c → LE.le.{0} 0 c) →
        (∀ (c : Real), Membership.mem.{0, 0} (Polynomial.coeffs.{0} Q) c → LE.le.{0} 0 c) →
          Eq.{1} R (HMul.hMul.{0, 0, 0} P Q) →
            Corpus.Mathoverflow339137.IsZeroOne R →
              And (Corpus.Mathoverflow339137.IsZeroOne P) (Corpus.Mathoverflow339137.IsZeroOne Q)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record