diff options
| author | Georges Gonthier | 2015-12-01 09:43:02 +0000 |
|---|---|---|
| committer | Georges Gonthier | 2015-12-04 15:07:18 +0000 |
| commit | efc830f03047c94b386ea4b356717bd128906014 (patch) | |
| tree | efcd2861a5bf4a33222903acc72d879765c66a7c /mathcomp/field/fieldext.v | |
| parent | bd8cf1baa6758fef61ba8bd9917dc16bd6150613 (diff) | |
Add instances & lemmas for regular algebras
Diffstat (limited to 'mathcomp/field/fieldext.v')
| -rw-r--r-- | mathcomp/field/fieldext.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 234ad47..5fefc49 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -265,6 +265,8 @@ End Exports. End FieldExt. Export FieldExt.Exports. +Canonical regular_fieldExtType (F : fieldType) := [fieldExtType F of F^o for F]. + Section FieldExtTheory. Variables (F0 : fieldType) (L : fieldExtType F0). |