The base hierarchy of algebraic structures NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. Reference: Francois Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau, Packaging mathematical structures, TPHOLs 2009 This file defines the following algebraic structures: nmodType == additive abelian monoid The HB class is called Nmodule. zmodType == additive abelian group (Nmodule with an opposite) The HB class is called Zmodule. pzSemiRingType == non-commutative semi rings (NModule with a multiplication) The HB class is called PzSemiRing. nzSemiRingType == non-commutative non-trivial semi rings (NModule with a multiplication) The HB class is called NzSemiRing. comPzSemiRingType == commutative semi rings The HB class is called ComPzSemiRing. comNzSemiRingType == commutative non-trivial semi rings The HB class is called ComNzSemiRing. pzRingType == non-commutative rings (semi rings with an opposite) The HB class is called PzRing. nzRingType == non-commutative non-trivial rings (semi rings with an opposite) The HB class is called NzRing. comPzRingType == commutative rings The HB class is called ComPzRing. comNzRingType == commutative non-trivial rings The HB class is called ComNzRing. lSemiModType R == semimodule with left multiplication by external scalars in the semiring R The HB class is called LSemiModule. lmodType R == module with left multiplication by external scalars in the pzRing R The HB class is called Lmodule. lSemiAlgType R == left semialgebra, semiring with scaling that associates on the left The HB class is called LSemiAlgebra. lalgType R == left algebra, ring with scaling that associates on the left The HB class is called Lalgebra. semiAlgType R == semialgebra, semiring with scaling that associates both left and right The HB class is called SemiAlgebra. algType R == algebra, ring with scaling that associates both left and right The HB class is called Algebra. comSemiAlgType R == commutative semiAlgType The HB class is called ComSemiAlgebra. comAlgType R == commutative algType The HB class is called ComAlgebra. unitRingType == Rings whose units have computable inverses The HB class is called UnitRing. comUnitRingType == commutative UnitRing The HB class is called ComUnitRing. unitAlgType R == algebra with computable inverses The HB class is called UnitAlgebra. comUnitAlgType R == commutative UnitAlgebra The HB class is called ComUnitAlgebra. idomainType == integral, commutative, ring with partial inverses The HB class is called IntegralDomain. fieldType == commutative fields The HB class is called Field. decFieldType == fields with a decidable first order theory The HB class is called DecidableField. closedFieldType == algebraically closed fields The HB class is called ClosedField. and their joins with subType: subNmodType V P == join of nmodType and subType (P : pred V) such that val is semi_additive The HB class is called SubNmodule. subZmodType V P == join of zmodType and subType (P : pred V) such that val is additive The HB class is called SubZmodule. subPzSemiRingType R P == join of pzSemiRingType and subType (P : pred R) such that val is a semiring morphism The HB class is called SubPzSemiRing. subNzSemiRingType R P == join of nzSemiRingType and subType (P : pred R) such that val is a semiring morphism The HB class is called SubNzSemiRing. subComPzSemiRingType R P == join of comPzSemiRingType and subType (P : pred R) such that val is a morphism The HB class is called SubComPzSemiRing. subComNzSemiRingType R P == join of comNzSemiRingType and subType (P : pred R) such that val is a morphism The HB class is called SubComNzSemiRing. subPzRingType R P == join of pzRingType and subType (P : pred R) such that val is a morphism The HB class is called SubPzRing. subComPzRingType R P == join of comPzRingType and subType (P : pred R) such that val is a morphism The HB class is called SubComPzRing. subNzRingType R P == join of nzRingType and subType (P : pred R) such that val is a morphism The HB class is called SubNzRing. subComNzRingType R P == join of comNzRingType and subType (P : pred R) such that val is a morphism The HB class is called SubComNzRing. subLSemiModType R V P == join of lSemiModType and subType (P : pred V) such that val is scalable The HB class is called SubLSemiModule. subLmodType R V P == join of lmodType and subType (P : pred V) such that val is scalable The HB class is called SubLmodule. subLSemiAlgType R V P == join of lSemiAlgType and subType (P : pred V) such that val is linear The HB class is called SubLSemiAlgebra. subLalgType R V P == join of lalgType and subType (P : pred V) such that val is linear The HB class is called SubLalgebra. subSemiAlgType R V P == join of semiAlgType and subType (P : pred V) such that val is linear The HB class is called SubSemiAlgebra. subAlgType R V P == join of algType and subType (P : pred V) such that val is linear The HB class is called SubAlgebra. subUnitRingType R P == join of unitRingType and subType (P : pred R) such that val is a ring morphism The HB class is called SubUnitRing. subComUnitRingType R P == join of comUnitRingType and subType (P : pred R) such that val is a ring morphism The HB class is called SubComUnitRing. subIdomainType R P == join of idomainType and subType (P : pred R) such that val is a ring morphism The HB class is called SubIntegralDomain. subField R P == join of fieldType and subType (P : pred R) such that val is a ring morphism The HB class is called SubField. Morphisms between the above structures (see below for details): {additive U -> V} == semi additive (resp. additive) functions between nmodType (resp. zmodType) instances U and V. The HB class is called Additive. {rmorphism R -> S} == semi ring (resp. ring) morphism between semiPzRingType (resp. pzRingType) instances R and S. The HB class is called RMorphism. {linear U -> V | s} == semilinear (resp. linear) functions of type U -> V, where U is a left semimodule (resp. left module) over semiring (resp. ring) R, V is an N-module (resp. Z-module), and s is a scaling operator (detailed below) of type R -> V -> V. The HB class is called Linear. {lrmorphism A -> B | s} == semialgebra (resp. algebra) morphisms of type A -> B, where A is a left semialgebra (resp. left algebra) over semiring (resp. ring) R, B is an semiring (resp. ring), and s is a scaling operator (detailed below) of type R -> B -> B. The HB class is called LRMorphism.

• > The scaling operator s above should be one of *:%R, *%R, or a combination nu \; *:%R or nu \; *%R with a semiring morphism nu; otherwise some of the theory (e.g., the linearZ rule) will not apply. To enable the overloading of the scaling operator, we use the following structures: GRing.Scale.preLaw R V == scaling morphisms of type R -> V -> V The HB class is called Scale.PreLaw.

GRing.Scale.semiLaw R V == scaling morphisms of type R -> V -> V The HB class is called Scale.SemiLaw. GRing.Scale.law R V == scaling morphisms of type R -> V -> V The HB class is called Scale.Law. Closedness predicates for the algebraic structures: addrClosed V == predicate closed under addition on V : nmodType The HB class is called AddClosed. opprClosed V == predicate closed under opposite on V : zmodType The HB class is called OppClosed. zmodClosed V == predicate closed under opposite and addition on V The HB class is called ZmodClosed. mulr2Closed R == predicate closed under multiplication on R : semiPzRingType The HB class is called Mul2Closed. mulrClosed R == predicate closed under multiplication and for 1 The HB class is called MulClosed. semiring2Closed R == predicate closed under addition and multiplication The HB class is called Semiring2Closed. semiringClosed R == predicate closed under semiring operations The HB class is called SemiringClosed. smulClosed R == predicate closed under multiplication and for -1 The HB class is called SmulClosed. subringClosed R == predicate closed under ring operations The HB class is called SubringClosed. divClosed R == predicate closed under division The HB class is called DivClosed. sdivClosed R == predicate closed under division and opposite The HB class is called SdivClosed. submodClosed R == predicate closed under lSemiModType operations The HB class is called SubmodClosed. subalgClosed R == predicate closed under lSemiAlgType operations The HB class is called SubalgClosed. divringClosed R == predicate closed under unitRing operations The HB class is called DivringClosed. divalgClosed R S == predicate closed under (S : unitAlg R) operations The HB class is called DivalgClosed. The rpred* lemmas ensure that the set S remains stable under the specified operations, provided the corresponding closedness predicate is satisfied. This stability is crucial for constructing and reasoning about substructures within algebraic hierarchies. For example:

• rpred0: Concludes 0 \in S if S is addrClosed.
• rpredD: Concludes x + y \in S if x \in S and y \in S and S is addrClosed.
• rpredN: Concludes -x \in S if x \in S and S is opprClosed.
• rpredZ: Concludes a *: v \in S if v \in S and S is scalerClosed.

Canonical properties of the algebraic structures:

Nmodule (additive abelian monoids):

0 == the zero (additive identity) of a Nmodule x + y == the sum of x and y (in a Nmodule) x *+ n == n times x, with n in nat (non-negative), i.e., x + (x + .. (x + x)..) (n terms); x *+ 1 is thus convertible to x, and x *+ 2 to x + x \sum_<range> e == iterated sum for a Nmodule (cf bigop.v) e`_i == nth 0 e i, when e : seq M and M has a nmodType structure support f == 0.-support f, i.e., [pred x | f x != 0] addr_closed S <-> collective predicate S is closed under finite sums (0 and x + y in S, for x, y in S) [SubChoice_isSubNmodule of U by <: ] == nmodType mixin for a subType whose base type is a nmodType and whose predicate's is an addrClosed

Zmodule (additive abelian groups):

• x == the opposite (additive inverse) of x

x - y == the difference of x and y; this is only notation for x + (- y) x *- n == notation for - (x *+ n), the opposite of x *+ n oppr_closed S <-> collective predicate S is closed under opposite zmod_closed S <-> collective predicate S is closed under zmodType operations (0 and x - y in S, for x, y in S) This property coerces to oppr_pred and addr_pred. [SubChoice_isSubZmodule of U by <: ] == zmodType mixin for a subType whose base type is a zmodType and whose predicate's is a zmodClosed

PzSemiRing (non-commutative semirings):

R^c == the converse (semi)ring for R: R^c is convertible to R but when R has a canonical (semi)ring structure R^c has the converse one: if x y : R^c, then x * y = (y : R) * (x : R) 1 == the multiplicative identity element of a semiring n%:R == the semiring image of an n in nat; this is just notation for 1 *+ n, so 1%:R is convertible to 1 and 2%:R to 1 + 1 <number> == <number>%:R with <number> a sequence of digits x * y == the semiring product of x and y \prod_<range> e == iterated product for a semiring (cf bigop.v) x ^+ n == x to the nth power with n in nat (non-negative), i.e., x * (x * .. (x * x)..) (n factors); x ^+ 1 is thus convertible to x, and x ^+ 2 to x * x GRing.comm x y <-> x and y commute, i.e., x * y = y * x GRing.lreg x <-> x if left-regular, i.e., *%R x is injective GRing.rreg x <-> x if right-regular, i.e., *%R^~ x is injective [pchar R] == the characteristic of R, defined as the set of prime numbers p such that p%:R = 0 in R The set [pchar R] has at most one element, and is implemented as a pred_nat collective predicate (see prime.v); thus the statement p \in [pchar R] can be read as `R has characteristic p', while [pchar R] =i pred0 means `R has characteristic 0' when R is a field. pFrobenius_aut chRp == the Frobenius automorphism mapping x in R to x ^+ p, where chRp : p \in [pchar R] is a proof that R has (non-zero) characteristic p mulr_closed S <-> collective predicate S is closed under finite products (1 and x * y in S for x, y in S) semiring_closed S <-> collective predicate S is closed under semiring operations (0, 1, x + y and x * y in S) [SubNmodule_isSubPzSemiRing of R by <: ] == [SubChoice_isSubPzSemiRing of R by <: ] == semiPzRingType mixin for a subType whose base type is a pzSemiRingType and whose predicate's is a semiringClosed

NzSemiRing (non-commutative non-trivial semirings):

[SubNmodule_isSubNzSemiRing of R by <: ] == [SubChoice_isSubNzSemiRing of R by <: ] == semiNzRingType mixin for a subType whose base type is a nzSemiRingType and whose predicate's is a semiringClosed

PzRing (non-commutative rings):

GRing.sign R b := (-1) ^+ b in R : pzRingType, with b : bool This is a parsing-only helper notation, to be used for defining more specific instances. smulr_closed S <-> collective predicate S is closed under products and opposite (-1 and x * y in S for x, y in S) subring_closed S <-> collective predicate S is closed under ring operations (1, x - y and x * y in S) [SubZmodule_isSubPzRing of R by <: ] == [SubChoice_isSubPzRing of R by <: ] == pzRingType mixin for a subType whose base type is a pzRingType and whose predicate's is a subringClosed

NzRing (non-commutative non-trivial rings):

[SubZmodule_isSubNzRing of R by <: ] == [SubChoice_isSubNzRing of R by <: ] == nzRingType mixin for a subType whose base type is a nzRingType and whose predicate's is a subringClosed

ComPzSemiRing (commutative PzSemiRings):

[SubNmodule_isSubComPzSemiRing of R by <: ] == [SubChoice_isSubComPzSemiRing of R by <: ] == comPzSemiRingType mixin for a subType whose base type is a comPzSemiRingType and whose predicate's is a semiringClosed

ComNzSemiRing (commutative NzSemiRings):

[SubNmodule_isSubComNzSemiRing of R by <: ] == [SubChoice_isSubComNzSemiRing of R by <: ] == comNzSemiRingType mixin for a subType whose base type is a comNzSemiRingType and whose predicate's is a semiringClosed

ComPzRing (commutative PzRings):

[SubZmodule_isSubComPzRing of R by <: ] == [SubChoice_isSubComPzRing of R by <: ] == comPzRingType mixin for a subType whose base type is a comPzRingType and whose predicate's is a subringClosed

ComNzRing (commutative NzRings):

[SubZmodule_isSubComNzRing of R by <: ] == [SubChoice_isSubComNzRing of R by <: ] == comNzRingType mixin for a subType whose base type is a comNzRingType and whose predicate's is a subringClosed

UnitRing (NzRings whose units have computable inverses):

x \is a GRing.unit <=> x is a unit (i.e., has an inverse) x^-1 == the ring inverse of x, if x is a unit, else x x / y == x divided by y (notation for x * y^-1) x ^- n := notation for (x ^+ n)^-1, the inverse of x ^+ n invr_closed S <-> collective predicate S is closed under inverse divr_closed S <-> collective predicate S is closed under division (1 and x / y in S) sdivr_closed S <-> collective predicate S is closed under division and opposite (-1 and x / y in S, for x, y in S) divring_closed S <-> collective predicate S is closed under unitRing operations (1, x - y and x / y in S) [SubNzRing_isSubUnitRing of R by <: ] == [SubChoice_isSubUnitRing of R by <: ] == unitRingType mixin for a subType whose base type is a unitRingType and whose predicate's is a divringClosed and whose ring structure is compatible with the base type's

ComUnitRing (commutative rings with computable inverses):

[SubChoice_isSubComUnitRing of R by <: ] == comUnitRingType mixin for a subType whose base type is a comUnitRingType and whose predicate's is a divringClosed and whose ring structure is compatible with the base type's

IntegralDomain (integral, commutative, ring with partial inverses):

[SubComUnitRing_isSubIntegralDomain R by <: ] == [SubChoice_isSubIntegralDomain R by <: ] == mixin axiom for a idomain subType

Field (commutative fields):

GRing.Field.axiom inv == field axiom: x != 0 -> inv x * x = 1 for all x This is equivalent to the property above, but does not require a unitRingType as inv is an explicit argument. [SubIntegralDomain_isSubField of R by <: ] == mixin axiom for a field subType

DecidableField (fields with a decidable first order theory):

GRing.term R == the type of formal expressions in a unit ring R with formal variables 'X_k, k : nat, and manifest constants x%:T, x : R The notation of all the ring operations is redefined for terms, in scope %T. GRing.formula R == the type of first order formulas over R; the %T scope binds the logical connectives /\, \/, ~, ==>, ==, and != to formulae; GRing.True/False and GRing.Bool b denote constant formulae, and quantifiers are written 'forall/'exists 'X_k, f GRing.Unit x tests for ring units GRing.If p_f t_f e_f emulates if-then-else GRing.Pick p_f t_f e_f emulates fintype.pick foldr GRing.Exists/Forall q_f xs can be used to write iterated quantifiers GRing.eval e t == the value of term t with valuation e : seq R (e maps 'X_i to e`_i) GRing.same_env e1 e2 <-> environments e1 and e2 are extensionally equal GRing.qf_form f == f is quantifier-free GRing.holds e f == the intuitionistic CiC interpretation of the formula f holds with valuation e GRing.qf_eval e f == the value (in bool) of a quantifier-free f GRing.sat e f == valuation e satisfies f (only in a decField) GRing.sol n f == a sequence e of size n such that e satisfies f, if one exists, or [:: ] if there is no such e 'exists 'X_i, u1 == 0 /\ ... /\ u_m == 0 /\ v1 != 0 ... /\ v_n != 0

LSemiModule (semimodule with left multiplication by external scalars).

a *: v == v scaled by a, when v is in an LSemiModule V and a is in the scalar semiring of V scaler_closed S <-> collective predicate S is closed under scaling subsemimod_closed S <-> collective predicate S is closed under lSemiModType operations (0, +%R, and *:%R) [SubNmodule_isSubLSemiModule of V by <: ] == [SubChoice_isSubLSemiModule of V by <: ] == mixin axiom for a subType of an lSemiModType

Lmodule (module with left multiplication by external scalars).

linear_closed S <-> collective predicate S is closed under linear combinations (a *: u + v in S when u, v in S) submod_closed S <-> collective predicate S is closed under lmodType operations (0 and a *: u + v in S) [SubZmodule_isSubLmodule of V by <: ] == [SubChoice_isSubLmodule of V by <: ] == mixin axiom for a subType of an lmodType

LSemiAlgebra

(left semialgebra, semiring with scaling that associates on the left): R^o == the regular (semi)algebra of R: R^o is convertible to R, but when R has a nz(Semi)RingType structure then R^o extends it to an l(Semi)AlgType structure by letting R act on itself: if x : R and y : R^o then x *: y = x * (y : R) k%:A == the image of the scalar k in a left semialgebra; this is simply notation for k *: 1 [SubSemiRing_SubLSemiModule_isSubLSemiAlgebra of V by <: ] == mixin axiom for a subType of an lSemiAlgType

Lalgebra (left algebra, ring with scaling that associates on the left):

subalg_closed S <-> collective predicate S is closed under lalgType operations (1, a *: u + v and u * v in S) [SubNzRing_SubLmodule_isSubLalgebra of V by <: ] == [SubChoice_isSubLalgebra of V by <: ] == mixin axiom for a subType of an lalgType

SemiAlgebra (semiring with scaling that associates both left and right):

[SubLSemiAlgebra_isSubSemiAlgebra of V by <: ] == == mixin axiom for a subType of an semiAlgType

Algebra (ring with scaling that associates both left and right):

[SubLalgebra_isSubAlgebra of V by <: ] == [SubChoice_isSubAlgebra of V by <: ] == mixin axiom for a subType of an algType

UnitAlgebra (algebra with computable inverses):

divalg_closed S <-> collective predicate S is closed under all unitAlgType operations (1, a *: u + v and u / v are in S fo u, v in S) In addition to this structure hierarchy, we also develop a separate, parallel hierarchy for morphisms linking these structures:

Additive (semiadditive or additive functions):

semi_additive f <-> f of type U -> V is semiadditive, i.e., f maps the Nmodule structure of U to that of V, 0 to 0 and + to + := (f 0 = 0) * {morph f : x y / x + y} additive f <-> f of type U -> V is additive, i.e., f maps the Zmodule structure of U to that of V, 0 to 0,

• to - and + to + (equivalently, binary - to -)

:= {morph f : u v / u - v} {additive U -> V} == the interface type for a Structure (keyed on a function f : U -> V) that encapsulates the semi_additive property; both U and V must have canonical nmodType instances When both U and V have zmodType instances, it is an additive function. := GRing.Additive.type U V

RMorphism (semiring or ring morphisms):

multiplicative f <-> f of type R -> S is multiplicative, i.e., f maps 1 and * in R to 1 and * in S, respectively R and S must have canonical pzSemiRingType instances {rmorphism R -> S} == the interface type for semiring morphisms; both R and S must have pzSemiRingType instances When both R and S have pzRingType instances, it is a ring morphism. := GRing.RMorphism.type R S

• > If R and S are UnitRings the f also maps units to units and inverses of units to inverses; if R is a field then f is a field isomorphism between R and its image.
• > Additive properties (raddf_suffix, see below) are duplicated and specialised for RMorphism (as rmorph_suffix). This allows more precise rewriting and cleaner chaining: although raddf lemmas will recognize RMorphism functions, the converse will not hold (we cannot add reverse inheritance rules because of incomplete backtracking in the Canonical Projection unification), so one would have to insert a /= every time one switched from additive to multiplicative rules.

Linear (semilinear or linear functions):

scalable_for s f <-> f of type U -> V is scalable for the scaling operator s of type R -> V -> V, i.e., f morphs a *: _ to s a _; R, U, and V must be a pzSemiRingType, an lSemiModType R, and an nmodType, respectively. := forall a, {morph f : u / a *: u >-> s a u} scalable f <-> f of type U -> V is scalable, i.e., f morphs scaling on U to scaling on V, a *: _ to a *: _; U and V must be lSemiModType R for the same pzSemiRingType R. := scalable_for *:%R f semilinear_for s f <-> f of type U -> V is semilinear for s of type R -> V -> V , i.e., f morphs a *: _ and addition on U to s a _ and addition on V, respectively; R, U, and V must be a pzSemiRingType, an lSemiModType R and an nmodType, respectively. := scalable_for s f * {morph f : x y / x + y} semilinear f <-> f of type U -> V is semilinear, i.e., f morphs scaling and addition on U to scaling and addition on V, respectively; U and V must be lSemiModType R for the same pzSemiRingType R. := semilinear_for *:% f semiscalar f <-> f of type U -> R is a semiscalar function, i.e., f morphs scaling and addition on U to multiplication and addition on R; R and U must be a pzSemiRingType and an lSemiModType R, respectively. := semilinear_for *%R f linear_for s f <-> f of type U -> V is linear for s of type R -> V -> V, i.e., f (a *: u + v) = s a (f u) + f v; R, U, and V must be a pzRingType, an lmodType R, and a zmodType, respectively. linear f <-> f of type U -> V is linear, i.e., f (f *: u + v) = a *: f u + f v; U and V must be lmodType R for the same pzRingType R. := linear_for *:%R f scalar f <-> f of type U -> R is a scalar function, i.e., f (a *: u + v) = a * f u + f v; R and U must be a pzRingType and an lmodType R, respectively. := linear_for *%R f {linear U -> V | s} == the interface type for functions (semi)linear for the scaling operator s of type R -> V -> V, i.e., a structure that encapsulates two properties semi_additive f and scalable_for s f for functions f : U -> V; R, U, and V must be a pzSemiRingType, an lSemiModType R, and an nmodType, respectively. {linear U -> V} == the interface type for (semi)linear functions, of type U -> V where both U and V must be lSemiModType R for the same pzSemiRingType R := {linear U -> V | *:%R} {scalar U} == the interface type for (semi)scalar functions, of type U -> R where U must be an lSemiModType R := {linear U -> R | *%R} (a *: u)%Rlin == transient forms that simplify to a *: u, a * u, (a * u)%Rlin nu a *: u, and nu a * u, respectively, and are (a *:^nu u)%Rlin created by rewriting with the linearZ lemma (a *^nu u)%Rlin The forms allows the RHS of linearZ to be matched reliably, using the GRing.Scale.law structure.

• > Similarly to semiring morphisms, semiadditive properties are specialized for semilinear functions.
• > Although {scalar U} is convertible to {linear U -> R^o}, it does not actually use R^o, so that rewriting preserves the canonical structure of the range of scalar functions.
• > The generic linearZ lemma uses a set of bespoke interface structures to ensure that both left-to-right and right-to-left rewriting work even in the presence of scaling functions that simplify non-trivially (e.g., idfun \; *%R). Because most of the canonical instances and projections are coercions the machinery will be mostly invisible (with only the {linear ...} structure and %Rlin notations showing), but users should beware that in (a *: f u)%Rlin, a actually occurs in the f u subterm.
• > The simpler linear_LR, or more specialized linearZZ and scalarZ rules should be used instead of linearZ if there are complexity issues, as well as for explicit forward and backward application, as the main parameter of linearZ is a proper sub-interface of {linear U -> V | s}.

LRMorphism (semialgebra or algebra morphisms):

{lrmorphism A -> B | s} == the interface type for semiring (resp. ring) morphisms semilinear (resp. linear) for the scaling operator s of type R -> B -> B, i.e., the join of semiring (resp. ring) morphisms {rmorphism A -> B} and semilinear (resp. linear) functions {linear A -> B | s}; R, A, and B must be a pzSemiRingType (resp. pzRingType), an lSemiAlgType R (resp. lalgType R), and a pzSemiRingType (resp. pzRingType), respectively {lrmorphism A -> B} == the interface type for semialgebra (resp. algebra) morphisms, where A and B must be lSemiAlgType R (resp. lalgType R) for the same pzSemiRingType (resp. pzRingType) R := {lrmorphism A -> B | *:%R}

• > Linear and rmorphism properties do not need to be specialized for as we supply inheritance join instances in both directions.

Finally we supply some helper notation for morphisms: x^f == the image of x under some morphism This notation is only reserved (not defined) here; it is bound locally in sections where some morphism is used heavily (e.g., the container morphism in the parametricity sections of poly and matrix, or the Frobenius section here) \0 == the constant null function, which has a canonical linear structure, and simplifies on application (see ssrfun.v) f \+ g == the additive composition of f and g, i.e., the function x |-> f x + g x; f \+ g is canonically linear when f and g are, and simplifies on application (see ssrfun.v) f \- g == the function x |-> f x - g x, canonically linear when f and g are, and simplifies on application \- g == the function x |-> - f x, canonically linear when f is, and simplifies on application k \*: f == the function x |-> k *: f x, which is canonically linear when f is and simplifies on application (this is a shorter alternative to *:%R k \o f) GRing.in_alg A == the ring morphism that injects R into A, where A has an lalgType R structure; GRing.in_alg A k simplifies to k%:A a \*o f == the function x |-> a * f x, canonically linear when f is and its codomain is an algType and which simplifies on application a \o* f == the function x |-> f x * a, canonically linear when f is and its codomain is an lalgType and which simplifies on application f \* g == the function x |-> f x * g x; f \* g simplifies on application The Lemmas about these structures are contained in both the GRing module and in the submodule GRing.Theory, which can be imported when unqualified access to the theory is needed (GRing.Theory also allows the unqualified use of additive, linear, Linear, etc). The main GRing module should NOT be imported. Notations are defined in scope ring_scope (delimiter %R), except term and formula notations, which are in term_scope (delimiter %T). This library also extends the conventional suffixes described in library ssrbool.v with the following: 0 -- ring 0, as in addr0 : x + 0 = x 1 -- ring 1, as in mulr1 : x * 1 = x D -- ring addition, as in linearD : f (u + v) = f u + f v B -- ring subtraction, as in opprB : - (x - y) = y - x M -- ring multiplication, as in invfM : (x * y)^-1 = x^-1 * y^-1 Mn -- ring by nat multiplication, as in raddfMn : f (x *+ n) = f x *+ n N -- ring opposite, as in mulNr : (- x) * y = - (x * y) V -- ring inverse, as in mulVr : x^-1 * x = 1 X -- ring exponentiation, as in rmorphXn : f (x ^+ n) = f x ^+ n Z -- (left) module scaling, as in linearZ : f (a *: v) = s *: f v The operator suffixes D, B, M and X are also used for the corresponding operations on nat, as in natrX : (m ^ n)%:R = m%:R ^+ n. For the binary power operator, a trailing "n" suffix is used to indicate the operator suffix applies to the left-hand ring argument, as in expr1n : 1 ^+ n = 1 vs. expr1 : x ^+ 1 = x.

Patch for recurring Coq parser bug: Coq seg faults when a level 200 notation is used as a pattern.

The ``field'' characteristic; the definition, and many of the theorems, has to apply to rings as well; indeed, we need the Frobenius automorphism results for a non commutative ring in the proof of Gorenstein 2.6.3.

Converse ring tag.