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.
A prime divides for
Statement
If is prime and , then
Facts & Assumptions
Given: A prime and a natural number with .
Binomial coefficients are natural numbers (The set of -element subsets and the binomial coefficient ).
The closed formula gives for ( for ; hence , the quotient is a natural number, and ).
A prime has no positive divisor strictly between and itself (Prime and composite integers: is prime when and its only positive divisors are and ).
If a prime divides a product of integers, it divides one of the factors (Euclid's lemma: if is prime and then or ).
Proof
Applying [L2] to and and cancelling the common nonzero factorial factors yields the integer identity .
Thus divides . Since , [L3] gives .
Euclid's lemma [L4] therefore forces . The excluded endpoints have coefficient and are not part of the claim.
Depends on
- 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}$
- Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$
- Euclid's lemma: if $p$ is prime and $p \mid ab$ then $p \mid a$ or $p \mid b$
Used by
- A purely inseparable field has nonzero Omega Counterexample
- Frobenius linear systems have nonreduced general members Counterexample
- Regular field factors can have a nonregular tensor product Counterexample
- A finite separable extension and an inseparable extension with differentials Example
- Base change of an inseparable field extension is a thickening Example
- Finite-type field extensions with zero Ω Lemma
- Separable generation after finite purely inseparable extensions Lemma
- In characteristic p the only pᵏ-th root of unity is 1, and t^pᵏ-1=(t-1)^pᵏ Proposition
- Finitely generated extensions of a perfect field are separably generated Theorem
- Frobenius x↦ xᵖ is an injective endomorphism in characteristic p, and an automorphism for finite fields Theorem
- Purely inseparable field algebras separate regularity from smoothness Theorem
- Regular algebras over a perfect field are geometrically regular Theorem
Dependency tree · two levels
43 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
- A. W. Knapp, Basic Algebra, 2nd ed., Chapter IX, Section 3 (standard reference, not scraped)