Library mathcomp.algebra.countalg

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.