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.
Bézout identity and the Euclidean algorithm for polynomials over a field
Statement
Let be a field and let be not both zero. Repeated polynomial division terminates at a last nonzero remainder, whose monic associate is . There are such that
Moreover, divides both and , and every common divisor of and divides .
Facts & Assumptions
Given: A field and polynomials not both zero.
The monic gcd is the monic generator of the ideal (The monic greatest common divisor of two polynomials over a field).
Division by a nonzero polynomial over a field gives a unique remainder of smaller degree or zero (Division algorithm for polynomials over a field).
Proof
If necessary interchange and so the second input is nonzero. Repeatedly apply [L2]; this also covers a zero first input, when the first remainder is already zero. Each nonzero remainder has strictly smaller natural degree than its divisor, so the process terminates. Every remainder is a polynomial linear combination of the original by back-substitution, and the last nonzero remainder divides the preceding remainder and hence, successively, both inputs.
Every common divisor of divides each remainder and therefore divides ; after multiplying and its back-substituted coefficients by , the resulting monic polynomial has the divisibility property and generates , so [L1] identifies it with .
Depends on
Used by
- Each projection in the primary decomposition is a polynomial in the endomorphism Corollary
- If the minimal polynomial splits, V is the direct sum of the stabilised generalised eigenspaces Corollary
- Long division, the Euclidean algorithm and a Bézout identity in ℚ[x] Example
- A proper rational function with split denominator has a unique repeated-pole partial-fraction expansion Lemma
- Brauer images retain the surviving primitive idempotents Lemma
- If gcd(f,g)=1 and (fg)(T)=0, then V=ker f(T)⊕ker g(T) Lemma
- The monic gcd of two base-field polynomials is unchanged after extending the coefficient field Lemma
- A nonzero polynomial over a field is separable exactly when its gcd with its derivative is 1 Theorem
- Every irreducible polynomial over a field is prime Theorem
- For a nonconstant p in F[x], the ideal (p) is maximal and F[x]/(p) is a field exactly when p is irreducible Theorem
- tⁿ-1 is separable over K exactly when the characteristic does not divide n, and then a splitting field carries n distinct n-th roots of unity Theorem
Cited to discharge well-definedness by The monic greatest common divisor of two polynomials over a field.
Dependency tree · two levels
8 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
- Thomas W. Judson, Abstract Algebra: Theory and Applications, Theorem 17.10 (standard reference, not scraped)
- Neil Donaldson, Math 120B Notes, Section 23 (standard reference, not scraped)