Formal target: Corpus.Erdos477.erdos_477.variants.X_pow_three

Probably there is no such $A$ for the polynomial $X^3$.

Exact formal statement

∀ (A : Set.{0} Int),
  Exists.{1} fun z =>
    Not
      (ExistsUnique.{1} fun a =>
        And
          (Membership.mem.{0, 0}
            (SProd.sprod.{0, 0, 0} A
              (Set.range.{0, 1} fun x => Polynomial.eval.{0} x (HPow.hPow.{0, 0, 0} Polynomial.X.{0} 3)))
            a)
          (Eq.{1} z (HAdd.hAdd.{0, 0, 0} (Prod.fst.{0, 0} a) (Prod.snd.{0, 0} a))))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record