Discriminant obstruction to ramification (source code)

= Discriminant obstruction to ramification
{title2=$p\text{ ramified}\implies p\mid\Delta_K$}

A ramified prime makes the finite algebra $\mathcal O_K/p\mathcal O_K$ have a nonzero <nilpotent element>. Multiplication by its product with any other element is nilpotent and has trace zero, so the reduced <trace pairing> is degenerate. Therefore the <field discriminant> is divisible by $p$. This proves finiteness of the ramified rational primes without requiring explicit prime factorization in the field.