Computable field extensions

Facade for the field-extension stack. Extensions are F[X] / f for an arbitrary monic modulus f; the binomial case f = X^d - W is the special case BinomialParams.toExtensionParams. See the individual modules for details:

• CompPoly/Fields/Extension/Binomial.lean — irreducibility of X^d - W over a finite field, via Rabin's test collapsed to two base-field exponentiations.
• CompPoly/Fields/Extension/Arithmetic.lean — ExtensionParams (an arbitrary monic modulus), the binomial front-end BinomialParams, plus the coefficient-vector carrier Ext P with its ring operations (shiftReduce, monomialMod, mul) and the inverse candidate.
• CompPoly/Fields/Extension/Defs.lean — polynomial specifications and binomial correspondence.
• CompPoly/Fields/Extension/Bridge.lean — toQuot : Ext P → AdjoinRoot P.poly, the multiply-by-X law toQuot_shiftReduce, and the CommRing structure.
• CompPoly/Fields/Extension/Cardinality.lean — optional finiteness and cardinality certificates.
• CompPoly/Fields/Extension/Field.lean — bijectivity and the certified Field structure.