Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
by both inclusion-exclusion and the prime-power product formula
Example
Euler's totient at is , obtained either by excluding multiples of or by multiplying the prime-power contributions.
Facts & Assumptions
Given: The positive integer .
Its canonical prime factorisation is (For and any injective list of primes containing every prime divisor of , one has ; the exponents are determined by , and for every prime outside the list).
Euler's formula gives over the distinct prime divisors of and, after carrying the natural numbers into , the equivalent form (Euler's product formula for , stated through a finite injective list of its prime divisors). Multiplying out that second product over the subsets of is the inclusion-exclusion display used below; the cited theorem states the two products, not that display.
Verification
Inclusion-exclusion over the multiples of gives .
The product form gives .
Both computations therefore give the same value, .
Depends on
- Euler's product formula $\varphi(n)=n\prod_{p\mid n}(1-1/p)=\prod_{p^k\parallel n}(p^k-p^{k-1})$ for $n\ge1$, stated through a finite injective list of its prime divisors
- For $n \ge 1$ and any injective list $p : r \to \mathbb{Z}$ of primes containing every prime divisor of $n$, one has $n = \prod_{i<r} p_i^{\,v_{p_i}(n)}$; the exponents are determined by $n$, and $v_q(n) = 0$ for every prime $q$ outside the list
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
44 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Mathematics LibreTexts, Euler's phi Function (standard reference, not scraped)
- K. Conrad, The Chinese Remainder Theorem (standard reference, not scraped)
- Carnegie Mellon, number-theory lecture notes (standard reference, not scraped)