Formal target: Corpus.WikipediaAgrawal.agrawal_conjecture.variants.popovych

**Roman B.

Exact formal statement

∀ (n r : Nat),
  GT.gt.{0} n 1 →
    GT.gt.{0} r 0 →
      Eq.{1} (n.gcd r) 1 →
        let R := Polynomial.{0} (ZMod n);
        let X := Polynomial.X.{0};
        let I := Ideal.span.{0} (Singleton.singleton.{0, 0} (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} X r) 1));
        Eq.{1} (DFunLike.coe.{1, 1, 1} (Ideal.Quotient.mk.{0} I) (HPow.hPow.{0, 0, 0} (HSub.hSub.{0, 0, 0} X 1) n))
            (DFunLike.coe.{1, 1, 1} (Ideal.Quotient.mk.{0} I) (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} X n) 1)) →
          Eq.{1} (DFunLike.coe.{1, 1, 1} (Ideal.Quotient.mk.{0} I) (HPow.hPow.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} X 2) n))
              (DFunLike.coe.{1, 1, 1} (Ideal.Quotient.mk.{0} I) (HAdd.hAdd.{0, 0, 0} (HPow.hPow.{0, 0, 0} X n) 2)) →
            Or (Nat.Prime n) (Eq.{1} (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) 2) 1)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record