Library mathcomp.algebra.finalg
(* (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 finset fingroup morphism perm action.
From mathcomp Require Import ssralg countalg.
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 finset fingroup morphism perm action.
From mathcomp Require Import ssralg countalg.
The algebraic part of the algebraic hierarchy for finite types
This file clones the entire ssralg hierarchy for finite types; this
allows type inference to function properly on expressions that mix
combinatorial and algebraic operators, e.g., [set x + y | x in A, y in A].
finNmodType, finZmodType, finSemiRingType, finRingType, finComRingType,
finComSemiRingType, finUnitRingType, finComUnitRingType, finIdomType,
finFieldType, finLmodType, finLalgType, finAlgType, finUnitAlgType
== the finite counterparts of nmodType, etc
Note that a finFieldType is canonically decidable.
This file also provides direct tie-ins with finite group theory:
[finGroupMixin of R for +%R] == structures for R
{unit R} == the type of units of R, which has a
canonical group structure
FinRing.unit R Ux == the element of {unit R} corresponding
to x, where Ux : x \in GRing.unit
'U%act == the action by right multiplication of
{unit R} on R, via FinRing.unit_act
(This is also a group action.)
Local Open Scope ring_scope.
Set Implicit Arguments.
Module FinRing.
Import GRing.Theory.
#[short(type="finNmodType")]
HB.structure Definition Nmodule := {M of GRing.Nmodule M & Finite M}.
#[short(type="finZmodType")]
HB.structure Definition Zmodule := {M of GRing.Zmodule M & Finite M}.
Module ZmoduleExports.
Notation "[ 'finGroupMixin' 'of' R 'for' +%R ]" :=
(isMulGroup.Build R (@addrA _) (@add0r _) (@addNr _))
(at level 0, format "[ 'finGroupMixin' 'of' R 'for' +%R ]") : form_scope.
End ZmoduleExports.
#[short(type="finSemiRingType")]
HB.structure Definition SemiRing := {R of GRing.SemiRing R & Finite R}.
#[short(type="finRingType")]
HB.structure Definition Ring := {R of GRing.Ring R & Finite R}.
#[short(type="finComSemiRingType")]
HB.structure Definition ComSemiRing := {R of GRing.ComSemiRing R & Finite R}.
#[short(type="finComRingType")]
HB.structure Definition ComRing := {R of GRing.ComRing R & Finite R}.
#[short(type="finUnitRingType")]
HB.structure Definition UnitRing := {R of GRing.UnitRing R & Finite R}.
#[short(type="finComUnitRingType")]
HB.structure Definition ComUnitRing := {R of GRing.ComUnitRing R & Finite R}.
#[short(type="finIdomainType")]
HB.structure Definition IntegralDomain :=
{R of GRing.IntegralDomain R & Finite R}.
#[short