two_pow_twelve
plain-language theorem explainer
The equality 2^12 = 4096 holds in the natural numbers. Number theorists may cite it as a fixed computational anchor when handling exponents inside arithmetic function identities. The proof is a one-line term that invokes native_decide to evaluate the power directly.
Claim. $2^{12} = 4096$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This declaration records a concrete power identity that can serve as a numerical constant in exponent calculations. No upstream lemmas are referenced; the result stands alone via direct computation.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the power expression directly.
why it matters
It supplies a verified numerical constant for potential anchoring of exponent calculations inside the arithmetic functions section. No parent theorems or downstream uses are recorded in the current dependency graph. The result fills a basic computational slot without touching the Möbius or squarefree machinery defined nearby.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.