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/fingroup/fingroup.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/fingroup') diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 01eea88..70553a0 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -232,7 +232,7 @@ Structure base_type : Type := PackBase { (* coercion of A * B to pred_sort in x \in A * B, or rho * tau to *) (* ffun and Funclass in (rho * tau) x, when rho tau : perm T. *) (* Therefore we define an alias of sort for argument types, and *) -(* make it the default coercion FinGroup.base_class >-> Sortclass *) +(* make it the default coercion FinGroup.base_type >-> Sortclass *) (* so that arguments of a functions whose parameters are of type, *) (* say, gT : finGroupType, can be coerced to the coercion class *) (* of arg_sort. Care should be taken, however, to declare the *) -- 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/fingroup/action.v | 2 +- mathcomp/fingroup/automorphism.v | 2 +- mathcomp/fingroup/fingroup.v | 2 +- mathcomp/fingroup/gproduct.v | 2 +- mathcomp/fingroup/morphism.v | 2 +- mathcomp/fingroup/perm.v | 2 +- mathcomp/fingroup/presentation.v | 2 +- mathcomp/fingroup/quotient.v | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) (limited to 'mathcomp/fingroup') diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 6ce38b9..1bde1f7 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.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/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index 5e52e5e..8813b45 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.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/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 70553a0..550aaaa 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.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/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index a8d2fb2..4ee2bc8 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.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/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index f4790e6..9f0a900 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.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/fingroup/perm.v b/mathcomp/fingroup/perm.v index 2f85d78..a306475 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.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/fingroup/presentation.v b/mathcomp/fingroup/presentation.v index afe33fa..ad712ee 100644 --- a/mathcomp/fingroup/presentation.v +++ b/mathcomp/fingroup/presentation.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/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 3fb0774..242b4b7 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.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