moving countalg and closed_field around

- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style

1 files changed, 8 insertions, 1 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index fca25a9..2a701a2 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -6,7 +6,7 @@ Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
 From mathcomp
 Require Import finfun bigop prime binomial ssralg finset fingroup finalg.
 From mathcomp
-Require Import perm zmodp.
+Require Import perm zmodp countalg.
 
 (******************************************************************************)
 (* Basic concrete linear algebra : definition of type for matrices, and all   *)
@@ -2071,6 +2071,10 @@ Proof.
 by apply/matrixP=> k i; rewrite !mxE; apply: eq_bigr => j _; rewrite !mxE.
 Qed.
 
+Canonical matrix_countZmodType (M : countZmodType) m n :=
+  [countZmodType of 'M[M]_(m, n)].
+Canonical matrix_countRingType (R : countRingType) n :=
+  [countRingType of 'M[R]_n.+1].
 Canonical matrix_finLmodType (R : finRingType) m n :=
   [finLmodType R of 'M[R]_(m, n)].
 Canonical matrix_finRingType (R : finRingType) n' :=
@@ -2644,6 +2648,9 @@ End MatrixInv.
 
 Prenex Implicits unitmx invmx.
 
+Canonical matrix_countUnitRingType (R : countComUnitRingType) n :=
+  [countUnitRingType of 'M[R]_n.+1].
+
 (* Finite inversible matrices and the general linear group. *)
 Section FinUnitMatrix.