Fundamental identity for prime decomposition (source code)

= Fundamental identity for prime decomposition

Let $B$ be the <integral closure> of a <Dedekind domain> $R$ in a finite separable extension $L/K$ of degree $n$. For a nonzero <prime ideal> $\mathfrak p$ of $R$, write
$$
\mathfrak pB=\prod_{\mathfrak q\mid\mathfrak p}\mathfrak q^{e_{\mathfrak q/\mathfrak p}}
$$
and let $f_{\mathfrak q/\mathfrak p}=[B/\mathfrak q:R/\mathfrak p]$. Then
$$
n=\sum_{\mathfrak q\mid\mathfrak p}e_{\mathfrak q/\mathfrak p}f_{\mathfrak q/\mathfrak p}.
$$