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/BGappendixC.v | 11 ++++++----- mathcomp/odd_order/PFsection11.v | 2 +- mathcomp/odd_order/PFsection3.v | 2 +- mathcomp/odd_order/PFsection5.v | 8 ++++---- mathcomp/odd_order/PFsection6.v | 6 +++--- mathcomp/odd_order/PFsection7.v | 2 +- 6 files changed, 16 insertions(+), 15 deletions(-) (limited to 'mathcomp/odd_order') diff --git a/mathcomp/odd_order/BGappendixC.v b/mathcomp/odd_order/BGappendixC.v index a64c49a..16a0a3c 100644 --- a/mathcomp/odd_order/BGappendixC.v +++ b/mathcomp/odd_order/BGappendixC.v @@ -288,7 +288,7 @@ Proof. have [q_gt4 | q_le4] := ltnP 4 q. pose inK x := enum_rank_in (classes1 H) (x ^: H). have inK_E x: x \in H -> enum_val (inK x) = x ^: H. - by move=> Hx; rewrite enum_rankK_in ?mem_classes. + by move=> Hx; rewrite enum_rankK_in ?mem_classes. pose j := inK s; pose k := inK (s ^+ 2)%g; pose e := gring_classM_coef j j k. have cPP: abelian P by rewrite -(injm_abelian inj_sigma) ?zmod_abelian. have Hs: s \in H by rewrite -(sdprodW defH) -[s]mulg1 mem_mulg. @@ -355,18 +355,19 @@ have [q_gt4 | q_le4] := ltnP 4 q. by rewrite sub_cent1 groupX // (subsetP cPP). rewrite mulrnA -second_orthogonality_relation ?groupX // big_mkcond. by apply: ler_sum => i _; rewrite normCK; case: ifP; rewrite ?mul_conjC_ge0. - have sqrtP_gt0: 0 < sqrtC #|P|%:R by rewrite sqrtC_gt0 ?gt0CG. - have{De ub_linH'}: `|(#|P| * e)%:R - #|U|%:R ^+ 2| <= #|P|%:R * sqrtC #|P|%:R. + have sqrtP_gt0: 0 < sqrtC #|P|%:R :> algC by rewrite sqrtC_gt0 ?gt0CG. + have{De ub_linH'}: + `|(#|P| * e)%:R - #|U|%:R ^+ 2| <= #|P|%:R * sqrtC #|P|%:R :> algC. rewrite natrM De mulrCA mulrA divfK ?neq0CG // (bigID linH) /= sum_linH. rewrite mulrDr addrC addKr mulrC mulr_suml /chi_s2. rewrite (ler_trans (ler_norm_sum _ _ _)) // -ler_pdivr_mulr // mulr_suml. apply: ler_trans (ub_linH' 1%N isT); apply: ler_sum => i linH'i. rewrite ler_pdivr_mulr // degU ?divfK ?neq0CG //. rewrite normrM -normrX norm_conjC ler_wpmul2l ?normr_ge0 //. - rewrite -ler_sqr ?qualifE ?normr_ge0 ?(@ltrW _ 0) // sqrtCK. + rewrite -ler_sqr ?qualifE ?normr_ge0 ?(@ltrW _ 0) // sqrtCK. apply: ler_trans (ub_linH' 2 isT); rewrite (bigD1 i) ?ler_paddr //=. by apply: sumr_ge0 => i1 _; rewrite exprn_ge0 ?normr_ge0. - rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _]. + rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _]. rewrite -ltC_nat -(ltr_pmul2l (gt0CG P)) {lb_Pe}(ltr_le_trans _ lb_Pe) //. rewrite ltr_subr_addl (@ler_lt_trans _ ((p ^ q.-1)%:R ^+ 2)) //; last first. rewrite -!natrX ltC_nat ltn_sqr oU ltn_divRL ?dvdn_pred_predX //. diff --git a/mathcomp/odd_order/PFsection11.v b/mathcomp/odd_order/PFsection11.v index b966f25..3c4ec9f 100644 --- a/mathcomp/odd_order/PFsection11.v +++ b/mathcomp/odd_order/PFsection11.v @@ -232,7 +232,7 @@ Lemma bounded_proper_coherent H1 : (#|HU : H1| <= 2 * q * #|U : C| + 1)%N. Proof. move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU. -suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R. +suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC. rewrite indexgg sqrtC1 mulr1 -leC_nat natrD -ler_subl_addr -mulnA natrM. congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)). rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC. diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v index cb55ae4..9011122 100644 --- a/mathcomp/odd_order/PFsection3.v +++ b/mathcomp/odd_order/PFsection3.v @@ -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. diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v index d318f5f..3f90da7 100644 --- a/mathcomp/odd_order/PFsection5.v +++ b/mathcomp/odd_order/PFsection5.v @@ -492,7 +492,7 @@ Definition subcoherent S tau R := (*c*) pairwise_orthogonal S, (*d*) {in S, forall xi : 'CF(L : {set gT}), [/\ {subset R xi <= 'Z[irr G]}, orthonormal (R xi) - & tau (xi - xi^*)%CF = \sum_(alpha <- R xi) alpha]} + & tau (xi - xi^*%CF) = \sum_(alpha <- R xi) alpha]} & (*e*) {in S &, forall xi phi : 'CF(L), orthogonal phi (xi :: xi^*%CF) -> orthogonal (R phi) (R xi)}]. @@ -621,7 +621,7 @@ have isoS1: {in S1, isometry [eta tau with eta1 |-> zeta1], to 'Z[irr G]}. split=> [xi eta | eta]; rewrite !in_cons /=; last first. by case: eqP => [-> | _ /isoS[/Ztau/zcharW]]. do 2!case: eqP => [-> _|_ /isoS[? ?]] //; last exact: Itau. - by apply/(can_inj conjCK); rewrite -!cfdotC. + by apply/(can_inj (@conjCK _)); rewrite -!cfdotC. have [nu Dnu IZnu] := Zisometry_of_iso freeS1 isoS1. exists nu; split=> // phi; rewrite zcharD1E => /andP[]. case/(zchar_expansion (free_uniq freeS1)) => b Zb {phi}-> phi1_0. @@ -646,7 +646,7 @@ have N_S: {subset S <= character} by move=> _ /irrS/irrP[i ->]; apply: irr_char. have Z_S: {subset S <= 'Z[irr L]} by move=> chi /N_S/char_vchar. have o1S: orthonormal S by apply: sub_orthonormal (irr_orthonormal L). have [[_ dotSS] oS] := (orthonormalP o1S, orthonormal_orthogonal o1S). -pose beta chi := tau (chi - chi^*)%CF; pose eqBP := _ =P beta _. +pose beta chi := tau (chi - chi^*%CF); pose eqBP := _ =P beta _. have Zbeta: {in S, forall chi, chi - (chi^*)%CF \in 'Z[S, L^#]}. move=> chi Schi; rewrite /= zcharD1E rpredB ?mem_zchar ?ccS //= !cfunE. by rewrite subr_eq0 conj_Cnat // Cnat_char1 ?N_S. @@ -885,7 +885,7 @@ Lemma subcoherent_norm chi psi (tau1 : {additive 'CF(L) -> 'CF(G)}) X Y : [/\ chi \in S, psi \in 'Z[irr L] & orthogonal (chi :: chi^*)%CF psi] -> let S0 := chi - psi :: chi - chi^*%CF in {in 'Z[S0], isometry tau1, to 'Z[irr G]} -> - tau1 (chi - chi^*)%CF = tau (chi - chi^*)%CF -> + tau1 (chi - chi^*%CF) = tau (chi - chi^*%CF) -> [/\ tau1 (chi - psi) = X - Y, '[X, Y] = 0 & orthogonal Y (R chi)] -> [/\ (*a*) '[chi] <= '[X] & (*b*) '[psi] <= '[Y] -> diff --git a/mathcomp/odd_order/PFsection6.v b/mathcomp/odd_order/PFsection6.v index 6d9ecfc..cbde798 100644 --- a/mathcomp/odd_order/PFsection6.v +++ b/mathcomp/odd_order/PFsection6.v @@ -83,13 +83,13 @@ Lemma coherent_seqIndD_bound (A B C D : {group gT}) : (*a*) [/\ A \proper K, B \subset D, D \subset C, C \subset K & D / B \subset 'Z(C / B)]%g -> (*b*) coherent (S A) L^# tau -> \unless coherent (S B) L^# tau, - #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R. + #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R :> algC. Proof. move=> [nsAL nsBL nsCL nsDL] [ltAK sBD sDC sCK sDbZC] cohA. have sBC := subset_trans sBD sDC; have sBK := subset_trans sBC sCK. have [sAK nsBK] := (proper_sub ltAK, normalS sBK sKL nsBL). have{sBC} [nsAK nsBC] := (normalS sAK sKL nsAL, normalS sBC sCK nsBK). -rewrite real_lerNgt ?rpredB ?ger0_real ?mulr_ge0 ?sqrtC_ge0 ?ler0n //. +rewrite real_lerNgt ?rpredB ?ger0_real ?mulr_ge0 ?sqrtC_ge0 ?ler0n ?ler01 //. apply/unless_contra; rewrite negbK -(Lagrange_index sKL sCK) natrM => lb_KA. pose S2 : seq 'CF(L) := [::]; pose S1 := S2 ++ S A; rewrite -[S A]/S1 in cohA. have ccsS1S: cfConjC_subset S1 calS by apply: seqInd_conjC_subset1. @@ -153,7 +153,7 @@ have sAbZH: (A / B \subset 'Z(H / B))%g. by apply: homg_quotientS; rewrite ?(subset_trans sHL) ?normal_norm. have ltAH: A \proper H. by rewrite properEneq sAH (contraTneq _ lbHA) // => ->; rewrite indexgg addn1. -set x := sqrtC #|H : A|%:R. +set x : algC := sqrtC #|H : A|%:R. have [nz_x x_gt0]: x != 0 /\ 0 < x by rewrite gtr_eqF sqrtC_gt0 gt0CiG. without loss{cohA} ubKA: / #|K : A|%:R - 1 <= 2%:R * #|L : H|%:R * x. have [sAK ltAK] := (subset_trans sAH sHK, proper_sub_trans ltAH sHK). 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 88b1305ed18f783c7ec8e16ae8da1f932303742c Mon Sep 17 00:00:00 2001 From: thery Date: Thu, 15 Sep 2016 17:39:55 +0200 Subject: Refactoring of binonial Variable renaming from 'C(m,n) to 'C(n,m) Renaming theorem mul_Sm_binn to mul_bin_diag Adding theorems mul_bin_left mul_bin_right --- mathcomp/odd_order/PFsection9.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/odd_order') diff --git a/mathcomp/odd_order/PFsection9.v b/mathcomp/odd_order/PFsection9.v index 63e10bb..e7f82bc 100644 --- a/mathcomp/odd_order/PFsection9.v +++ b/mathcomp/odd_order/PFsection9.v @@ -1953,7 +1953,7 @@ have [gtS4alpha s4gt0]: (size S4)%:R > '[alpha] /\ (size S4 > 0)%N. rewrite ltn_pmul2r ?expn_gt0 ?a_gt0 // -doubleS. by rewrite -(prednK q_gt0) expnS mul2n leq_double ltn_expl. rewrite mulnA leq_pmul2r ?expn_gt0 ?a_gt0 // -(subnKC q_gt2). - rewrite mulnCA mulnA addSn -mul_Sm_binm bin1 -mulnA leq_pmul2l //. + rewrite mulnCA mulnA addSn -mul_bin_diag bin1 -mulnA leq_pmul2l //. by rewrite mulnS -addSnnS leq_addr. rewrite Dp -Da_p mul2n (addnC a.*2) expnDn -(subnKC q_gt2) !addSn add0n. rewrite 3!big_ord_recl big_ord_recr /= !exp1n /= bin1 binn !mul1n /bump /=. -- 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/BGappendixAB.v | 2 +- mathcomp/odd_order/BGappendixC.v | 2 +- mathcomp/odd_order/BGsection1.v | 2 +- mathcomp/odd_order/BGsection10.v | 2 +- mathcomp/odd_order/BGsection11.v | 2 +- mathcomp/odd_order/BGsection12.v | 2 +- mathcomp/odd_order/BGsection13.v | 2 +- mathcomp/odd_order/BGsection14.v | 2 +- mathcomp/odd_order/BGsection15.v | 2 +- mathcomp/odd_order/BGsection16.v | 2 +- mathcomp/odd_order/BGsection2.v | 2 +- mathcomp/odd_order/BGsection3.v | 2 +- mathcomp/odd_order/BGsection4.v | 2 +- mathcomp/odd_order/BGsection5.v | 2 +- mathcomp/odd_order/BGsection6.v | 2 +- mathcomp/odd_order/BGsection7.v | 2 +- mathcomp/odd_order/BGsection8.v | 2 +- mathcomp/odd_order/BGsection9.v | 2 +- mathcomp/odd_order/PFsection1.v | 2 +- mathcomp/odd_order/PFsection10.v | 2 +- mathcomp/odd_order/PFsection11.v | 2 +- mathcomp/odd_order/PFsection12.v | 2 +- mathcomp/odd_order/PFsection13.v | 2 +- mathcomp/odd_order/PFsection14.v | 2 +- mathcomp/odd_order/PFsection2.v | 2 +- mathcomp/odd_order/PFsection3.v | 2 +- mathcomp/odd_order/PFsection4.v | 2 +- mathcomp/odd_order/PFsection5.v | 2 +- mathcomp/odd_order/PFsection6.v | 2 +- mathcomp/odd_order/PFsection7.v | 2 +- mathcomp/odd_order/PFsection8.v | 2 +- mathcomp/odd_order/PFsection9.v | 2 +- mathcomp/odd_order/stripped_odd_order_theorem.v | 2 +- mathcomp/odd_order/wielandt_fixpoint.v | 2 +- 34 files changed, 34 insertions(+), 34 deletions(-) (limited to 'mathcomp/odd_order') diff --git a/mathcomp/odd_order/BGappendixAB.v b/mathcomp/odd_order/BGappendixAB.v index f1ec1b2..cb104f4 100644 --- a/mathcomp/odd_order/BGappendixAB.v +++ b/mathcomp/odd_order/BGappendixAB.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 diff --git a/mathcomp/odd_order/BGappendixC.v b/mathcomp/odd_order/BGappendixC.v index 16a0a3c..f8b9137 100644 --- a/mathcomp/odd_order/BGappendixC.v +++ b/mathcomp/odd_order/BGappendixC.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 diff --git a/mathcomp/odd_order/BGsection1.v b/mathcomp/odd_order/BGsection1.v index 79bb387..7539af3 100644 --- a/mathcomp/odd_order/BGsection1.v +++ b/mathcomp/odd_order/BGsection1.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 diff --git a/mathcomp/odd_order/BGsection10.v b/mathcomp/odd_order/BGsection10.v index 6c8e91b..5a61e25 100644 --- a/mathcomp/odd_order/BGsection10.v +++ b/mathcomp/odd_order/BGsection10.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 diff --git a/mathcomp/odd_order/BGsection11.v b/mathcomp/odd_order/BGsection11.v index fa3cd65..fe41e8d 100644 --- a/mathcomp/odd_order/BGsection11.v +++ b/mathcomp/odd_order/BGsection11.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 diff --git a/mathcomp/odd_order/BGsection12.v b/mathcomp/odd_order/BGsection12.v index a266ed3..1dc8454 100644 --- a/mathcomp/odd_order/BGsection12.v +++ b/mathcomp/odd_order/BGsection12.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 diff --git a/mathcomp/odd_order/BGsection13.v b/mathcomp/odd_order/BGsection13.v index 13b7dcb..e90be7f 100644 --- a/mathcomp/odd_order/BGsection13.v +++ b/mathcomp/odd_order/BGsection13.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 diff --git a/mathcomp/odd_order/BGsection14.v b/mathcomp/odd_order/BGsection14.v index 18d4b08..2e3f523 100644 --- a/mathcomp/odd_order/BGsection14.v +++ b/mathcomp/odd_order/BGsection14.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 diff --git a/mathcomp/odd_order/BGsection15.v b/mathcomp/odd_order/BGsection15.v index 553feda..06d7eb9 100644 --- a/mathcomp/odd_order/BGsection15.v +++ b/mathcomp/odd_order/BGsection15.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 diff --git a/mathcomp/odd_order/BGsection16.v b/mathcomp/odd_order/BGsection16.v index 32850e4..737a92d 100644 --- a/mathcomp/odd_order/BGsection16.v +++ b/mathcomp/odd_order/BGsection16.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 diff --git a/mathcomp/odd_order/BGsection2.v b/mathcomp/odd_order/BGsection2.v index 9008cf8..5d7a899 100644 --- a/mathcomp/odd_order/BGsection2.v +++ b/mathcomp/odd_order/BGsection2.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 diff --git a/mathcomp/odd_order/BGsection3.v b/mathcomp/odd_order/BGsection3.v index 03455c3..007aaf4 100644 --- a/mathcomp/odd_order/BGsection3.v +++ b/mathcomp/odd_order/BGsection3.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 diff --git a/mathcomp/odd_order/BGsection4.v b/mathcomp/odd_order/BGsection4.v index a9b519a..217f151 100644 --- a/mathcomp/odd_order/BGsection4.v +++ b/mathcomp/odd_order/BGsection4.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 diff --git a/mathcomp/odd_order/BGsection5.v b/mathcomp/odd_order/BGsection5.v index 50f8e21..bf84a99 100644 --- a/mathcomp/odd_order/BGsection5.v +++ b/mathcomp/odd_order/BGsection5.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 diff --git a/mathcomp/odd_order/BGsection6.v b/mathcomp/odd_order/BGsection6.v index 6d2df4d..e344b98 100644 --- a/mathcomp/odd_order/BGsection6.v +++ b/mathcomp/odd_order/BGsection6.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 diff --git a/mathcomp/odd_order/BGsection7.v b/mathcomp/odd_order/BGsection7.v index 6af8f7d..71e800e 100644 --- a/mathcomp/odd_order/BGsection7.v +++ b/mathcomp/odd_order/BGsection7.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 diff --git a/mathcomp/odd_order/BGsection8.v b/mathcomp/odd_order/BGsection8.v index 9ced163..db378f3 100644 --- a/mathcomp/odd_order/BGsection8.v +++ b/mathcomp/odd_order/BGsection8.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 diff --git a/mathcomp/odd_order/BGsection9.v b/mathcomp/odd_order/BGsection9.v index 3baa270..f649e84 100644 --- a/mathcomp/odd_order/BGsection9.v +++ b/mathcomp/odd_order/BGsection9.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 diff --git a/mathcomp/odd_order/PFsection1.v b/mathcomp/odd_order/PFsection1.v index 7c74766..1d784ed 100644 --- a/mathcomp/odd_order/PFsection1.v +++ b/mathcomp/odd_order/PFsection1.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 diff --git a/mathcomp/odd_order/PFsection10.v b/mathcomp/odd_order/PFsection10.v index 18fbf8c..11b3b20 100644 --- a/mathcomp/odd_order/PFsection10.v +++ b/mathcomp/odd_order/PFsection10.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 diff --git a/mathcomp/odd_order/PFsection11.v b/mathcomp/odd_order/PFsection11.v index 3c4ec9f..c37633f 100644 --- a/mathcomp/odd_order/PFsection11.v +++ b/mathcomp/odd_order/PFsection11.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 diff --git a/mathcomp/odd_order/PFsection12.v b/mathcomp/odd_order/PFsection12.v index fa5a453..fcc35bf 100644 --- a/mathcomp/odd_order/PFsection12.v +++ b/mathcomp/odd_order/PFsection12.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 diff --git a/mathcomp/odd_order/PFsection13.v b/mathcomp/odd_order/PFsection13.v index 1ab2aee..18e8606 100644 --- a/mathcomp/odd_order/PFsection13.v +++ b/mathcomp/odd_order/PFsection13.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 diff --git a/mathcomp/odd_order/PFsection14.v b/mathcomp/odd_order/PFsection14.v index 5c43caa..c634ec1 100644 --- a/mathcomp/odd_order/PFsection14.v +++ b/mathcomp/odd_order/PFsection14.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 diff --git a/mathcomp/odd_order/PFsection2.v b/mathcomp/odd_order/PFsection2.v index 04c4eba..f92bb16 100644 --- a/mathcomp/odd_order/PFsection2.v +++ b/mathcomp/odd_order/PFsection2.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 diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v index 9011122..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 diff --git a/mathcomp/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v index 01ca8a5..c897e84 100644 --- a/mathcomp/odd_order/PFsection4.v +++ b/mathcomp/odd_order/PFsection4.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 diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v index 3f90da7..636c48c 100644 --- a/mathcomp/odd_order/PFsection5.v +++ b/mathcomp/odd_order/PFsection5.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 diff --git a/mathcomp/odd_order/PFsection6.v b/mathcomp/odd_order/PFsection6.v index cbde798..b32a57d 100644 --- a/mathcomp/odd_order/PFsection6.v +++ b/mathcomp/odd_order/PFsection6.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 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 diff --git a/mathcomp/odd_order/PFsection8.v b/mathcomp/odd_order/PFsection8.v index fd085f6..d4ffa46 100644 --- a/mathcomp/odd_order/PFsection8.v +++ b/mathcomp/odd_order/PFsection8.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 diff --git a/mathcomp/odd_order/PFsection9.v b/mathcomp/odd_order/PFsection9.v index e7f82bc..0cd1109 100644 --- a/mathcomp/odd_order/PFsection9.v +++ b/mathcomp/odd_order/PFsection9.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 diff --git a/mathcomp/odd_order/stripped_odd_order_theorem.v b/mathcomp/odd_order/stripped_odd_order_theorem.v index 05c24a9..19b9d0b 100644 --- a/mathcomp/odd_order/stripped_odd_order_theorem.v +++ b/mathcomp/odd_order/stripped_odd_order_theorem.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 mathcomp.ssreflect.ssreflect. From mathcomp diff --git a/mathcomp/odd_order/wielandt_fixpoint.v b/mathcomp/odd_order/wielandt_fixpoint.v index 4f40c11..3a9a099 100644 --- a/mathcomp/odd_order/wielandt_fixpoint.v +++ b/mathcomp/odd_order/wielandt_fixpoint.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