diff options
| author | Cyril Cohen | 2018-12-13 15:05:06 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-13 15:05:06 +0100 |
| commit | f962d2a88254a99bffbc7d0a40949872a80f4669 (patch) | |
| tree | 60a84ff296299226d530dd0b495be24fd7675748 /mathcomp/field/algC.v | |
| parent | fa9b7b19fc0409f3fdfa680e08f40a84594e8307 (diff) | |
| parent | 0b1ea03dafcf36880657ba910eec28ab78ccd018 (diff) | |
Merge pull request #262 from math-comp/cancel-lemmas-implicit
Cancel lemmas implicit
Diffstat (limited to 'mathcomp/field/algC.v')
| -rw-r--r-- | mathcomp/field/algC.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index fc01763..ae60027 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -279,7 +279,7 @@ Canonical eqType := EqType type eqMixin. Definition choiceMixin : Choice.mixin_of type := EquivQuot.choiceMixin _. Canonical choiceType := ChoiceType type choiceMixin. -Definition countMixin : Countable.mixin_of type := CanCountMixin (@reprK _ _). +Definition countMixin : Countable.mixin_of type := CanCountMixin reprK. Canonical countType := CountType type countMixin. Definition CtoL (u : type) := rootQtoL (repr u). @@ -607,7 +607,8 @@ Local Notation intrp := (map_poly intr). Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj _ : injective ZtoC) : core. + +Local Hint Resolve (intr_inj : injective ZtoC) : core. (* Specialization of a few basic ssrnum order lemmas. *) @@ -882,7 +883,7 @@ Lemma CintE x : (x \in Cint) = (x \in Cnat) || (- x \in Cnat). Proof. apply/idP/idP=> [/CintP[[n | n] ->] | ]; first by rewrite Cnat_nat. by rewrite NegzE opprK Cnat_nat orbT. -by case/pred2P=> [<- | /(canLR (@opprK _)) <-]; rewrite ?rpredN rpred_nat. +by case/pred2P=> [<- | /(canLR opprK) <-]; rewrite ?rpredN rpred_nat. Qed. Lemma Cnat_norm_Cint x : x \in Cint -> `|x| \in Cnat. |