Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedaudited 2026-09-07
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.

Dedekind--Kummer prime factorisation

Statement

Let L/K be a finite extension of number fields, let αOL with OL=OK[α], and let FOK[X] be its monic minimal polynomial over K. Let p be a nonzero prime ideal of OK, not dividing the index of this power order (the index is 1 under the stated monogeneity hypothesis). If Fˉ=igˉiei with distinct monic irreducibles over OK/p, then pOL=iPiei,Pi=(p,gi(α)),f(Pi/p)=deggˉi, Here giOK[X] are any monic lifts of gˉi, and the last f denotes the residue degree from Primes above and residue degree.

Proof

Given: monogeneity, the index hypothesis, and the displayed factorisation.

1.1

Put A=OK, B=OL and k=A/p. Monic division by F shows that the kernel of A[X]B, Xα, is (F): a remainder of degree less than degF vanishing at α is zero by minimality over K. Monogeneity gives surjectivity, hence B/pBk[X]/(Fˉ).

givenalgebra
2.1

The maximal ideals of this quotient are exactly those generated by the gˉi; their inverse images in B are Pi=(p,gi(α)). They are independent of the chosen lifts. Their residue fields are k[X]/(gˉi), of degree deggˉi, and their contractions are p. Thus they are exactly the primes above p.

step 1.1algebra
3.1

The local factorisation theorem Integral ideal factorisation in a number field, in ZF writes pB=iPiai. In the DVR BPi used in that theorem's proof, the maximal ideal of BPi/pBPi has nilpotency index exactly ai. On the polynomial side of step 1.1, localisation at (gˉi) gives k[X](gˉi)/(gˉiei), whose maximal ideal has nilpotency index exactly ei: its ei-th power vanishes and its (ei1)-st power does not. Thus ai=ei, proving the ideal factorisation and the stated ramification and residue degrees.

step 1.1step 2.1algebra

Depends on

Used by

Dependency tree · two levels

10 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