two_pow_six
plain-language theorem explainer
The equality 2 to the sixth power equals 64 holds in the natural numbers. It supplies a basic numerical constant for arithmetic computations inside the module on Möbius and related functions. The proof evaluates the expression directly via a native decision procedure with no lemmas required.
Claim. $2^6 = 64$ in the natural numbers.
background
The declaration sits in the module supplying lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The module keeps statements minimal while deeper Dirichlet inversion remains for later layering. No upstream results are referenced.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the power equality directly.
why it matters
The equality supplies a ready numerical fact for use in arithmetic function calculations. It does not yet connect to Möbius properties or prime results in the module. No downstream theorems cite it at present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.