Formal target: Corpus.OEIS1818.conjecture1

Conjecture 1: For any primitive $2n$-th root $\zeta$ of unity, the permanent of the $2n \times 2n$ matrix $[m(j,k)]_{j,k=1..2n}$ coincides with $a(n) = ((2n-1)!!)^2$, where $m(j,k)$ is $(1+\zeta^{j-k})/(1-\zeta^{j-k})$ if $j \neq k$, and $1$ otherwise.

Exact formal statement

∀ (n : Nat),
  LE.le.{0} 1 n →
    ∀ (ζ : Complex),
      IsPrimitiveRoot.{0} ζ (HMul.hMul.{0, 0, 0} 2 n) →
        Eq.{1}
          (Matrix.permanent.{0, 0} fun i j =>
            ite.{1} (Eq.{1} i j) 1
              (HDiv.hDiv.{0, 0, 0}
                (HAdd.hAdd.{0, 0, 0} 1
                  (HPow.hPow.{0, 0, 0} ζ (HSub.hSub.{0, 0, 0} (Nat.cast.{0} i.val) (Nat.cast.{0} j.val))))
                (HSub.hSub.{0, 0, 0} 1
                  (HPow.hPow.{0, 0, 0} ζ (HSub.hSub.{0, 0, 0} (Nat.cast.{0} i.val) (Nat.cast.{0} j.val))))))
          (Nat.cast.{0} (Corpus.OEIS1818.a n))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record