How 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.
If with , then
Statement
Let be prime and let satisfy . Then The valuation is applied only to nonzero integers. See The -adic valuation of a nonzero integer: the greatest with .
Facts & Assumptions
Given: The hypotheses and objects in the Statement.
For a prime and a nonzero integer , the -adic valuation is the value is undefined. (The -adic valuation of a nonzero integer: the greatest with ).
For a prime and nonzero integers , the product is nonzero and ( for nonzero integers , and whenever , and are all nonzero).
For a finite set and put the set of -element subsets of . Every is finite (thm-subset-of-a-finite-set), so the condition makes sense for every subset. (The set of -element subsets and the binomial coefficient ).
Let with . Then and consequently . ( for ; hence , the quotient is a natural number, and ).
The factorial and falling factorial satisfy and for , is the product . (The factorial and the falling factorial , defined by recursion in ).
Proof
We apply the valuation to the identity .
If , write with ; then and , whose parenthesized factor is prime to . Hence . The factor contributes , exactly matching the contribution of in , so all valuations cancel.
If , the binomial coefficient is , which is nonzero and prime to . No valuation of zero occurs in either case. This proves the stated claim.
Depends on
- The $p$-adic valuation $v_p(a)$ of a nonzero integer: the greatest $k \in \mathbb{N}$ with $p^{k} \mid a$
- $v_p(ab) = v_p(a) + v_p(b)$ for nonzero integers $a, b$, and $v_p(a+b) \ge \min\{v_p(a), v_p(b)\}$ whenever $a$, $b$ and $a+b$ are all nonzero
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le n$; hence $\binom{n}{k}\,k! = n^{\underline{k}}$, the quotient $n!/(k!(n-k)!)$ is a natural number, and $\binom{n}{k} = \binom{n}{n-k}$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 103 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Keith Conrad, Consequences of the Sylow Theorems, Sections 1-5 (standard reference, not scraped)