diff options
Diffstat (limited to 'mathcomp/field/fieldext.v')
| -rw-r--r-- | mathcomp/field/fieldext.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 8d2af81..2a905e9 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -696,7 +696,7 @@ move=> sKE; apply: minPoly_dvdp; last exact: root_minPoly. by apply: (polyOverSv sKE); rewrite minPolyOver. Qed. -Implicit Arguments Fadjoin_polyP [K x v]. +Arguments Fadjoin_polyP [K x v]. Lemma Fadjoin1_polyP x v : reflect (exists p, v = (map_poly (in_alg L) p).[x]) (v \in <<1; x>>%VS). Proof. @@ -737,13 +737,13 @@ Notation "'C_ ( E ) ( V )" := (capv_aspace E 'C(V)) Notation "E * F" := (prodv_aspace E F) : aspace_scope. Notation "f @: E" := (aimg_aspace f E) : aspace_scope. -Implicit Arguments Fadjoin_idP [F0 L K x]. -Implicit Arguments FadjoinP [F0 L K x E]. -Implicit Arguments Fadjoin_seqP [F0 L K rs E]. -Implicit Arguments polyOver_subvs [F0 L K p]. -Implicit Arguments Fadjoin_polyP [F0 L K x v]. -Implicit Arguments Fadjoin1_polyP [F0 L x v]. -Implicit Arguments minPoly_XsubC [F0 L K x]. +Arguments Fadjoin_idP [F0 L K x]. +Arguments FadjoinP [F0 L K x E]. +Arguments Fadjoin_seqP [F0 L K rs E]. +Arguments polyOver_subvs [F0 L K p]. +Arguments Fadjoin_polyP [F0 L K x v]. +Arguments Fadjoin1_polyP [F0 L x v]. +Arguments minPoly_XsubC [F0 L K x]. Section MapMinPoly. |