Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-26
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 recursion defines a unique monic Φn∈Z[t], of degree φ(n)

Statement

The recursion of The cyclotomic polynomials Φn∈Z[t], defined by ∏d∣nΦd=tn−1 is well posed: for every n≥1 the division defining Φn is exact, Φn is a monic element of Z[t],

∏d∣nΦd=tn−1,

the product being over the positive divisors of n, and

deg⁡Φn=φ(n)

(The unit group (Z/n)× and Euler's totient φ(n)=∣(Z/n)×∣ for n≥1). Moreover (Φn)n≥1 is the only family of monic polynomials in Z[t] satisfying the displayed product identity for every n≥1.

Facts & Assumptions

Given: The recursion of The cyclotomic polynomials Φn∈Z[t], defined by ∏d∣nΦd=tn−1; the field Q, which is an ordered field (The rationals form a totally ordered field), so that m⋅1>0 and in particular m⋅1≠0 for every m≥1, whence char⁡Q=0 (The characteristic of a ring: the least n≥1 with n⋅1R=0 when one exists, and 0 otherwise) and char⁡Q divides no n≥1 (Divisibility in Z: d∣a when a=dq for some integer q).

[L1]

Let R be a commutative ring and g∈R[x] monic. For every f∈R[x] there are unique q,r∈R[x] with f=qg+r and r=0 or deg⁡r<deg⁡g (Division by a monic polynomial over a commutative ring).

[L3]

Every nonzero f∈K[x] has a splitting field over K (Every nonzero polynomial over a field has a splitting field); f monic of degree m splits over E when f=∏j=1m(t−αj) with αj∈E, repetitions allowed (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

[L4]

f is separable over K when it has no repeated root in any extension field, a repeated root of f in E being an a with (t−a)2 dividing the image of f in E[t] (Repeated roots in extension fields and separable polynomials).

[L7]

If R is an integral domain then so is R[x] (A polynomial ring over an integral domain is an integral domain), and for nonzero f,g one has deg⁡(fg)=deg⁡f+deg⁡g and lc⁡(fg)=lc⁡(f)lc⁡(g) (Over an integral domain, degrees add under multiplication of nonzero polynomials, Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

Proof

technique · induction
1.1basegiven

The assertion to be proved by strong induction on n is: the division defining Φn is exact, Φn∈Z[t] is monic, ∏d∣nΦd=tn−1, and deg⁡Φn=φ(n). At n=1 the recursion sets Φ1=t−1 outright, the only positive divisor of 1 is 1 so the product is Φ1=t−1, and deg⁡Φ1=1=φ(1).

1.2ih

Inductive hypothesis: fix n≥2 and assume the assertion for every m with 1≤m<n.

1.3L2L3given

Since char⁡Q=0 does not divide n, [L2] and [L3] supply a splitting field E of tn−1 over Q in which tn−1 is separable and μn(E) is cyclic of order n. For a positive divisor d of n put Sd:={ζ∈μn(E):ord⁡(ζ)=d} and Ψd:=∏ζ∈Sd(t−ζ)∈E[t], a monic polynomial of degree ∣Sd∣.

2.1step 1.3L3L4algebra

For every positive divisor m of n one has tm−1=∏ζ∈μm(E)(t−ζ) with ∣μm(E)∣=m: the polynomial tm−1 divides tn−1 in Z[t], since tn−1=(tm−1)(tn−m+tn−2m+⋯+1) when m∣n, so it splits over E by [L3], and a repeated root of tm−1 in an extension would be a repeated root of tn−1 there, which [L4] excludes; hence its m roots are distinct and they are by definition the elements of μm(E).

3.1step 1.3step 2.1L5

For every positive divisor m of n, μm(E) is the disjoint union of the Sd over positive divisors d of m: an element ζ∈μn(E) has finite order dividing n, and ζm=1 holds exactly when ord⁡(ζ)∣m by [L5]. Hence ∏d∣mΨd=∏ζ∈μm(E)(t−ζ)=tm−1 by step 2.1.

4.1step 1.2step 3.1L7

For every positive divisor d of n with d<n one has Φd=Ψd, by induction on d through the divisors of n: at d=1 both equal t−1, since S1={1}; and if Φe=Ψe for every positive divisor e of d with e<d, then step 1.2 and step 3.1 give (∏e∣d, e<dΨe)Φd=td−1=(∏e∣d, e<dΨe)Ψd, and cancelling the nonzero left factor in the integral domain E[t] ([L7]) yields Φd=Ψd.

5.1step 1.2step 3.1step 4.1L7

Write P:=∏d∣n, d<nΦd, monic in Z[t] by step 1.2 and [L7]. By step 4.1 and step 3.1 applied with m=n, in E[t] one has tn−1=(∏d∣n, d<nΨd)Ψn=P Ψn.

6.1step 5.1L1L7

The division of tn−1 by P in Z[t] is exact and its quotient is Ψn: by [L1] over Z there are unique q,r∈Z[t] with tn−1=qP+r and r=0 or deg⁡r<deg⁡P; this is also a division by the monic P in E[t], where step 5.1 exhibits the division with quotient Ψn and remainder 0, so the uniqueness clause of [L1] over E forces q=Ψn and r=0. Hence Φn=q=Ψn is monic in Z[t] and ∏d∣nΦd=PΦn=tn−1.

7.1step 1.2step 6.1L6L7

Degrees: taking degrees in tn−1=PΦn with [L7] gives n=deg⁡P+deg⁡Φn, and deg⁡P=∑d∣n, d<ndeg⁡Φd=∑d∣n, d<nφ(d) by step 1.2 and [L7]; so deg⁡Φn=n−∑d∣n, d<nφ(d)=φ(n) by [L6].

8.1step 6.1step 7.1L7discharge-induction∎

This is the assertion at n, so the strong induction is complete and the assertion holds for every n≥1. Uniqueness of the family follows by the same induction: if (Φm′)m≥1 is monic in Z[t] with ∏d∣mΦd′=tm−1 for all m, then Φ1′=t−1=Φ1, and if Φm′=Φm for all m<n then PΦn′=tn−1=PΦn with P≠0 in the integral domain Z[t] ([L7]), so Φn′=Φn.

Remarks

Depends on

Used by

Cited to discharge well-definedness by The cyclotomic polynomials Φₙ∈ℤ[t], defined by ∏_d∣ nΦ_d=tⁿ-1.

Dependency tree · two levels

91 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