Finiteness and cardinality of monic quotient presentations

The coordinate equivalence gives Finite (Ext P) from Finite F, and gives an optional Fintype (Ext P) when an enumeration of the base is available. A separate certificate Fact (Nat.card F = P.q) identifies the stored exponent parameter with the base cardinality. The resulting extension cardinality is P.q ^ P.d.

These facts require neither a polynomial quotient bridge nor irreducibility. All finiteness and cardinality assumptions used by field laws are propositions, so executable arithmetic never receives an enumeration dictionary merely to use those laws.

theorem CompPoly.Extension.ExtensionParams.card_eq {F : Type u_1} [Fintype F] (P : ExtensionParams F) [Fact (Nat.card F = P.q)] : Fintype.card F = P.q

The certified cardinality agrees with any enumeration of the base type.

theorem CompPoly.Extension.BinomialParams.card_eq {F : Type u_1} [Fintype F] (P : BinomialParams F) [Fact (Nat.card F = P.q)] : Fintype.card F = P.q

The certified binomial base cardinality agrees with any enumeration.

instance CompPoly.Extension.instFactEqNatCardQToExtensionParamsOfQ {F : Type u_1} [Ring F] (P : BinomialParams F) [Fact (Nat.card F = P.q)] : Fact (Nat.card F = P.toExtensionParams.q)

instance CompPoly.Extension.Ext.instFinite {F : Type u_1} {P : ExtensionParams F} [Finite F] : Finite (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instFintype {F : Type u_1} {P : ExtensionParams F} [Fintype F] : Fintype (Ext P)

theorem CompPoly.Extension.Ext.card_ext {F : Type u_1} {P : ExtensionParams F} [Fintype F] [Fact (Nat.card F = P.q)] : Fintype.card (Ext P) = P.q ^ P.d

The enumerated extension cardinality is the certified base cardinality to the degree.

theorem CompPoly.Extension.Ext.nat_card_ext {F : Type u_1} {P : ExtensionParams F} [Finite F] [Fact (Nat.card F = P.q)] : Nat.card (Ext P) = P.q ^ P.d

The extension has q^d elements, independently of any chosen enumeration.