From fbf0b7568b8d6231671954cba8bcae4120e591cc Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 5 Feb 2019 15:38:39 +0100 Subject: Make an appropriate use of the order library everywhere (#278, #280, #282, #283, #285, #286, #288, #296, #330, #334, and #341) ssrnum related changes: - Redefine the intermediate structure between `idomainType` and `numDomainType`, which is `normedDomainType` (normed integral domain without an order). - Generalize (by using `normedDomainType` or the order structures), relocate (to order.v), and rename ssrnum related definitions and lemmas. - Add a compatibility module `Num.mc_1_9` and export it to check compilation. - Remove the use of the deprecated definitions and lemmas from entire theories. - Implement factories mechanism to construct several ordered and num structures from fewer axioms. order related changes: - Reorganize the hierarchy of finite lattice structures. Finite lattices have top and bottom elements except for empty set. Therefore we removed finite lattice structures without top and bottom. - Reorganize the theory modules in order.v: + `LTheory` (lattice and partial order, without complement and totality) + `CTheory` (`LTheory` + complement) + `Theory` (all) - Give a unique head symbol for `Total.mixin_of`. - Replace reverse and `^r` with converse and `^c` respectively. - Fix packing and cloning functions and notations. - Provide more ordered type instances: Products and lists can be ordered in two different ways: the lexicographical ordering and the pointwise ordering. Now their canonical instances are not exported to make the users choose them. - Export `Order.*.Exports` modules by default. - Specify the core hint database explicitly in order.v. (see #252) - Apply 80 chars per line restriction. General changes: - Give consistency to shape of formulae and namings of `lt_def` and `lt_neqAle` like lemmas: lt_def x y : (x < y) = (y != x) && (x <= y), lt_neqAle x y : (x < y) = (x != y) && (x <= y). - Enable notation overloading by using scopes and displays: + Define `min` and `max` notations (`minr` and `maxr` for `ring_display`) as aliases of `meet` and `join` specialized for `total_display`. + Provide the `ring_display` version of `le`, `lt`, `ge`, `gt`, `leif`, and `comparable` notations and their explicit variants in `Num.Def`. + Define 3 variants of `[arg min_(i < n | P) F]` and `[arg max_(i < n | P) F]` notations in `nat_scope` (specialized for nat), `order_scope` (general version), and `ring_scope` (specialized for `ring_display`). - Update documents and put CHANGELOG entries. --- mathcomp/character/character.v | 33 ++++++++++++++++----------------- mathcomp/character/classfun.v | 23 +++++++++++------------ mathcomp/character/inertia.v | 24 ++++++++++++------------ mathcomp/character/integral_char.v | 28 ++++++++++++++-------------- mathcomp/character/vcharacter.v | 31 +++++++++++++++---------------- 5 files changed, 68 insertions(+), 71 deletions(-) (limited to 'mathcomp/character') diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index c95d03b..78c5295 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -1,9 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice ssrnat seq. -From mathcomp Require Import path div fintype tuple finfun bigop prime ssralg. -From mathcomp Require Import poly finset gproduct fingroup morphism perm. -From mathcomp Require Import automorphism quotient finalg action zmodp. +From mathcomp Require Import path div fintype tuple finfun bigop prime order. +From mathcomp Require Import ssralg poly finset gproduct fingroup morphism. +From mathcomp Require Import perm automorphism quotient finalg action zmodp. From mathcomp Require Import commutator cyclic center pgroup nilpotent sylow. From mathcomp Require Import abelian matrix mxalgebra mxpoly mxrepresentation. From mathcomp Require Import vector ssrnum algC classfun. @@ -67,7 +67,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GroupScope GRing.Theory Num.Theory. +Import Order.TTheory GroupScope GRing.Theory Num.Theory. Local Open Scope ring_scope. Local Notation algCF := [fieldType of algC]. @@ -656,7 +656,7 @@ Lemma irr1_gt0 i : 0 < 'chi_i 1%g. Proof. by rewrite irr1_degree ltr0n irr_degree_gt0. Qed. Lemma irr1_neq0 i : 'chi_i 1%g != 0. -Proof. by rewrite eqr_le ltr_geF ?irr1_gt0. Qed. +Proof. by rewrite eq_le lt_geF ?irr1_gt0. Qed. Lemma irr_neq0 i : 'chi_i != 0. Proof. by apply: contraNneq (irr1_neq0 i) => ->; rewrite cfunE. Qed. @@ -880,7 +880,7 @@ Lemma char1_eq0 chi : chi \is a character -> (chi 1%g == 0) = (chi == 0). Proof. case/char_sum_irr=> r ->; apply/idP/idP=> [|/eqP->]; last by rewrite cfunE. case: r => [|i r]; rewrite ?big_nil // sum_cfunE big_cons. -rewrite paddr_eq0 ?sumr_ge0 => // [||j _]; rewrite 1?ltrW ?irr1_gt0 //. +rewrite paddr_eq0 ?sumr_ge0 => // [||j _]; rewrite 1?ltW ?irr1_gt0 //. by rewrite (negbTE (irr1_neq0 i)). Qed. @@ -1021,7 +1021,7 @@ Proof. by move=> Gx; rewrite -lin_charX // expg_order lin_char1. Qed. Lemma normC_lin_char x : x \in G -> `|xi x| = 1. Proof. -move=> Gx; apply/eqP; rewrite -(@pexpr_eq1 _ _ #[x]) ?normr_ge0 //. +move=> Gx; apply/eqP; rewrite -(@pexpr_eq1 _ _ #[x]) //. by rewrite -normrX // lin_char_unity_root ?normr1. Qed. @@ -1163,12 +1163,11 @@ have exp_e j: e 0 j ^+ #[x] = 1. rewrite expgS repr_mxM ?groupX // {1}rGx -!mulmxA mulKVmx //. by rewrite mul_diag_mx mulmxA [M in _ = M]mxE -IHn exprS {1}mxE eqxx. have norm1_e j: `|e 0 j| = 1. - apply/eqP; rewrite -(@pexpr_eq1 _ _ #[x]) ?normr_ge0 //. - by rewrite -normrX exp_e normr1. + by apply/eqP; rewrite -(@pexpr_eq1 _ _ #[x]) // -normrX exp_e normr1. exists e; split=> //; first by exists B. rewrite cfRepr1 !cfunE Gx rGx mxtrace_mulC mulKVmx // mxtrace_diag. - split=> //=; apply: (ler_trans (ler_norm_sum _ _ _)). - by rewrite (eq_bigr _ (in1W norm1_e)) sumr_const card_ord lerr. + split=> //=; apply: (le_trans (ler_norm_sum _ _ _)). + by rewrite (eq_bigr _ (in1W norm1_e)) sumr_const card_ord lexx. rewrite !cfunE groupV !mulrb Gx rGx mxtrace_mulC mulKVmx //. rewrite -trace_map_mx map_diag_mx; set d' := diag_mx _. rewrite -[d'](mulKVmx unitB) mxtrace_mulC -[_ *m _](repr_mxK rG Gx) rGx. @@ -1559,7 +1558,7 @@ Lemma constt_ortho_char (phi psi : 'CF(G)) i j : Proof. move=> _ _ /constt_charP[//|phi1 Nphi1 ->] /constt_charP[//|psi1 Npsi1 ->]. rewrite cfdot_irr; case: eqP => // -> /eqP/idPn[]. -rewrite cfdotDl !cfdotDr cfnorm_irr -addrA gtr_eqF ?ltr_paddr ?ltr01 //. +rewrite cfdotDl !cfdotDr cfnorm_irr -addrA gt_eqF ?ltr_paddr ?ltr01 //. by rewrite Cnat_ge0 ?rpredD ?Cnat_cfdot_char ?irr_char. Qed. @@ -1756,7 +1755,7 @@ Lemma constt_Res_trans j psi : psi \is a character -> j \in irr_constt psi -> {subset irr_constt ('Res[H, G] 'chi_j) <= irr_constt ('Res[H] psi)}. Proof. -move=> Npsi Cj i; apply: contraNneq; rewrite eqr_le => {1}<-. +move=> Npsi Cj i; apply: contraNneq; rewrite eq_le => {1}<-. rewrite cfdot_Res_ge_constt ?Cnat_ge0 ?Cnat_cfdot_char_irr //. by rewrite cfRes_char ?irr_char. Qed. @@ -2859,18 +2858,18 @@ by rewrite cfcenter_eq_center subsetIr. Qed. (* This is Isaacs (2.29). *) -Lemma cfnorm_Res_lerif H phi : +Lemma cfnorm_Res_leif H phi : H \subset G -> '['Res[H] phi] <= #|G : H|%:R * '[phi] ?= iff (phi \in 'CF(G, H)). Proof. move=> sHG; rewrite cfun_onE mulrCA natf_indexg // -mulrA mulKf ?neq0CG //. rewrite (big_setID H) (setIidPr sHG) /= addrC. -rewrite (mono_lerif (ler_pmul2l _)) ?invr_gt0 ?gt0CG // -lerif_subLR -sumrB. +rewrite (mono_leif (ler_pmul2l _)) ?invr_gt0 ?gt0CG // -leif_subLR -sumrB. rewrite big1 => [|x Hx]; last by rewrite !cfResE ?subrr. have ->: (support phi \subset H) = (G :\: H \subset [set x | phi x == 0]). rewrite subDset setUC -subDset; apply: eq_subset => x. by rewrite !inE (andb_idr (contraR _)) // => /cfun0->. -rewrite (sameP subsetP forall_inP); apply: lerif_0_sum => x _. +rewrite (sameP subsetP forall_inP); apply: leif_0_sum => x _. by rewrite !inE /] := cfcenter_Res 'chi_i. have /irrP[j ->] := lin_char_irr Lxi; rewrite cfdotZl cfdotZr cfdot_irr eqxx. by rewrite mulr1 irr1_degree conjC_nat. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 3f461e3..c8ae7b1 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path. -From mathcomp Require Import div choice fintype tuple finfun bigop prime. +From mathcomp Require Import div choice fintype tuple finfun bigop prime order. From mathcomp Require Import ssralg poly finset fingroup morphism perm. From mathcomp Require Import automorphism quotient finalg action gproduct. From mathcomp Require Import zmodp commutator cyclic center pgroup sylow. @@ -91,7 +91,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GroupScope GRing.Theory Num.Theory. +Import Order.TTheory GroupScope GRing.Theory Num.Theory. Local Open Scope ring_scope. Delimit Scope cfun_scope with CF. @@ -900,7 +900,7 @@ by rewrite phi0 // => y _; apply: mul_conjC_ge0. Qed. Lemma cfnorm_gt0 phi : ('[phi] > 0) = (phi != 0). -Proof. by rewrite ltr_def cfnorm_ge0 cfnorm_eq0 andbT. Qed. +Proof. by rewrite lt_def cfnorm_ge0 cfnorm_eq0 andbT. Qed. Lemma sqrt_cfnorm_ge0 phi : 0 <= sqrtC '[phi]. Proof. by rewrite sqrtC_ge0 cfnorm_ge0. Qed. @@ -944,7 +944,7 @@ Lemma cfCauchySchwarz phi psi : Proof. rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC. have [-> | nz_psi] /= := altP (psi =P 0). - by apply/lerifP; rewrite !cfdot0r normCK mul0r mulr0. + by apply/leifP; rewrite !cfdot0r normCK mul0r mulr0. without loss ophi: phi / '[phi, psi] = 0. move=> IHo; pose a := '[phi, psi] / '[psi]; pose phi1 := phi - a *: psi. have ophi: '[phi1, psi] = 0. @@ -952,7 +952,7 @@ without loss ophi: phi / '[phi, psi] = 0. rewrite (canRL (subrK _) (erefl phi1)) rpredDr ?rpredZ ?memv_line //. rewrite cfdotDl ophi add0r cfdotZl normrM (ger0_norm (cfnorm_ge0 _)). rewrite exprMn mulrA -cfnormZ cfnormDd; last by rewrite cfdotZr ophi mulr0. - by have:= IHo _ ophi; rewrite mulrDl -lerif_subLR subrr ophi normCK mul0r. + by have:= IHo _ ophi; rewrite mulrDl -leif_subLR subrr ophi normCK mul0r. rewrite ophi normCK mul0r; split; first by rewrite mulr_ge0 ?cfnorm_ge0. rewrite eq_sym mulf_eq0 orbC cfnorm_eq0 (negPf nz_psi) /=. apply/idP/idP=> [|/vlineP[a {2}->]]; last by rewrite cfdotZr ophi mulr0. @@ -963,20 +963,19 @@ Lemma cfCauchySchwarz_sqrt phi psi : `|'[phi, psi]| <= sqrtC '[phi] * sqrtC '[psi] ?= iff ~~ free (phi :: psi). Proof. rewrite -(sqrCK (normr_ge0 _)) -sqrtCM ?qualifE ?cfnorm_ge0 //. -rewrite (mono_in_lerif (@ler_sqrtC _)) 1?rpredM ?qualifE; -rewrite ?normr_ge0 ?cfnorm_ge0 //. +rewrite (mono_in_leif (@ler_sqrtC _)) 1?rpredM ?qualifE ?cfnorm_ge0 //. exact: cfCauchySchwarz. Qed. -Lemma cf_triangle_lerif phi psi : +Lemma cf_triangle_leif phi psi : sqrtC '[phi + psi] <= sqrtC '[phi] + sqrtC '[psi] ?= iff ~~ free (phi :: psi) && (0 <= coord [tuple psi] 0 phi). Proof. -rewrite -(mono_in_lerif ler_sqr) ?rpredD ?qualifE ?sqrtC_ge0 ?cfnorm_ge0 //. -rewrite andbC sqrrD !sqrtCK addrAC cfnormD (mono_lerif (ler_add2l _)). +rewrite -(mono_in_leif ler_sqr) ?rpredD ?qualifE ?sqrtC_ge0 ?cfnorm_ge0 //. +rewrite andbC sqrrD !sqrtCK addrAC cfnormD (mono_leif (ler_add2l _)). rewrite -mulr_natr -[_ + _](divfK (negbT (eqC_nat 2 0))) -/('Re _). -rewrite (mono_lerif (ler_pmul2r _)) ?ltr0n //. -have:= lerif_trans (lerif_Re_Creal '[phi, psi]) (cfCauchySchwarz_sqrt phi psi). +rewrite (mono_leif (ler_pmul2r _)) ?ltr0n //. +have:= leif_trans (leif_Re_Creal '[phi, psi]) (cfCauchySchwarz_sqrt phi psi). congr (_ <= _ ?= iff _); apply: andb_id2r. rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC. have [-> | nz_psi] := altP (psi =P 0); first by rewrite cfdot0r coord0. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index c644150..3809e73 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. -From mathcomp Require Import choice div fintype tuple finfun bigop prime. +From mathcomp Require Import choice fintype div tuple finfun bigop prime order. From mathcomp Require Import ssralg ssrnum finset fingroup morphism perm. From mathcomp Require Import automorphism quotient action zmodp cyclic center. From mathcomp Require Import gproduct commutator gseries nilpotent pgroup. @@ -12,7 +12,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GroupScope GRing.Theory Num.Theory. +Import Order.TTheory GroupScope GRing.Theory Num.Theory. Local Open Scope ring_scope. (******************************************************************************) @@ -938,7 +938,7 @@ have AtoB_P s (psi := 'chi_s) (chi := 'Ind[G] psi): s \in calA -> have ub_chi_r: 'chi_r 1%g <= chi 1%g ?= iff ('chi_r == chi). have Nchi: chi \is a character by rewrite cfInd_char ?irr_char. have [chi1 Nchi1->] := constt_charP _ Nchi sGr. - rewrite addrC cfunE -lerif_subLR subrr eq_sym -subr_eq0 addrK. + rewrite addrC cfunE -leif_subLR subrr eq_sym -subr_eq0 addrK. by split; rewrite ?char1_ge0 // eq_sym char1_eq0. have lb_chi_r: chi 1%g <= 'chi_r 1%g ?= iff (f == e). rewrite cfInd1 // -(cfRes1 H) DpsiH -(cfRes1 H 'chi_r) DrH !cfunE sum_cfunE. @@ -946,10 +946,10 @@ have AtoB_P s (psi := 'chi_s) (chi := 'Ind[G] psi): s \in calA -> by case/cfclassP=> y _ ->; rewrite cfConjg1. rewrite reindex_cfclass //= sumr_const -(eq_card (cfclass_IirrE _ _)). rewrite mulr_natl mulrnAr card_cfclass_Iirr //. - rewrite (mono_lerif (ler_pmuln2r (indexg_gt0 G T))). - rewrite (mono_lerif (ler_pmul2r (irr1_gt0 t))); apply: lerif_eq. + rewrite (mono_leif (ler_pmuln2r (indexg_gt0 G T))). + rewrite (mono_leif (ler_pmul2r (irr1_gt0 t))); apply: leif_eq. by rewrite /e -(cfResRes _ sHT) ?cfdot_Res_ge_constt. - have [_ /esym] := lerif_trans ub_chi_r lb_chi_r; rewrite eqxx. + have [_ /esym] := leif_trans ub_chi_r lb_chi_r; rewrite eqxx. by case/andP=> /eqP Dchi /eqP->; rewrite cfIirrE -/chi -?Dchi ?mem_irr. have part_c: {in calA, forall s (chi := 'Ind[G] 'chi_s), [predI irr_constt ('Res[T] chi) & calA] =i pred1 s}. @@ -957,14 +957,14 @@ have part_c: {in calA, forall s (chi := 'Ind[G] 'chi_s), have chiTs: s \in irr_constt ('Res[T] chi). by rewrite irr_consttE cfdot_Res_l irrWnorm ?oner_eq0. apply/andP/eqP=> [[/= chiTs1 As1] | -> //]. - apply: contraTeq Dchi_theta => s's1; rewrite ltr_eqF // -/chi. + apply: contraTeq Dchi_theta => s's1; rewrite lt_eqF // -/chi. have [|phi Nphi DchiT] := constt_charP _ _ chiTs. by rewrite cfRes_char ?cfInd_char ?irr_char. have [|phi1 Nphi1 Dphi] := constt_charP s1 Nphi _. rewrite irr_consttE -(canLR (addKr _) DchiT) addrC cfdotBl cfdot_irr. by rewrite mulrb ifN_eqC ?subr0. rewrite -(cfResRes chi sHT sTG) DchiT Dphi !rmorphD !cfdotDl /=. - rewrite -ltr_subl_addl subrr ltr_paddr ?ltr_def //; + rewrite -ltr_subl_addl subrr ltr_paddr ?lt_def //; rewrite Cnat_ge0 ?Cnat_cfdot_char ?cfRes_char ?irr_char //. by rewrite andbT -irr_consttE -constt_Ind_Res. do [split=> //; try by move=> s /AtoB_P[]] => [s1 s2 As1 As2 | r]. @@ -1039,8 +1039,8 @@ have [_]: '['Ind[G] phi] <= '['Ind[G] psi] ?= iff d_delta. rewrite DpsiG cfdot_suml; apply: eq_bigr => b _. rewrite -scalerAl cfdotZl cfdot_sumr; congr (_ * _). by apply: eq_bigr => g _; rewrite -scalerAl cfdotZr conj_Cnat. - have eMmono := mono_lerif (ler_pmul2l (egt0 _ _)). - apply: lerif_sum => b /eMmono->; apply: lerif_sum => g /eMmono->. + have eMmono := mono_leif (ler_pmul2l (egt0 _ _)). + apply: leif_sum => b /eMmono->; apply: leif_sum => g /eMmono->. split; last exact: eq_sym. have /CnatP[n Dd]: d b g \in Cnat by rewrite Cnat_cfdot_char. have [Db | _] := eqP; rewrite Dd leC_nat // -ltC_nat -Dd Db cfnorm_gt0. @@ -1059,7 +1059,7 @@ apply/idP/idP=> [|/imageP[b Sb ->]]. apply: contraR => N'i; rewrite big1 // => b Sb. rewrite cfdotZl cfdot_irr mulrb ifN_eqC ?mulr0 //. by apply: contraNneq N'i => ->; apply: image_f. -rewrite gtr_eqF // (bigD1 b) //= cfdotZl cfnorm_irr mulr1 ltr_paddr ?egt0 //. +rewrite gt_eqF // (bigD1 b) //= cfdotZl cfnorm_irr mulr1 ltr_paddr ?egt0 //. apply: sumr_ge0 => g /andP[Sg _]; rewrite cfdotZl cfdot_irr. by rewrite mulr_ge0 ?ler0n ?Cnat_ge0. Qed. @@ -1186,7 +1186,7 @@ have ltUK: U \proper K. rewrite Dmu subGcfker -irr_eq1 -Dmu cfMod_eq1 //. by rewrite (can2_eq (divrK Uj) (mulrK Uj)) mul1r (inj_eq irr_inj). suffices: theta \in 'CF(K, L). - rewrite -cfnorm_Res_lerif // DthL cfnormZ !cfnorm_irr !mulr1 normr_nat. + rewrite -cfnorm_Res_leif // DthL cfnormZ !cfnorm_irr !mulr1 normr_nat. by rewrite -natrX eqC_nat => /eqP. have <-: gcore U G = L. apply: maxL; last by rewrite sub_gcore ?cfker_mod. diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index 22bd171..1022afa 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path. -From mathcomp Require Import div choice fintype tuple finfun bigop prime. +From mathcomp Require Import div choice fintype tuple finfun bigop prime order. From mathcomp Require Import ssralg poly finset fingroup morphism perm. From mathcomp Require Import automorphism quotient action finalg zmodp. From mathcomp Require Import commutator cyclic center pgroup sylow gseries. @@ -34,7 +34,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GroupScope GRing.Theory Num.Theory. +Import Order.TTheory GroupScope GRing.Theory Num.Theory. Local Open Scope ring_scope. Lemma group_num_field_exists (gT : finGroupType) (G : {group gT}) : @@ -274,7 +274,7 @@ have nz_m: m%:R != 0 :> algC by rewrite pnatr_eq0 -lt0n. pose alpha := 'chi_i g / m%:R. have a_lt1: `|alpha| < 1. rewrite normrM normfV normr_nat -{2}(divff nz_m). - rewrite ltr_def (can_eq (mulfVK nz_m)) eq_sym -{1}Dm -irr_cfcenterE // notZg. + rewrite lt_def (can_eq (mulfVK nz_m)) eq_sym -{1}Dm -irr_cfcenterE // notZg. by rewrite ler_pmul2r ?invr_gt0 ?ltr0n // -Dm char1_ge_norm ?irr_char. have Za: alpha \in Aint. have [u _ /dvdnP[v eq_uv]] := Bezoutl #|g ^: G| m_gt0. @@ -304,13 +304,13 @@ have Zbeta: beta \in Cint. have [|nz_a] := boolP (alpha == 0). by rewrite (can2_eq (divfK _) (mulfK _)) // mul0r => /eqP. have: beta != 0 by rewrite Dbeta; apply/prodf_neq0 => nu _; rewrite fmorph_eq0. -move/(norm_Cint_ge1 Zbeta); rewrite ltr_geF //; apply: ler_lt_trans a_lt1. +move/(norm_Cint_ge1 Zbeta); rewrite lt_geF //; apply: le_lt_trans a_lt1. rewrite -[`|alpha|]mulr1 Dbeta (bigD1 1%g) ?group1 //= -Da. -case: (gQnC _) => /= _ <-; rewrite gal_id normrM. -rewrite -subr_ge0 -mulrBr mulr_ge0 ?normr_ge0 // Da subr_ge0. -elim/big_rec: _ => [|nu c _]; first by rewrite normr1 lerr. -apply: ler_trans; rewrite -subr_ge0 -{1}[`|c|]mul1r normrM -mulrBl. -by rewrite mulr_ge0 ?normr_ge0 // subr_ge0 norm_a_nu. +case: (gQnC _) => /= _ <-. +rewrite gal_id normrM -subr_ge0 -mulrBr mulr_ge0 // Da subr_ge0. +elim/big_rec: _ => [|nu c _]; first by rewrite normr1 lexx. +apply: le_trans; rewrite -subr_ge0 -{1}[`|c|]mul1r normrM -mulrBl. +by rewrite mulr_ge0 // subr_ge0 norm_a_nu. Qed. End GringIrrMode. @@ -677,18 +677,18 @@ have{pi1 Zpi1} pi2_ge1: 1 <= pi2. by rewrite Cint_normK // sqr_Cint_ge1 //; apply/prodf_neq0. have Sgt0: (#|S| > 0)%N by rewrite (cardD1 g) [g \in S]Sg. rewrite -mulr_natr -ler_pdivl_mulr ?ltr0n //. -have n2chi_ge0 s: s \in S -> 0 <= `|chi s| ^+ 2 by rewrite exprn_ge0 ?normr_ge0. +have n2chi_ge0 s: s \in S -> 0 <= `|chi s| ^+ 2 by rewrite exprn_ge0. rewrite -(expr_ge1 Sgt0); last by rewrite divr_ge0 ?ler0n ?sumr_ge0. -by rewrite (ler_trans pi2_ge1) // lerif_AGM. +by rewrite (le_trans pi2_ge1) // leif_AGM. Qed. (* This is Burnside's vanishing theorem (Isaacs, Theorem (3.15)). *) Theorem nonlinear_irr_vanish gT (G : {group gT}) i : 'chi[G]_i 1%g > 1 -> exists2 x, x \in G & 'chi_i x = 0. Proof. -move=> chi1gt1; apply/exists_eq_inP; apply: contraFT (ltr_geF chi1gt1). -move/exists_inPn => -nz_chi. -rewrite -(norm_Cnat (Cnat_irr1 i)) -(@expr_le1 _ 2) ?normr_ge0 //. +move=> chi1gt1; apply/exists_eq_inP; apply: contraFT (lt_geF chi1gt1). +move=> /exists_inPn-nz_chi. +rewrite -(norm_Cnat (Cnat_irr1 i)) -(@expr_le1 _ 2)//. rewrite -(ler_add2r (#|G|%:R * '['chi_i])) {1}cfnorm_irr mulr1. rewrite (cfnormE (cfun_onG _)) mulVKf ?neq0CG // (big_setD1 1%g) //=. rewrite addrCA ler_add2l (cardsD1 1%g) group1 mulrS ler_add2l. diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index 72bacc3..e886c5a 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path. -From mathcomp Require Import div choice fintype tuple finfun bigop prime. +From mathcomp Require Import div choice fintype tuple finfun bigop prime order. From mathcomp Require Import ssralg poly finset fingroup morphism perm. From mathcomp Require Import automorphism quotient finalg action gproduct. From mathcomp Require Import zmodp commutator cyclic center pgroup sylow. @@ -40,7 +40,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GroupScope GRing.Theory Num.Theory. +Import Order.Theory GroupScope GRing.Theory Num.Theory. Local Open Scope ring_scope. Section Basics. @@ -225,8 +225,8 @@ exists chi1; last exists (- nchi2); last by rewrite opprK. apply: rpred_sum => i zi_ge0; rewrite -tnth_nth rpredZ_Cnat ?irr_char //. by rewrite CnatEint Zz. rewrite -sumrN rpred_sum // => i zi_lt0; rewrite -scaleNr -tnth_nth. -rewrite rpredZ_Cnat ?irr_char // CnatEint rpredN Zz oppr_ge0 ltrW //. -by rewrite real_ltrNge ?Creal_Cint. +rewrite rpredZ_Cnat ?irr_char // CnatEint rpredN Zz oppr_ge0 ltW //. +by rewrite real_ltNge ?Creal_Cint. Qed. Lemma Aint_vchar phi x : phi \in 'Z[irr G] -> phi x \in Aint. @@ -501,8 +501,8 @@ have neq_ji: j != i. by rewrite signr_eq0. have neq_bc: b != c. apply: contraTneq phi1_0; rewrite def_phi def_chi def_xi => ->. - rewrite -scalerDr !cfunE mulf_eq0 signr_eq0 eqr_le ltr_geF //. - by rewrite ltr_paddl ?ltrW ?irr1_gt0. + rewrite -scalerDr !cfunE mulf_eq0 signr_eq0 eq_le lt_geF //. + by rewrite ltr_paddl ?ltW ?irr1_gt0. rewrite {}def_phi {}def_chi {}def_xi !scaler_sign. case: b c neq_bc => [|] [|] // _; last by exists i, j. by exists j, i; rewrite 1?eq_sym // addrC. @@ -691,8 +691,8 @@ have def_phi: {in H, phi =1 'chi_i}. have [j def_chi_j]: {j | 'chi_j = phi}. apply/sig_eqW; have [[] [j]] := vchar_norm1P Zphi n1phi; last first. by rewrite scale1r; exists j. - move/cfunP/(_ 1%g)/eqP; rewrite scaleN1r def_phi // cfunE -addr_eq0 eqr_le. - by rewrite ltr_geF // ltr_paddl ?ltrW ?irr1_gt0. + move/cfunP/(_ 1%g)/eqP; rewrite scaleN1r def_phi // cfunE -addr_eq0 eq_le. + by rewrite lt_geF // ltr_paddl ?ltW ?irr1_gt0. exists j; rewrite ?cfkerEirr def_chi_j //; apply/subsetP => x /setDP[Gx notHx]. rewrite inE cfunE def_phi // cfunE -/a cfun1E // Gx mulr1 cfIndE //. rewrite big1 ?mulr0 ?add0r // => y Gy; apply/theta0/(contra _ notHx) => Hxy. @@ -834,7 +834,7 @@ Proof. by rewrite inE. Qed. Lemma Cnat_dirr (phi : 'CF(G)) i : phi \in 'Z[irr G] -> i \in dirr_constt phi -> '[phi, dchi i] \in Cnat. Proof. -move=> PiZ; rewrite CnatEint dirr_consttE andbC => /ltrW -> /=. +move=> PiZ; rewrite CnatEint dirr_consttE andbC => /ltW -> /=. by case: i => b i; rewrite cfdotZr rmorph_sign rpredMsign Cint_cfdot_vchar_irr. Qed. @@ -846,15 +846,14 @@ Lemma dirr_constt_oppI (phi: 'CF(G)) : dirr_constt phi :&: dirr_constt (-phi) = set0. Proof. apply/setP=> i; rewrite inE !dirr_consttE cfdotNl inE. -apply/idP=> /andP [L1 L2]; have := ltr_paddl (ltrW L1) L2. -by rewrite subrr ltr_def eqxx. +apply/idP=> /andP [L1 L2]; have := ltr_paddl (ltW L1) L2. +by rewrite subrr lt_def eqxx. Qed. Lemma dirr_constt_oppl (phi: 'CF(G)) i : - i \in dirr_constt phi -> (ndirr i) \notin dirr_constt phi. + i \in dirr_constt phi -> (ndirr i) \notin dirr_constt phi. Proof. -rewrite !dirr_consttE dchi_ndirrE cfdotNr oppr_gt0. -by move/ltrW=> /ler_gtF ->. +by rewrite !dirr_consttE dchi_ndirrE cfdotNr oppr_gt0 => /ltW /le_gtF ->. Qed. Definition to_dirr (B : {set gT}) (phi : 'CF(B)) (i : Iirr B) : dIirr B := @@ -876,7 +875,7 @@ Lemma of_irrK (phi: 'CF(G)) : {in dirr_constt phi, cancel (@of_irr G) (to_dirr phi)}. Proof. case=> b i; rewrite dirr_consttE cfdotZr rmorph_sign /= /to_dirr mulr_sign. -by rewrite fun_if oppr_gt0; case: b => [|/ltrW/ler_gtF] ->. +by rewrite fun_if oppr_gt0; case: b => [|/ltW/le_gtF] ->. Qed. Lemma cfdot_todirrE (phi: 'CF(G)) i (phi_i := dchi (to_dirr phi i)) : @@ -913,7 +912,7 @@ Lemma dirr_small_norm (phi : 'CF(G)) n : Proof. move=> PiZ Pln; rewrite ltnNge -leC_nat => Nl4. suffices Fd i: i \in dirr_constt phi -> '[phi, dchi i] = 1. - split; last 2 [by apply/setP=> u; rewrite !inE cfdotNl oppr_gt0 ltr_asym]. + split; last 2 [by apply/setP=> u; rewrite !inE cfdotNl oppr_gt0 lt_asym]. apply/eqP; rewrite -eqC_nat -sumr_const -Pln (cnorm_dconstt PiZ). by apply/eqP/eq_bigr=> i Hi; rewrite Fd // expr1n. rewrite {1}[phi]cfun_sum_dconstt //. -- cgit v1.2.3