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/PFsection7.v | |
| parent | 5daf14d44b9cd22c6b51b2b23b4eebe5f3aee79f (diff) | |
| parent | 23e57fb47874331c5feaace883513b7abecdff28 (diff) | |
Merge remote-tracking branch 'upstream/master' into fixdoc
Diffstat (limited to 'mathcomp/odd_order/PFsection7.v')
| -rw-r--r-- | mathcomp/odd_order/PFsection7.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v index cea9319..455681c 100644 --- a/mathcomp/odd_order/PFsection7.v +++ b/mathcomp/odd_order/PFsection7.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 @@ -324,7 +324,7 @@ transitivity (\sum_(x in A) \sum_(xi <- S) \sum_(mu <- S) F xi mu x). apply: eq_bigr => x Ax; rewrite part_a // sum_cfunE -mulrA mulr_suml. apply: eq_bigr => xi _; rewrite mulrA -mulr_suml rmorph_sum; congr (_ * _). rewrite mulr_sumr; apply: eq_bigr => mu _; rewrite !cfunE (cfdotC mu). - rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM conjCK -4!mulrA 2!(mulrCA _^-1). + rewrite -{1}[mu x]conjCK -fmorph_div -rmorphM conjCK -3!mulrA 2!(mulrCA _^-1). by rewrite (mulrA _^-1) -invfM 2!(mulrCA (xi x)) mulrA 2!(mulrA _^*). rewrite exchange_big; apply: eq_bigr => xi _; rewrite exchange_big /=. apply: eq_big_seq => mu Smu; have Tmu := sST mu Smu. |