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.

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.)