Library mathcomp.algebra.countalg

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop ssralg.

The algebraic part of the algebraic hierarchy for countable types This file clones part of ssralg hierarchy for countable types; it does not cover the left module / algebra interfaces, providing only countNmodType == countable nmodType interface countZmodType == countable zmodType interface countSemiRingType == countable semiRingType interface countRingType == countable ringType interface countComSemiRingType == countable comSemiRingType interface countComRingType == countable comRingType interface countUnitRingType == countable unitRingType interface countComUnitRingType == countable comUnitRingType interface countIdomainType == countable idomainType interface countFieldType == countable fieldType interface countDecFieldType == countable decFieldType interface countClosedFieldType == countable closedFieldType interface This file provides constructions for both simple extension and algebraic closure of countable fields.