The binomial extension of an explicit binary quotient

The root of the binary modulus supplies the coefficient of X^(3^v) - t. The resulting quotient is identified with the larger binary quotient in the surface module. No field or finiteness instances are installed globally.

noncomputable def Algebraic.Cutwidth.Extractor.extensionModulus (s v : ℕ) : Polynomial (AdjoinRoot (binaryModulus s))

The extension modulus over the binary quotient, with its named root as coefficient.

Equations

• Algebraic.Cutwidth.Extractor.extensionModulus s v = Algebraic.Cutwidth.Extractor.binomialModulus (AdjoinRoot.root (Algebraic.Cutwidth.Extractor.binaryModulus s)) v