Formal target: Corpus.OEIS2454.conjecture

Let $\zeta$ be a primitive $(2n+1)$-th root of unity.

Exact formal statement

∀ (n : Nat),
  have N := HMul.hMul.{0, 0, 0} 2 n;
  have K := HAdd.hAdd.{0, 0, 0} N 1;
  ∀ (ζ : Complex),
    IsPrimitiveRoot.{0} ζ K →
      Eq.{1}
        (Matrix.permanent.{0, 0} fun j k =>
          ite.{1} (Eq.{1} j k) 1
            (have pow := HSub.hSub.{0, 0, 0} (Nat.cast.{0} j.val) (Nat.cast.{0} k.val);
            HDiv.hDiv.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} 1 (HPow.hPow.{0, 0, 0} ζ pow))
              (HSub.hSub.{0, 0, 0} 1 (HPow.hPow.{0, 0, 0} ζ pow))))
        (HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (Corpus.OEIS2454.a n)) (Nat.cast.{0} K))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record