prime_threehundredninetyseven
plain-language theorem explainer
397 is a prime integer under the standard definition. Number theorists checking small cases for arithmetic functions or Möbius inversions would cite this verified fact. The proof reduces to a single native_decide call that settles the claim by direct computation.
Claim. $397$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local conventions keep statements minimal so that Dirichlet inversion can be added later. Upstream results include the active edge count A from IntegrationGap, defined as the φ-power balance identity at D=3, and the coherence energy unit from Masses.Anchor.
proof idea
The proof is a one-line wrapper that applies native_decide to the Prime predicate imported from the Basic primes module.
why it matters
This supplies a concrete prime for use in the arithmetic functions library and the 3-almost primes section that follows. It supports Möbius and squarefree checks without adding new hypotheses. No direct connection to the forcing chain or phi-ladder appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.