diff options
| author | affeldt-aist | 2020-11-20 12:41:11 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-20 12:41:11 +0900 |
| commit | 3bb1ccc63170e3e71ef9d5b62758b6fdb1c4371c (patch) | |
| tree | 076b8d8c53eaaf424258388bbd0068970c55b85f /mathcomp/field/finfield.v | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
| parent | e565f8d9bebd4fd681c34086d5448dbaebc11976 (diff) | |
Merge pull request #658 from CohenCyril/duplicate_clear
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/field/finfield.v')
| -rw-r--r-- | mathcomp/field/finfield.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index 492aed8..19684dc 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -405,7 +405,7 @@ have fZ: linear f. have /kAut_to_gal[alpha galLalpha Dalpha]: kAut 1 {:L} (linfun (Linear fZ)). rewrite kAutfE; apply/kHomP; split=> [x y _ _ | x /idfP]; rewrite !lfunE //=. exact: (rmorphM (RMorphism fM)). -have{Dalpha} Dalpha: alpha =1 f by move=> a; rewrite -Dalpha ?memvf ?lfunE. +have{} Dalpha: alpha =1 f by move=> a; rewrite -Dalpha ?memvf ?lfunE. suffices <-: fixedField [set alpha] = 1%AS. by rewrite gal_generated /generator; exists alpha. apply/vspaceP=> x; apply/fixedFieldP/idfP; rewrite ?memvf // => id_x. @@ -442,7 +442,7 @@ End FinGalois. Lemma Fermat's_little_theorem (L : fieldExtType F) (K : {subfield L}) a : (a \in K) = (a ^+ order K == a). Proof. -move: K a; wlog [{L}L -> K a]: L / exists galL : splittingFieldType F, L = galL. +move: K a; wlog [{}L -> K a]: L / exists galL : splittingFieldType F, L = galL. by pose galL := (FinSplittingFieldType F L) => /(_ galL); apply; exists galL. have /galois_fixedField fixLK := finField_galois (subvf K). have [alpha defGalLK Dalpha] := finField_galois_generator (subvf K). |