diff options
| author | Florent Hivert | 2016-11-17 01:33:36 +0100 |
|---|---|---|
| committer | Florent Hivert | 2016-11-17 01:33:36 +0100 |
| commit | 84cc11db01159b17a8dcf4d02dbe0549067d228f (patch) | |
| tree | 964ee247bbf305022235217e716578a37be0bf62 /mathcomp/odd_order/PFsection3.v | |
| parent | 5daf14d44b9cd22c6b51b2b23b4eebe5f3aee79f (diff) | |
| parent | 23e57fb47874331c5feaace883513b7abecdff28 (diff) | |
Merge remote-tracking branch 'upstream/master' into fixdoc
Diffstat (limited to 'mathcomp/odd_order/PFsection3.v')
| -rw-r--r-- | mathcomp/odd_order/PFsection3.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v index cb55ae4..eb5ccf8 100644 --- a/mathcomp/odd_order/PFsection3.v +++ b/mathcomp/odd_order/PFsection3.v @@ -1,4 +1,4 @@ -(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp @@ -1360,7 +1360,7 @@ have{oxi_00} oxi_i0 i j i0: '[xi_ i j, xi_ i0 0] = ((i == i0) && (j == 0))%:R. by rewrite cfdotC Xi0_X0j // conjC0. have [-> | nzi2] := altP (i2 =P 0); first exact: oxi_0j. have [-> | nzj2] := altP (j2 =P 0); first exact: oxi_i0. -rewrite cfdotC eq_sym; apply: canLR conjCK _; rewrite rmorph_nat. +rewrite cfdotC eq_sym; apply: canLR (@conjCK _) _; rewrite rmorph_nat. have [-> | nzi1] := altP (i1 =P 0); first exact: oxi_0j. have [-> | nzj1] := altP (j1 =P 0); first exact: oxi_i0. have ->: xi_ i1 j1 = beta i1 j1 + xi_ i1 0 + xi_ 0 j1 by rewrite /xi_ !ifN. |