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 countNzSemiRingType == countable nzSemiRingType interface countNzRingType == countable nzRingType interface countComNzSemiRingType == countable comNzSemiRingType interface countComNzRingType == countable comNzRingType 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.

Set Implicit Arguments.

Local Open Scope ring_scope.
Import GRing.Theory CodeSeq.

Module CountRing.

Import GRing.Theory.

#[short (type ="countNmodType")]
HB.structure Definition Nmodule := {M of GRing.Nmodule M & Countable M }.

#[short (type ="countZmodType")]
HB.structure Definition Zmodule := {M of GRing.Zmodule M & Countable M }.

#[short (type ="countNzSemiRingType")]
HB.structure Definition NzSemiRing := {R of GRing.NzSemiRing R & Countable R }.

#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.NzSemiRing instead.")]
Notation SemiRing R := (NzSemiRing R) (only parsing).

Module SemiRing.
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.NzSemiRing.sort instead.")]
Notation sort := (NzSemiRing.sort) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.NzSemiRing.on instead.")]
Notation on R := (NzSemiRing.on R) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.NzSemiRing.copy instead.")]
Notation copy T U := (NzSemiRing.copy T U) (only parsing).
End SemiRing.

#[short (type ="countNzRingType")]
HB.structure Definition NzRing := {R of GRing.NzRing R & Countable R }.

#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.NzRing instead.")]
Notation Ring R := (NzRing R) (only parsing).

Module Ring.
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.NzRing.sort instead.")]
Notation sort := (NzRing.sort) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.NzRing.on instead.")]
Notation on R := (NzRing.on R) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.NzRing.copy instead.")]
Notation copy T U := (NzRing.copy T U) (only parsing).
End Ring.

#[short (type ="countComNzSemiRingType")]
HB.structure Definition ComNzSemiRing :=
  {R of GRing.ComNzSemiRing R & Countable R }.

#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.ComNzSemiRing instead.")]
Notation ComSemiRing R := (ComNzSemiRing R) (only parsing).

Module ComSemiRing.
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.ComNzSemiRing.sort instead.")]
Notation sort := (ComNzSemiRing.sort) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.ComNzSemiRing.on instead.")]
Notation on R := (ComNzSemiRing.on R) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.ComNzSemiRing.copy instead.")]
Notation copy T U := (ComNzSemiRing.copy T U) (only parsing).
End ComSemiRing.

#[short (type ="countComNzRingType")]
HB.structure Definition ComNzRing := {R of GRing.ComNzRing R & Countable R }.

#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.ComNzRing instead.")]
Notation ComRing R := (ComNzRing R) (only parsing).

Module ComRing.
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.ComNzRing.sort instead.")]
Notation sort := (ComNzRing.sort) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.ComNzRing.on instead.")]
Notation on R := (ComNzRing.on R) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use CountRing.ComNzRing.copy instead.")]
Notation copy T U := (ComNzRing.copy T U) (only parsing).
End ComRing.

#[short (type ="countUnitRingType")]
HB.structure Definition UnitRing := {R of GRing.UnitRing R & Countable R }.

#[short (type ="countComUnitRingType")]
HB.structure Definition ComUnitRing := {R of GRing.ComUnitRing R & Countable R }.

#[short (type ="countIdomainType")]
HB.structure Definition IntegralDomain :=
  {R of GRing.IntegralDomain R & Countable R }.

#[short (type ="countFieldType")]
HB.structure Definition Field := {R of GRing.Field R & Countable R }.

#[short (type ="countDecFieldType")]
HB.structure Definition DecidableField :=
  {R of GRing.DecidableField R & Countable R }.

#[short (type ="countClosedFieldType")]
HB.structure Definition ClosedField := {R of GRing.ClosedField R & Countable R }.

#[export ]
HB.instance Definition _ (R : countNmodType ) := Nmodule.on R ^o.
#[export ]
HB.instance Definition _ (R : countZmodType ) := Zmodule.on R ^o.
#[export ]
HB.instance Definition _ (R : countNzSemiRingType ) := NzSemiRing.on R ^o.
#[export ]
HB.instance Definition _ (R : countNzRingType ) := NzRing.on R ^o.

End CountRing.

Import CountRing.

#[deprecated(since="mathcomp 2.4.0",
             note="Use countNzSemiRingType instead.")]
Notation countSemiRingType := (countNzSemiRingType) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use countNzRingType instead.")]
Notation countRingType := (countNzRingType) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use countComNzSemiRingType instead.")]
Notation countComSemiRingType := (countComNzSemiRingType) (only parsing).
#[deprecated(since="mathcomp 2.4.0",
             note="Use countComNzRingType instead.")]
Notation countComRingType := (countComNzRingType) (only parsing).