Definition 11.2 (Residue class degree). fi:=[OLPi:OK𝔭] is the residue class degree of Pi over 𝔭.