Formal target: Corpus.OEIS60841.conjecture

"Conjecture: $1/\det(M)$ is an integer only for n: 1 to 34, 36 and 38.

Exact formal statement

And
  (∀ (n : Nat),
    LE.le.{0} 1 n →
      Iff (Eq.{1} (Inv.inv.{0} (Matrix.det.{0, 0} (Corpus.OEIS60841.lcmMatrix n))).den 1)
        (Membership.mem.{0, 0} Corpus.OEIS60841.integerDetN n))
  (∀ (n : Nat),
    LE.le.{0} 1 n →
      Exists.{1} fun k =>
        Eq.{1} (Inv.inv.{0} (Matrix.det.{0, 0} (Corpus.OEIS60841.lcmMatrix n))).den (HPow.hPow.{0, 0, 0} 2 k))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record