From 2d824f394e8c3148e95b3374fb9903f6032ba3e6 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 25 Aug 2016 01:38:44 +0200
Subject: Enriched numClosedFieldType so that it factors a lot of theory from
 both complex and algC.

The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory
have been moved to the numClosedFieldType structure in ssrnum.
This covers boths the uses in algC and complex.v. To that end the
numClosedFieldType structure has been enriched with conjugation and 'i.
Note that 'i can be deduced from the property of algebraic closure and is
only here to let the user chose which definitional equality should hold
on 'i. Same thing for conjC that could be written  `|x|^+2/x, the only
nontrivial (up to my knowledge) property is the fact that conjugation
is a ring morphism.
---
 mathcomp/odd_order/PFsection7.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/odd_order/PFsection7.v')

diff --git a/mathcomp/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v
index cea9319..4610829 100644
--- a/mathcomp/odd_order/PFsection7.v
+++ b/mathcomp/odd_order/PFsection7.v
@@ -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.
-- 
cgit v1.2.3


From 2a8af6f6b80c82a5f07cae220427cccc30ef8dac Mon Sep 17 00:00:00 2001
From: Assia Mahboubi
Date: Mon, 7 Nov 2016 15:40:31 +0100
Subject: update copyright banner

---
 mathcomp/odd_order/PFsection7.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/odd_order/PFsection7.v')

diff --git a/mathcomp/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v
index 4610829..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
-- 
cgit v1.2.3