Formal target: Corpus.WikipediaKummerVandiver.kummer_vandiver

Kummer–Vandiver conjecture states that for every prime $p$, the class number of the maximal real subfield of $\mathbb{Q}(\zeta_p)$ is not divisible by $p$.

Exact formal statement

∀ (p : PNat),
  p.Prime →
    Not
      (Dvd.dvd.{0} p.val
        (NumberField.classNumber.{0}
          (Subtype.{1} fun x =>
            Membership.mem.{0, 0} (NumberField.maximalRealSubfield.{0} (CyclotomicField.{0} p.val Rat)) x)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record