LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

The product of primitive integer polynomials is primitive, and contents multiply

Statement

If $f, g \in Z [x]$ are primitive, then $f g$ is primitive. More generally, for all nonzero $f, g \in Z [x]$ ,

$cont (f g) = cont (f) cont (g) .$

Facts & Assumptions

Given: Nonzero integer polynomials $f, g$ .

[L1]

Content is the positive gcd of the coefficients, and primitive means content $1$ (Content and primitive integer polynomials).

[L2]

A polynomial is primitive exactly when no prime divides all of its coefficients (Content is the positive common divisor of the coefficients divisible by every common divisor).

[L3]

A polynomial ring over a domain is a domain (A polynomial ring over an integral domain is an integral domain).

[L4]

A ring homomorphism of coefficients extends to a homomorphism of polynomial rings (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[L5]

The canonical quotient map has its defining ideal as kernel (The canonical projection $R \to R / I$ is a surjective ring homomorphism with kernel $I$ ).

[L6]

The ring $Z / p$ is the quotient $Z / p Z$ (For every $n \in N$ , the congruence-class ring $Z / n$ is the quotient ring $Z / n Z$ ).

[L7]

For prime $p$ , the ring $Z / p$ is a field (For every prime $p$ , the two operations on $Z / p$ make it a field).

Proof

technique · contradiction

1.1

Suppose primitive $f, g$ had nonprimitive product; by [L2] some prime $p$ would divide every coefficient of $f g$ , so [L4], [L5], and [L6] would give $\overset{ˉ}{f} \overset{ˉ}{g} = 0$ in $(Z / p) [x]$ , while primitiveness makes both reductions nonzero; [L7] and [L3] contradict this.

assume-contragivenL2L3L4L5L6L7

2.1

For general nonzero $f, g$ , [L1] and [L2] allow $f = c (f) f_{0}$ and $g = c (g) g_{0}$ with primitive integer polynomials $f_{0}, g_{0}$ ; step 1.1 makes $f_{0} g_{0}$ primitive, and the universal divisibility characterization of [L2] then gives $cont (f g) = c (f) c (g)$ .

step 1.1L1L2discharge-contradiction∎

Depends on

Used by

Gauss lemma: primitive factorisations over ℚ can be cleared to primitive factorisations over ℤ Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 100 results over 22 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

Thomas W. Judson, Abstract Algebra: Theory and Applications, Theorem 17.14 (standard reference, not scraped)
Keith Conrad, Irreducibility Tests in Q[T], Appendix A (standard reference, not scraped)