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.
Division algorithm for polynomials over a field
Statement
Let be a field, let , and let . There are unique polynomials such that
The statement includes and nonzero constant divisors.
Facts & Assumptions
Given: A field , a polynomial , and a nonzero polynomial with leading coefficient .
Division by a monic polynomial over a commutative ring has a unique quotient and degree-small remainder (Division by a monic polynomial over a commutative ring).
Degrees add under multiplication of nonzero polynomials over a domain (Over an integral domain, degrees add under multiplication of nonzero polynomials).
Every nonzero element of a field has a multiplicative inverse, and a field is commutative (Field).
A nonzero polynomial has a nonzero leading coefficient; it is monic when that coefficient is (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).
Proof
By [L3] the coefficient has an inverse, and is monic with the same degree as ; [L1] gives unique with and or , so gives .
If , then ; unless , [L2] makes the left side have degree at least , while the right side is zero or has degree below , so and then .
Depends on
Used by
- For every field F, F[x] is a Euclidean domain with degree as Euclidean function Corollary
- ℚ[x]/(x²-1) is not a field: reducibility creates nonzero zero divisors Counterexample
- A polynomial PID has a nonzero Kunneth Tor class Example
- Long division, the Euclidean algorithm and a Bézout identity in ℚ[x] Example
- A coefficient sequence is eventually linearly recurrent if and only if its formal generating function is rational Theorem
- A simple algebraic extension is its minimal-polynomial quotient and has power basis 1,a,…,aⁿ⁻¹ and degree n Theorem
- A vector annihilator gives a power basis and its companion matrix Theorem
- Bézout identity and the Euclidean algorithm for polynomials over a field Theorem
- F[x]/(p) for monic irreducible p is a field extension containing the root x+(p) with unique reduced representatives Theorem
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.6 (standard reference, not scraped)
- Neil Donaldson, Math 120B Notes, Theorem 23.2 (standard reference, not scraped)