Cyclotomic Euler norm factor at a new prime (source code)

= Cyclotomic Euler norm factor at a new prime
{title2=$N_{\mathbb Q(\mu_{mq})/\mathbb Q(\mu_m)}\Phi(\rho\zeta)=\Phi(\zeta)^{\operatorname{Fr}_q-1}$}

Let $q\nmid m$ be outside the excluded primes, let $\zeta$ have order $m$, and let $\rho$ be a primitive qth <root of unity>. Galois equivariance identifies the conjugates with $\Phi(\rho^i\zeta)$ for $1\leq i\leq q-1$. The distribution axiom includes the missing $i=0$ factor, so the <field norm> is $\Phi(\zeta^q)/\Phi(\zeta)$. Arithmetic <Frobenius> sends $\zeta$ to $\zeta^q$, giving the displayed factor. At higher powers of an already ramified prime all q translates occur instead. These are different norm relations; norm compatibility in just a p-power tower does not supply the auxiliary-prime relation by itself.