Finite dimensional field extentions

fieldExtType F == the interface type for finite field extensions of F it simply combines the fieldType and FalgType F interfaces. [fieldExtType F of L] == a fieldExt F structure for a type L that has both FalgType F and fieldType canonical instances. The field class instance must be manifest with explicit comRing, idomain, and field mixins. If L has an abstract field class should use the 'for' variant. [fieldExtType F of L for K] == a fieldExtType F structure for a type L that has an FalgType F canonical structure, given a K : fieldType whose unitRingType projection coincides with the canonical unitRingType for F. {subfield L} == the type of subfields of L that are also extensions of F; since we are in a finite dimensional setting these are exactly the F-subalgebras of L, and indeed {subfield L} is just display notation for {aspace L} when L is an extFieldType. --> All aspace operations apply to {subfield L}, but there are several additional lemmas and canonical instances specific to {subfield L} spaces, e.g., subvs_of E is an extFieldType F when E : {subfield L}. --> Also note that not all constructive subfields have type {subfield E} in the same way that not all constructive subspaces have type {vspace E}. These types only include the so called "detachable" subspaces (and subalgebras). (E :&: F)%AS, (E * F)%AS == the intersection and product (meet and join) of E and F as subfields. subFExtend iota z p == Given a field morphism iota : F -> L, this is a type for the field F^iota(z) obtained by adjoining z to the image of F in L under iota. The construction requires a non-zero polynomial p in F such that z is a root of p^iota; it returns the field F^iota if this is not so. However, p need not be irredicible. subfx_inj x == The injection of F^iota(z) into L. inj_subfx iota z p x == The injection of F into F^iota(z). subfx_eval iota z p q == Given q : {poly F} returns q. [z] as a value of type F^iota(z). subfx_root iota z p == The generator of F^iota(z) over F. SubFieldExtType pz0 irr_p == A fieldExtType F structure for F^iota(z) (more precisely, subFExtend iota z p), given proofs pz0: root (map_poly iota p) z and irr_p : irreducible_poly p. The corresponding vectType substructure (SubfxVectType pz0 irr_p) has dimension (size p).-1 over F. minPoly K x == the monic minimal polynomial of x over the subfield K. adjoin_degree K x == the degree of the minimial polynomial or the dimension of K(x)/K. Fadjoin_poly K x y == a polynomial p over K such that y = p. [x]. fieldOver F == L, but with an extFieldType (subvs_of F) structure, for F : {subfield L} vspaceOver F V == the smallest subspace of fieldOver F containing V; this coincides with V if V is an F-module. baseFieldType L == L, but with an extFieldType F0 structure, when L has a canonical extFieldType F structure and F in turn has an extFieldType F0 structure. baseVspace V == the subspace of baseFieldType L that coincides with V : {vspace L}. --> Some caution must be exercised when using fieldOver and baseFieldType, because these are convertible to L while carrying different Lmodule structures. This means that the safeguards engineered in the ssralg library that normally curb the Coq kernel's inclination to diverge are no longer effectcive, so additional precautions should be taken when matching or rewriting terms of the form a *: u, because Coq may take forever to realize it's dealing with a *: in the wrong structure. The baseField_scaleE and fieldOver_scaleE lemmas should be used to expand or fold such "trans-structure" operations explicitly beforehand.

Changing up the reference field of a fieldExtType.

Changing the reference field to a smaller field.

Base of fieldOver, finally.