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/integral_char.v | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'mathcomp/character/integral_char.v') 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. -- cgit v1.2.3