From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.algebra.ring_quotient.html | 328 +++++++++++------------ 1 file changed, 163 insertions(+), 165 deletions(-) (limited to 'docs/htmldoc/mathcomp.algebra.ring_quotient.html') diff --git a/docs/htmldoc/mathcomp.algebra.ring_quotient.html b/docs/htmldoc/mathcomp.algebra.ring_quotient.html index 35d7bc6..0e42147 100644 --- a/docs/htmldoc/mathcomp.algebra.ring_quotient.html +++ b/docs/htmldoc/mathcomp.algebra.ring_quotient.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -67,9 +66,9 @@ unitRingQuotType ... u i == As in the previous cases, instance of unit ring whose unit predicate is obtained from u and the inverse from i. - idealr R S == (S : pred R) is a non-trivial, decidable, + idealr R S == S : {pred R} is a non-trivial, decidable, right ideal of the ring R. - prime_idealr R S == (S : pred R) is a non-trivial, decidable, + prime_idealr R S == S : {pred R} is a non-trivial, decidable, right, prime ideal of the ring R.
@@ -85,22 +84,21 @@
- MkIdeal idealS == packs idealS : proper_ideal S into an - idealr S interface structure associating the + MkIdeal idealS == packs idealS : proper_ideal S into an idealr S + interface structure associating the idealr_closed property to the canonical pred_key S (see ssrbool), which must already - be an zmodPred (see ssralg). + be a zmodPred (see ssralg). MkPrimeIdeal pidealS == packs pidealS : prime_idealr_closed S into a prime_idealr S interface structure associating the prime_idealr_closed property to the canonical pred_key S (see ssrbool), which must already be an idealr (see above). {ideal_quot kI} == quotient by the keyed (right) ideal predicate - kI of a commutative ring R. Note that we indeed - only provide canonical structures of ring - quotients for the case of commutative rings, - for which a right ideal is obviously a - two-sided ideal. + kI of a commutative ring R. Note that we only + provide canonical structures of ring quotients + for commutative rings, in which a right ideal + is obviously a two-sided ideal.
@@ -138,18 +136,18 @@
Variable (T : Type).
-Variable eqT : rel T.
-Variables (zeroT : T) (oppT : T → T) (addT : T → T → T).
+Variable eqT : rel T.
+Variables (zeroT : T) (oppT : T → T) (addT : T → T → T).

Record zmod_quot_mixin_of (Q : Type) (qc : quot_class_of T Q)
  (zc : GRing.Zmodule.class_of Q) := ZmodQuotMixinPack {
    zmod_eq_quot_mixin :> eq_quot_mixin_of eqT qc zc;
-    _ : \pi_(QuotTypePack qc Q) zeroT = 0 :> GRing.Zmodule.Pack zc Q;
-    _ : {morph \pi_(QuotTypePack qc Q) : x /
-         oppT x >-> @GRing.opp (GRing.Zmodule.Pack zc Q) x};
-    _ : {morph \pi_(QuotTypePack qc Q) : x y /
-         addT x y >-> @GRing.add (GRing.Zmodule.Pack zc Q) x y}
+    _ : \pi_(QuotTypePack qc) zeroT = 0 :> GRing.Zmodule.Pack zc;
+    _ : {morph \pi_(QuotTypePack qc) : x /
+         oppT x >-> @GRing.opp (GRing.Zmodule.Pack zc) x};
+    _ : {morph \pi_(QuotTypePack qc) : x y /
+         addT x y >-> @GRing.add (GRing.Zmodule.Pack zc) x y}
}.

@@ -164,7 +162,7 @@ Structure zmodQuotType : Type := ZmodQuotTypePack {
  zmod_quot_sort :> Type;
  _ : zmod_quot_class_of zmod_quot_sort;
-  _ : Type
+ 
}.

@@ -172,21 +170,21 @@
Definition zmod_quot_class zqT : zmod_quot_class_of zqT :=
-  let: ZmodQuotTypePack _ cT _ as qT' := zqT return zmod_quot_class_of qT' in cT.
+  let: ZmodQuotTypePack _ cT as qT' := zqT return zmod_quot_class_of qT' in cT.

Definition zmod_eq_quot_class zqT (zqc : zmod_quot_class_of zqT) :
  eq_quot_class_of eqT zqT := EqQuotClass zqc.

-Canonical zmodQuotType_eqType zqT := Equality.Pack (zmod_quot_class zqT) zqT.
+Canonical zmodQuotType_eqType zqT := Equality.Pack (zmod_quot_class zqT).
Canonical zmodQuotType_choiceType zqT :=
-  Choice.Pack (zmod_quot_class zqT) zqT.
+  Choice.Pack (zmod_quot_class zqT).
Canonical zmodQuotType_zmodType zqT :=
-  GRing.Zmodule.Pack (zmod_quot_class zqT) zqT.
-Canonical zmodQuotType_quotType zqT := QuotTypePack (zmod_quot_class zqT) zqT.
+  GRing.Zmodule.Pack (zmod_quot_class zqT).
+Canonical zmodQuotType_quotType zqT := QuotTypePack (zmod_quot_class zqT).
Canonical zmodQuotType_eqQuotType zqT := EqQuotTypePack
-  (zmod_eq_quot_class (zmod_quot_class zqT)) zqT.
+  (zmod_eq_quot_class (zmod_quot_class zqT)).

Coercion zmodQuotType_eqType : zmodQuotType >-> eqType.
@@ -198,32 +196,32 @@
Definition ZmodQuotType_pack Q :=
  fun (qT : quotType T) (zT : zmodType) qc zc
-  of phant_id (quot_class qT) qc & phant_id (GRing.Zmodule.class zT) zc ⇒
-    fun m ⇒ ZmodQuotTypePack (@ZmodQuotClass Q qc zc m) Q.
+  of phant_id (quot_class qT) qc & phant_id (GRing.Zmodule.class zT) zc ⇒
+    fun m ⇒ ZmodQuotTypePack (@ZmodQuotClass Q qc zc m).

Definition ZmodQuotMixin_pack Q :=
  fun (qT : eqQuotType eqT) (qc : eq_quot_class_of eqT Q)
-      of phant_id (eq_quot_class qT) qc ⇒
-  fun (zT : zmodType) zc of phant_id (GRing.Zmodule.class zT) zc ⇒
+      of phant_id (eq_quot_class qT) qc ⇒
+  fun (zT : zmodType) zc of phant_id (GRing.Zmodule.class zT) zc ⇒
    fun e m0 mN mD ⇒ @ZmodQuotMixinPack Q qc zc e m0 mN mD.

Definition ZmodQuotType_clone (Q : Type) qT cT
-  of phant_id (zmod_quot_class qT) cT := @ZmodQuotTypePack Q cT Q.
+  of phant_id (zmod_quot_class qT) cT := @ZmodQuotTypePack Q cT.

Lemma zmod_quot_mixinP zqT :
  zmod_quot_mixin_of (zmod_quot_class zqT) (zmod_quot_class zqT).

-Lemma pi_zeror zqT : \pi_zqT zeroT = 0.
+Lemma pi_zeror zqT : \pi_zqT zeroT = 0.

-Lemma pi_oppr zqT : {morph \pi_zqT : x / oppT x >-> - x}.
+Lemma pi_oppr zqT : {morph \pi_zqT : x / oppT x >-> - x}.

-Lemma pi_addr zqT : {morph \pi_zqT : x y / addT x y >-> x + y}.
+Lemma pi_addr zqT : {morph \pi_zqT : x y / addT x y >-> x + y}.

Canonical pi_zero_quot_morph zqT := PiMorph (pi_zeror zqT).
@@ -235,22 +233,22 @@
Notation ZmodQuotType z o a Q m :=
-  (@ZmodQuotType_pack _ _ z o a Q _ _ _ _ id id m).
-Notation "[ 'zmodQuotType' z , o & a 'of' Q ]" :=
-  (@ZmodQuotType_clone _ _ z o a Q _ _ id)
+  (@ZmodQuotType_pack _ _ z o a Q _ _ _ _ id id m).
+Notation "[ 'zmodQuotType' z , o & a 'of' Q ]" :=
+  (@ZmodQuotType_clone _ _ z o a Q _ _ id)
  (at level 0, format "[ 'zmodQuotType' z , o & a 'of' Q ]") : form_scope.
Notation ZmodQuotMixin Q m0 mN mD :=
-  (@ZmodQuotMixin_pack _ _ _ _ _ Q _ _ id _ _ id (pi_eq_quot _) m0 mN mD).
+  (@ZmodQuotMixin_pack _ _ _ _ _ Q _ _ id _ _ id (pi_eq_quot _) m0 mN mD).

Section PiAdditive.

-Variables (V : zmodType) (equivV : rel V) (zeroV : V).
-Variable Q : @zmodQuotType V equivV zeroV -%R +%R.
+Variables (V : zmodType) (equivV : rel V) (zeroV : V).
+Variable Q : @zmodQuotType V equivV zeroV -%R +%R.

-Lemma pi_is_additive : additive \pi_Q.
+Lemma pi_is_additive : additive \pi_Q.

Canonical pi_additive := Additive pi_is_additive.
@@ -263,17 +261,17 @@
Variable (T : Type).
-Variable eqT : rel T.
-Variables (zeroT : T) (oppT : T → T) (addT : T → T → T).
-Variables (oneT : T) (mulT : T → T → T).
+Variable eqT : rel T.
+Variables (zeroT : T) (oppT : T → T) (addT : T → T → T).
+Variables (oneT : T) (mulT : T → T → T).

Record ring_quot_mixin_of (Q : Type) (qc : quot_class_of T Q)
  (rc : GRing.Ring.class_of Q) := RingQuotMixinPack {
    ring_zmod_quot_mixin :> zmod_quot_mixin_of eqT zeroT oppT addT qc rc;
-    _ : \pi_(QuotTypePack qc Q) oneT = 1 :> GRing.Ring.Pack rc Q;
-    _ : {morph \pi_(QuotTypePack qc Q) : x y /
-         mulT x y >-> @GRing.mul (GRing.Ring.Pack rc Q) x y}
+    _ : \pi_(QuotTypePack qc) oneT = 1 :> GRing.Ring.Pack rc;
+    _ : {morph \pi_(QuotTypePack qc) : x y /
+         mulT x y >-> @GRing.mul (GRing.Ring.Pack rc) x y}
}.

@@ -288,7 +286,7 @@ Structure ringQuotType : Type := RingQuotTypePack {
  ring_quot_sort :> Type;
  _ : ring_quot_class_of ring_quot_sort;
-  _ : Type
+ 
}.

@@ -296,7 +294,7 @@
Definition ring_quot_class rqT : ring_quot_class_of rqT :=
-  let: RingQuotTypePack _ cT _ as qT' := rqT return ring_quot_class_of qT' in cT.
+  let: RingQuotTypePack _ cT as qT' := rqT return ring_quot_class_of qT' in cT.

Definition ring_zmod_quot_class rqT (rqc : ring_quot_class_of rqT) :
@@ -305,17 +303,17 @@   eq_quot_class_of eqT rqT := EqQuotClass rqc.

-Canonical ringQuotType_eqType rqT := Equality.Pack (ring_quot_class rqT) rqT.
-Canonical ringQuotType_choiceType rqT := Choice.Pack (ring_quot_class rqT) rqT.
+Canonical ringQuotType_eqType rqT := Equality.Pack (ring_quot_class rqT).
+Canonical ringQuotType_choiceType rqT := Choice.Pack (ring_quot_class rqT).
Canonical ringQuotType_zmodType rqT :=
-  GRing.Zmodule.Pack (ring_quot_class rqT) rqT.
+  GRing.Zmodule.Pack (ring_quot_class rqT).
Canonical ringQuotType_ringType rqT :=
-  GRing.Ring.Pack (ring_quot_class rqT) rqT.
-Canonical ringQuotType_quotType rqT := QuotTypePack (ring_quot_class rqT) rqT.
+  GRing.Ring.Pack (ring_quot_class rqT).
+Canonical ringQuotType_quotType rqT := QuotTypePack (ring_quot_class rqT).
Canonical ringQuotType_eqQuotType rqT :=
-  EqQuotTypePack (ring_eq_quot_class (ring_quot_class rqT)) rqT.
+  EqQuotTypePack (ring_eq_quot_class (ring_quot_class rqT)).
Canonical ringQuotType_zmodQuotType rqT :=
-  ZmodQuotTypePack (ring_zmod_quot_class (ring_quot_class rqT)) rqT.
+  ZmodQuotTypePack (ring_zmod_quot_class (ring_quot_class rqT)).

Coercion ringQuotType_eqType : ringQuotType >-> eqType.
@@ -329,30 +327,30 @@
Definition RingQuotType_pack Q :=
  fun (qT : quotType T) (zT : ringType) qc rc
-  of phant_id (quot_class qT) qc & phant_id (GRing.Ring.class zT) rc ⇒
-    fun m ⇒ RingQuotTypePack (@RingQuotClass Q qc rc m) Q.
+  of phant_id (quot_class qT) qc & phant_id (GRing.Ring.class zT) rc ⇒
+    fun m ⇒ RingQuotTypePack (@RingQuotClass Q qc rc m).

Definition RingQuotMixin_pack Q :=
  fun (qT : zmodQuotType eqT zeroT oppT addT) ⇒
  fun (qc : zmod_quot_class_of eqT zeroT oppT addT Q)
-      of phant_id (zmod_quot_class qT) qc ⇒
-  fun (rT : ringType) rc of phant_id (GRing.Ring.class rT) rc ⇒
+      of phant_id (zmod_quot_class qT) qc ⇒
+  fun (rT : ringType) rc of phant_id (GRing.Ring.class rT) rc ⇒
    fun mZ m1 mM ⇒ @RingQuotMixinPack Q qc rc mZ m1 mM.

Definition RingQuotType_clone (Q : Type) qT cT
-  of phant_id (ring_quot_class qT) cT := @RingQuotTypePack Q cT Q.
+  of phant_id (ring_quot_class qT) cT := @RingQuotTypePack Q cT.

Lemma ring_quot_mixinP rqT :
  ring_quot_mixin_of (ring_quot_class rqT) (ring_quot_class rqT).

-Lemma pi_oner rqT : \pi_rqT oneT = 1.
+Lemma pi_oner rqT : \pi_rqT oneT = 1.

-Lemma pi_mulr rqT : {morph \pi_rqT : x y / mulT x y >-> x × y}.
+Lemma pi_mulr rqT : {morph \pi_rqT : x y / mulT x y >-> x × y}.

Canonical pi_one_quot_morph rqT := PiMorph (pi_oner rqT).
@@ -363,24 +361,24 @@
Notation RingQuotType o mul Q mix :=
-  (@RingQuotType_pack _ _ _ _ _ o mul Q _ _ _ _ id id mix).
-Notation "[ 'ringQuotType' o & m 'of' Q ]" :=
-  (@RingQuotType_clone _ _ _ _ _ o m Q _ _ id)
+  (@RingQuotType_pack _ _ _ _ _ o mul Q _ _ _ _ id id mix).
+Notation "[ 'ringQuotType' o & m 'of' Q ]" :=
+  (@RingQuotType_clone _ _ _ _ _ o m Q _ _ id)
  (at level 0, format "[ 'ringQuotType' o & m 'of' Q ]") : form_scope.
Notation RingQuotMixin Q m1 mM :=
-  (@RingQuotMixin_pack _ _ _ _ _ _ _ Q _ _ id _ _ id (zmod_quot_mixinP _) m1 mM).
+  (@RingQuotMixin_pack _ _ _ _ _ _ _ Q _ _ id _ _ id (zmod_quot_mixinP _) m1 mM).

Section PiRMorphism.

-Variables (R : ringType) (equivR : rel R) (zeroR : R).
+Variables (R : ringType) (equivR : rel R) (zeroR : R).

-Variable Q : @ringQuotType R equivR zeroR -%R +%R 1 *%R.
+Variable Q : @ringQuotType R equivR zeroR -%R +%R 1 *%R.

-Lemma pi_is_multiplicative : multiplicative \pi_Q.
+Lemma pi_is_multiplicative : multiplicative \pi_Q.

Canonical pi_rmorphism := AddRMorphism pi_is_multiplicative.
@@ -393,20 +391,20 @@
Variable (T : Type).
-Variable eqT : rel T.
-Variables (zeroT : T) (oppT : T → T) (addT : T → T → T).
-Variables (oneT : T) (mulT : T → T → T).
-Variables (unitT : pred T) (invT : T → T).
+Variable eqT : rel T.
+Variables (zeroT : T) (oppT : T → T) (addT : T → T → T).
+Variables (oneT : T) (mulT : T → T → T).
+Variables (unitT : pred T) (invT : T → T).

Record unit_ring_quot_mixin_of (Q : Type) (qc : quot_class_of T Q)
  (rc : GRing.UnitRing.class_of Q) := UnitRingQuotMixinPack {
    unit_ring_zmod_quot_mixin :>
        ring_quot_mixin_of eqT zeroT oppT addT oneT mulT qc rc;
-    _ : {mono \pi_(QuotTypePack qc Q) : x /
-         unitT x >-> x \in @GRing.unit (GRing.UnitRing.Pack rc Q)};
-    _ : {morph \pi_(QuotTypePack qc Q) : x /
-         invT x >-> @GRing.inv (GRing.UnitRing.Pack rc Q) x}
+    _ : {mono \pi_(QuotTypePack qc) : x /
+         unitT x >-> x \in @GRing.unit (GRing.UnitRing.Pack rc)};
+    _ : {morph \pi_(QuotTypePack qc) : x /
+         invT x >-> @GRing.inv (GRing.UnitRing.Pack rc) x}
}.

@@ -421,7 +419,7 @@ Structure unitRingQuotType : Type := UnitRingQuotTypePack {
  unit_ring_quot_sort :> Type;
  _ : unit_ring_quot_class_of unit_ring_quot_sort;
-  _ : Type
+ 
}.

@@ -429,7 +427,7 @@
Definition unit_ring_quot_class rqT : unit_ring_quot_class_of rqT :=
-  let: UnitRingQuotTypePack _ cT _ as qT' := rqT
+  let: UnitRingQuotTypePack _ cT as qT' := rqT
    return unit_ring_quot_class_of qT' in cT.

@@ -442,23 +440,23 @@
Canonical unitRingQuotType_eqType rqT :=
-  Equality.Pack (unit_ring_quot_class rqT) rqT.
+  Equality.Pack (unit_ring_quot_class rqT).
Canonical unitRingQuotType_choiceType rqT :=
-  Choice.Pack (unit_ring_quot_class rqT) rqT.
+  Choice.Pack (unit_ring_quot_class rqT).
Canonical unitRingQuotType_zmodType rqT :=
-  GRing.Zmodule.Pack (unit_ring_quot_class rqT) rqT.
+  GRing.Zmodule.Pack (unit_ring_quot_class rqT).
Canonical unitRingQuotType_ringType rqT :=
-  GRing.Ring.Pack (unit_ring_quot_class rqT) rqT.
+  GRing.Ring.Pack (unit_ring_quot_class rqT).
Canonical unitRingQuotType_unitRingType rqT :=
-  GRing.UnitRing.Pack (unit_ring_quot_class rqT) rqT.
+  GRing.UnitRing.Pack (unit_ring_quot_class rqT).
Canonical unitRingQuotType_quotType rqT :=
-  QuotTypePack (unit_ring_quot_class rqT) rqT.
+  QuotTypePack (unit_ring_quot_class rqT).
Canonical unitRingQuotType_eqQuotType rqT :=
-  EqQuotTypePack (unit_ring_eq_quot_class (unit_ring_quot_class rqT)) rqT.
+  EqQuotTypePack (unit_ring_eq_quot_class (unit_ring_quot_class rqT)).
Canonical unitRingQuotType_zmodQuotType rqT :=
-  ZmodQuotTypePack (unit_ring_zmod_quot_class (unit_ring_quot_class rqT)) rqT.
+  ZmodQuotTypePack (unit_ring_zmod_quot_class (unit_ring_quot_class rqT)).
Canonical unitRingQuotType_ringQuotType rqT :=
-  RingQuotTypePack (unit_ring_ring_quot_class (unit_ring_quot_class rqT)) rqT.
+  RingQuotTypePack (unit_ring_ring_quot_class (unit_ring_quot_class rqT)).

Coercion unitRingQuotType_eqType : unitRingQuotType >-> eqType.
@@ -474,30 +472,30 @@
Definition UnitRingQuotType_pack Q :=
  fun (qT : quotType T) (rT : unitRingType) qc rc
-  of phant_id (quot_class qT) qc & phant_id (GRing.UnitRing.class rT) rc ⇒
-    fun m ⇒ UnitRingQuotTypePack (@UnitRingQuotClass Q qc rc m) Q.
+  of phant_id (quot_class qT) qc & phant_id (GRing.UnitRing.class rT) rc ⇒
+    fun m ⇒ UnitRingQuotTypePack (@UnitRingQuotClass Q qc rc m).

Definition UnitRingQuotMixin_pack Q :=
  fun (qT : ringQuotType eqT zeroT oppT addT oneT mulT) ⇒
  fun (qc : ring_quot_class_of eqT zeroT oppT addT oneT mulT Q)
-      of phant_id (zmod_quot_class qT) qc ⇒
-  fun (rT : unitRingType) rc of phant_id (GRing.UnitRing.class rT) rc ⇒
+      of phant_id (zmod_quot_class qT) qc ⇒
+  fun (rT : unitRingType) rc of phant_id (GRing.UnitRing.class rT) rc ⇒
    fun mR mU mV ⇒ @UnitRingQuotMixinPack Q qc rc mR mU mV.

Definition UnitRingQuotType_clone (Q : Type) qT cT
-  of phant_id (unit_ring_quot_class qT) cT := @UnitRingQuotTypePack Q cT Q.
+  of phant_id (unit_ring_quot_class qT) cT := @UnitRingQuotTypePack Q cT.

Lemma unit_ring_quot_mixinP rqT :
  unit_ring_quot_mixin_of (unit_ring_quot_class rqT) (unit_ring_quot_class rqT).

-Lemma pi_unitr rqT : {mono \pi_rqT : x / unitT x >-> x \in GRing.unit}.
+Lemma pi_unitr rqT : {mono \pi_rqT : x / unitT x >-> x \in GRing.unit}.

-Lemma pi_invr rqT : {morph \pi_rqT : x / invT x >-> x^-1}.
+Lemma pi_invr rqT : {morph \pi_rqT : x / invT x >-> x^-1}.

Canonical pi_unit_quot_morph rqT := PiMono1 (pi_unitr rqT).
@@ -508,68 +506,68 @@
Notation UnitRingQuotType u i Q mix :=
-  (@UnitRingQuotType_pack _ _ _ _ _ _ _ u i Q _ _ _ _ id id mix).
-Notation "[ 'unitRingQuotType' u & i 'of' Q ]" :=
-  (@UnitRingQuotType_clone _ _ _ _ _ _ _ u i Q _ _ id)
+  (@UnitRingQuotType_pack _ _ _ _ _ _ _ u i Q _ _ _ _ id id mix).
+Notation "[ 'unitRingQuotType' u & i 'of' Q ]" :=
+  (@UnitRingQuotType_clone _ _ _ _ _ _ _ u i Q _ _ id)
  (at level 0, format "[ 'unitRingQuotType' u & i 'of' Q ]") : form_scope.
Notation UnitRingQuotMixin Q mU mV :=
  (@UnitRingQuotMixin_pack _ _ _ _ _ _ _ _ _ Q
-    _ _ id _ _ id (zmod_quot_mixinP _) mU mV).
+    _ _ id _ _ id (zmod_quot_mixinP _) mU mV).

Section IdealDef.

-Definition proper_ideal (R : ringType) (S : predPredType R) : Prop :=
-  1 \notin S ∧ ∀ a, {in S, ∀ u, a × u \in S}.
+Definition proper_ideal (R : ringType) (S : {pred R}) : Prop :=
+  1 \notin S ∧ ∀ a, {in S, ∀ u, a × u \in S}.

-Definition prime_idealr_closed (R : ringType) (S : predPredType R) : Prop :=
-  ∀ u v, u × v \in S → (u \in S) || (v \in S).
+Definition prime_idealr_closed (R : ringType) (S : {pred R}) : Prop :=
+  ∀ u v, u × v \in S → (u \in S) || (v \in S).

-Definition idealr_closed (R : ringType) (S : predPredType R) :=
-  [/\ 0 \in S, 1 \notin S & ∀ a, {in S &, ∀ u v, a × u + v \in S}].
+Definition idealr_closed (R : ringType) (S : {pred R}) :=
+  [/\ 0 \in S, 1 \notin S & ∀ a, {in S &, ∀ u v, a × u + v \in S}].

-Lemma idealr_closed_nontrivial R S : @idealr_closed R S → proper_ideal S.
+Lemma idealr_closed_nontrivial R S : @idealr_closed R S → proper_ideal S.

-Lemma idealr_closedB R S : @idealr_closed R S → zmod_closed S.
+Lemma idealr_closedB R S : @idealr_closed R S → zmod_closed S.

Coercion idealr_closedB : idealr_closed >-> zmod_closed.
Coercion idealr_closed_nontrivial : idealr_closed >-> proper_ideal.

-Structure idealr (R : ringType) (S : predPredType R) := MkIdeal {
+Structure idealr (R : ringType) (S : {pred R}) := MkIdeal {
  idealr_zmod :> zmodPred S;
  _ : proper_ideal S
}.

-Structure prime_idealr (R : ringType) (S : predPredType R) := MkPrimeIdeal {
+Structure prime_idealr (R : ringType) (S : {pred R}) := MkPrimeIdeal {
  prime_idealr_zmod :> idealr S;
  _ : prime_idealr_closed S
}.

-Definition Idealr (R : ringType) (I : predPredType R) (zmodI : zmodPred I)
-            (kI : keyed_pred zmodI) : proper_ideal I → idealr I.
+Definition Idealr (R : ringType) (I : {pred R}) (zmodI : zmodPred I)
+            (kI : keyed_pred zmodI) : proper_ideal I → idealr I.

Section IdealTheory.
-Variables (R : ringType) (I : predPredType R)
-          (idealrI : idealr I) (kI : keyed_pred idealrI).
+Variables (R : ringType) (I : {pred R})
+          (idealrI : idealr I) (kI : keyed_pred idealrI).

-Lemma idealr1 : 1 \in kI = false.
+Lemma idealr1 : 1 \in kI = false.

-Lemma idealMr a u : u \in kI → a × u \in kI.
+Lemma idealMr a u : u \in kI → a × u \in kI.

-Lemma idealr0 : 0 \in kI.
+Lemma idealr0 : 0 \in kI.

End IdealTheory.
@@ -578,11 +576,11 @@ Section PrimeIdealTheory.

-Variables (R : comRingType) (I : predPredType R)
-          (pidealrI : prime_idealr I) (kI : keyed_pred pidealrI).
+Variables (R : comRingType) (I : {pred R})
+          (pidealrI : prime_idealr I) (kI : keyed_pred pidealrI).

-Lemma prime_idealrM u v : (u × v \in kI) = (u \in kI) || (v \in kI).
+Lemma prime_idealrM u v : (u × v \in kI) = (u \in kI) || (v \in kI).

End PrimeIdealTheory.
@@ -593,14 +591,14 @@
Module Quotient.
Section ZmodQuotient.
-Variables (R : zmodType) (I : predPredType R)
-          (zmodI : zmodPred I) (kI : keyed_pred zmodI).
+Variables (R : zmodType) (I : {pred R})
+          (zmodI : zmodPred I) (kI : keyed_pred zmodI).

-Definition equiv (x y : R) := (x - y) \in kI.
+Definition equiv (x y : R) := (x - y) \in kI.

-Lemma equivE x y : (equiv x y) = (x - y \in kI).
+Lemma equivE x y : (equiv x y) = (x - y \in kI).

Lemma equiv_is_equiv : equiv_class_of equiv.
@@ -610,99 +608,99 @@ Canonical equiv_encModRel := defaultEncModRel equiv.

-Definition type := {eq_quot equiv}.
-Definition type_of of phant R := type.
+Definition type := {eq_quot equiv}.
+Definition type_of of phant R := type.

-Canonical rquot_quotType := [quotType of type].
-Canonical rquot_eqType := [eqType of type].
-Canonical rquot_choiceType := [choiceType of type].
-Canonical rquot_eqQuotType := [eqQuotType equiv of type].
+Canonical rquot_quotType := [quotType of type].
+Canonical rquot_eqType := [eqType of type].
+Canonical rquot_choiceType := [choiceType of type].
+Canonical rquot_eqQuotType := [eqQuotType equiv of type].

-Lemma idealrBE x y : (x - y) \in kI = (x == y %[mod type]).
+Lemma idealrBE x y : (x - y) \in kI = (x == y %[mod type]).

-Lemma idealrDE x y : (x + y) \in kI = (x == - y %[mod type]).
+Lemma idealrDE x y : (x + y) \in kI = (x == - y %[mod type]).

Definition zero : type := lift_cst type 0.
-Definition add := lift_op2 type +%R.
-Definition opp := lift_op1 type -%R.
+Definition add := lift_op2 type +%R.
+Definition opp := lift_op1 type -%R.

Canonical pi_zero_morph := PiConst zero.

-Lemma pi_opp : {morph \pi : x / - x >-> opp x}.
+Lemma pi_opp : {morph \pi : x / - x >-> opp x}.

Canonical pi_opp_morph := PiMorph1 pi_opp.

-Lemma pi_add : {morph \pi : x y / x + y >-> add x y}.
+Lemma pi_add : {morph \pi : x y / x + y >-> add x y}.
Canonical pi_add_morph := PiMorph2 pi_add.

-Lemma addqA: associative add.
+Lemma addqA: associative add.

-Lemma addqC: commutative add.
+Lemma addqC: commutative add.

-Lemma add0q: left_id zero add.
+Lemma add0q: left_id zero add.

-Lemma addNq: left_inverse zero opp add.
+Lemma addNq: left_inverse zero opp add.

Definition rquot_zmodMixin := ZmodMixin addqA addqC add0q addNq.
Canonical rquot_zmodType := Eval hnf in ZmodType type rquot_zmodMixin.

-Definition rquot_zmodQuotMixin := ZmodQuotMixin type (lock _) pi_opp pi_add.
-Canonical rquot_zmodQuotType := ZmodQuotType 0 -%R +%R type rquot_zmodQuotMixin.
+Definition rquot_zmodQuotMixin := ZmodQuotMixin type (lock _) pi_opp pi_add.
+Canonical rquot_zmodQuotType := ZmodQuotType 0 -%R +%R type rquot_zmodQuotMixin.

End ZmodQuotient.

-Notation "{quot I }" := (@type_of _ _ _ I (Phant _)).
+Notation "{quot I }" := (@type_of _ _ _ I (Phant _)).

Section RingQuotient.

-Variables (R : comRingType) (I : predPredType R)
-          (idealI : idealr I) (kI : keyed_pred idealI).
+Variables (R : comRingType) (I : {pred R})
+          (idealI : idealr I) (kI : keyed_pred idealI).


Definition one: type := lift_cst type 1.
-Definition mul := lift_op2 type *%R.
+Definition mul := lift_op2 type *%R.

Canonical pi_one_morph := PiConst one.

-Lemma pi_mul: {morph \pi : x y / x × y >-> mul x y}.
+Lemma pi_mul: {morph \pi : x y / x × y >-> mul x y}.
Canonical pi_mul_morph := PiMorph2 pi_mul.

-Lemma mulqA: associative mul.
+Lemma mulqA: associative mul.

-Lemma mulqC: commutative mul.
+Lemma mulqC: commutative mul.

-Lemma mul1q: left_id one mul.
+Lemma mul1q: left_id one mul.

-Lemma mulq_addl: left_distributive mul +%R.
+Lemma mulq_addl: left_distributive mul +%R.

-Lemma nonzero1q: one != 0.
+Lemma nonzero1q: one != 0.

Definition rquot_comRingMixin :=
@@ -713,8 +711,8 @@ Canonical rquot_comRingType := Eval hnf in ComRingType type mulqC.

-Definition rquot_ringQuotMixin := RingQuotMixin type (lock _) pi_mul.
-Canonical rquot_ringQuotType := RingQuotType 1 *%R type rquot_ringQuotMixin.
+Definition rquot_ringQuotMixin := RingQuotMixin type (lock _) pi_mul.
+Canonical rquot_ringQuotType := RingQuotType 1 *%R type rquot_ringQuotMixin.

End RingQuotient.
@@ -723,11 +721,11 @@ Section IDomainQuotient.

-Variables (R : comRingType) (I : predPredType R)
-          (pidealI : prime_idealr I) (kI : keyed_pred pidealI).
+Variables (R : comRingType) (I : {pred R})
+          (pidealI : prime_idealr I) (kI : keyed_pred pidealI).

-Lemma rquot_IdomainAxiom (x y : {quot kI}): x × y = 0 → (x == 0) || (y == 0).
+Lemma rquot_IdomainAxiom (x y : {quot kI}): x × y = 0 → (x == 0) || (y == 0).

End IDomainQuotient.
@@ -736,15 +734,15 @@ End Quotient.

-Notation "{ideal_quot I }" := (@Quotient.type_of _ _ _ I (Phant _)).
-Notation "x == y %[mod_ideal I ]" :=
-  (x == y %[mod {ideal_quot I}]) : quotient_scope.
-Notation "x = y %[mod_ideal I ]" :=
-  (x = y %[mod {ideal_quot I}]) : quotient_scope.
-Notation "x != y %[mod_ideal I ]" :=
-  (x != y %[mod {ideal_quot I}]) : quotient_scope.
-Notation "x <> y %[mod_ideal I ]" :=
-  (x ≠ y %[mod {ideal_quot I}]) : quotient_scope.
+Notation "{ideal_quot I }" := (@Quotient.type_of _ _ _ I (Phant _)).
+Notation "x == y %[mod_ideal I ]" :=
+  (x == y %[mod {ideal_quot I}]) : quotient_scope.
+Notation "x = y %[mod_ideal I ]" :=
+  (x = y %[mod {ideal_quot I}]) : quotient_scope.
+Notation "x != y %[mod_ideal I ]" :=
+  (x != y %[mod {ideal_quot I}]) : quotient_scope.
+Notation "x <> y %[mod_ideal I ]" :=
+  (x ≠ y %[mod {ideal_quot I}]) : quotient_scope.

Canonical Quotient.rquot_eqType.
-- cgit v1.2.3