diff options
| author | Cyril Cohen | 2018-07-14 01:26:16 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-07-14 01:26:16 +0100 |
| commit | ededc3786a779f26303e9545dc68bd6006b4aae4 (patch) | |
| tree | cebe4ef3365d341b2289aefd977bb717988ef27d /mathcomp/algebra/ssralg.v | |
| parent | 618c9229fecbf6f1e85035aa0033943dcd4f3464 (diff) | |
Laurent's simplifications
Diffstat (limited to 'mathcomp/algebra/ssralg.v')
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 31579ce..9ccb92f 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1172,7 +1172,7 @@ Lemma signrMK n : @involutive R ( *%R ((-1) ^+ n)). Proof. by move=> x; rewrite mulrA -expr2 sqrr_sign mul1r. Qed. Lemma lastr_eq0 (s : seq R) x : x != 0 -> (last x s == 0) = (last 1 s == 0). -Proof. by elim: s => [|y s ihs] /negPf // ->; rewrite oner_eq0. Qed. +Proof. by case: s => [|y s] /negPf // ->; rewrite oner_eq0. Qed. Lemma mulrI_eq0 x y : lreg x -> (x * y == 0) = (y == 0). Proof. by move=> reg_x; rewrite -{1}(mulr0 x) (inj_eq reg_x). Qed. |