diff options
| author | Cyril Cohen | 2020-06-08 17:27:57 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-08 17:27:57 +0200 |
| commit | 6bfc094b858c7ab1c5df7f780d68e04ba0ba4c23 (patch) | |
| tree | 367fa8929cfa4f707b1630c267927c733b048e0a /mathcomp/field | |
| parent | ed58f3059881b6179ec36448d7d4f6d74030b686 (diff) | |
turning let into local definition
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 52472a6..ce8c5b7 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -116,8 +116,8 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Let intr_inj_algC := @intr_inj [numDomainType of algC]. -Local Hint Resolve intr_inj_algC : core. +Local Definition algC_intr_inj := @intr_inj [numDomainType of algC]. +Local Hint Resolve algC_intr_inj. Local Notation QtoC_M := (ratr_rmorphism [numFieldType of algC]). Lemma C_prim_root_exists n : (n > 0)%N -> {z : algC | n.-primitive_root z}. |