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/character/all_character.v | 14 +++++++------- mathcomp/character/classfun.v | 3 ++- 2 files changed, 9 insertions(+), 8 deletions(-) (limited to 'mathcomp/character') diff --git a/mathcomp/character/all_character.v b/mathcomp/character/all_character.v index 936fa6c..03f1b57 100644 --- a/mathcomp/character/all_character.v +++ b/mathcomp/character/all_character.v @@ -1,7 +1,7 @@ -Require Export character. -Require Export classfun. -Require Export inertia. -Require Export integral_char. -Require Export mxabelem. -Require Export mxrepresentation. -Require Export vcharacter. +From mathcomp Require Export character. +From mathcomp Require Export classfun. +From mathcomp Require Export inertia. +From mathcomp Require Export integral_char. +From mathcomp Require Export mxabelem. +From mathcomp Require Export mxrepresentation. +From mathcomp Require Export vcharacter. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 4c27bd7..7473338 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -969,7 +969,8 @@ 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 ?normr_ge0 ?cfnorm_ge0 //. +rewrite (mono_in_lerif (@ler_sqrtC _)) 1?rpredM ?qualifE; +rewrite ?normr_ge0 ?cfnorm_ge0 //. exact: cfCauchySchwarz. Qed. -- 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/character/character.v | 2 +- mathcomp/character/classfun.v | 2 +- mathcomp/character/inertia.v | 2 +- mathcomp/character/integral_char.v | 2 +- mathcomp/character/mxabelem.v | 2 +- mathcomp/character/mxrepresentation.v | 2 +- mathcomp/character/vcharacter.v | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) (limited to 'mathcomp/character') diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 89c7697..0738b14 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.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/character/classfun.v b/mathcomp/character/classfun.v index 7473338..54cbc41 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.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/character/inertia.v b/mathcomp/character/inertia.v index f06ae9e..3890fdd 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.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/character/integral_char.v b/mathcomp/character/integral_char.v index 4320307..ad2980f 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.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/character/mxabelem.v b/mathcomp/character/mxabelem.v index aa14808..c178d75 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.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/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 7eef614..6dd4eec 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.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/character/vcharacter.v b/mathcomp/character/vcharacter.v index a1bc40e..5b1ff05 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.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