diff options
| author | Georges Gonthier | 2019-05-06 18:04:48 +0200 |
|---|---|---|
| committer | GitHub | 2019-05-06 18:04:48 +0200 |
| commit | 02830d7cf24f9198d5e7cb81843d6ca5cb69f68a (patch) | |
| tree | 73e8bf66926855dc2d0a440f6a6a0c97a92344b3 /mathcomp/field | |
| parent | a3f3d1aead4b5c35fb4a74be1cca7a5cde253d9a (diff) | |
| parent | b59653a5b377f91a21e8036bf0b5d98a35fc4963 (diff) | |
Merge pull request #342 from math-comp/deprecation
add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma names
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/galois.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 459250f..ae54fa1 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -1332,9 +1332,9 @@ rewrite -coef_map rmorph_prod; congr (_ : {poly _})`_i. symmetry; rewrite (eq_big_perm (map x r)) /= ?(big_map x). by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC. have Uxr: uniq (map x r) by rewrite map_inj_uniq //; apply: fmorph_inj. -have /leq_size_perm: {subset map x r <= r}. +have /uniq_min_size: {subset map x r <= r}. by rewrite -map_comp => _ /codomP[b ->] /=; rewrite -galM // r_xa ?groupM. -by rewrite (size_map x) perm_eq_sym; case=> // /uniq_perm_eq->. +by rewrite (size_map x) perm_eq_sym; case=> // _ /uniq_perm_eq->. Qed. Lemma mem_galTrace K E a : galois K E -> a \in E -> galTrace K E a \in K. |