Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2004 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (152 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (25 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (213 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (15 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (687 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (109 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (101 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (76 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (109 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (27 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (32 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (368 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (90 entries)

Global Index

A

Acc_rect_dep [definition, in smithpid]
ACC_GCD [definition, in dvdring]
acc_dep [definition, in dvdring]
addid [definition, in stronglydiscrete]
addidC [lemma, in stronglydiscrete]
addid_congr [lemma, in stronglydiscrete]
addid_addA [lemma, in stronglydiscrete]
addid0 [lemma, in stronglydiscrete]
addmA_subproof [lemma, in fpmod]
addmC_subproof [lemma, in fpmod]
addmor [definition, in fpmod]
addmor_proof [lemma, in fpmod]
addNm_subproof [lemma, in fpmod]
add_diag_block [lemma, in mxstructure]
add_addir [lemma, in stronglydiscrete]
add_addil [lemma, in stronglydiscrete]
add0id [lemma, in stronglydiscrete]
add0m_subproof [lemma, in fpmod]
AdequacyEDR [section, in kaplansky]
AdequacyEDR.gdco [variable, in kaplansky]
AdequacyEDR.gdcoP [variable, in kaplansky]
AdequacyEDR.R [variable, in kaplansky]
AdequacyGdco [section, in kaplansky]
AdequacyGdco.R [variable, in kaplansky]
AdequacyPID [section, in kaplansky]
AdequacyPID.R [variable, in kaplansky]
AdequateSpec [constructor, in kaplansky]
AdequateSpec0 [constructor, in kaplansky]
adequate_gdco [lemma, in kaplansky]
adequate_spec [inductive, in kaplansky]
AlgOp [module, in refinements]
AlgOp.AlgOp [section, in refinements]
AlgOp.divr [definition, in refinements]
AlgOp.subr [definition, in refinements]


B

bcap [definition, in coherent]
bcap_spec [lemma, in coherent]
bcap_int [lemma, in coherent]
bcap_wrP [lemma, in coherent]
bcap_wr [definition, in coherent]
bcap_wlP [lemma, in coherent]
bcap_wl [definition, in coherent]
bdim_cap [definition, in coherent]
bezout [definition, in dvdring]
BezoutCoherent [section, in coherent]
BezoutCoherent.R [variable, in coherent]
BezoutDomain [module, in dvdring]
BezoutDomainTheory [section, in dvdring]
BezoutDomainTheory.Bezout_mx [section, in dvdring]
BezoutDomainTheory.R [variable, in dvdring]
BezoutDomain.base [projection, in dvdring]
BezoutDomain.bezout [projection, in dvdring]
BezoutDomain.BezoutSpec [constructor, in dvdring]
BezoutDomain.bezout_spec [inductive, in dvdring]
BezoutDomain.choiceType [definition, in dvdring]
BezoutDomain.class [definition, in dvdring]
BezoutDomain.Class [constructor, in dvdring]
BezoutDomain.ClassDef [section, in dvdring]
BezoutDomain.ClassDef.cT [variable, in dvdring]
BezoutDomain.ClassDef.T [variable, in dvdring]
BezoutDomain.class_of [record, in dvdring]
BezoutDomain.clone [definition, in dvdring]
BezoutDomain.comRingType [definition, in dvdring]
BezoutDomain.comUnitRingType [definition, in dvdring]
BezoutDomain.dvdRingType [definition, in dvdring]
BezoutDomain.eqType [definition, in dvdring]
BezoutDomain.Exports [module, in dvdring]
BezoutDomain.Exports.BezoutDomainMixin [abbreviation, in dvdring]
BezoutDomain.Exports.BezoutDomainType [abbreviation, in dvdring]
BezoutDomain.Exports.bezoutDomainType [abbreviation, in dvdring]
[ bezoutDomainType of _ ] (form_scope) [notation, in dvdring]
[ bezoutDomainType of _ for _ ] (form_scope) [notation, in dvdring]
BezoutDomain.gcdDomainType [definition, in dvdring]
BezoutDomain.idomainType [definition, in dvdring]
BezoutDomain.mixin [projection, in dvdring]
BezoutDomain.Mixin [constructor, in dvdring]
BezoutDomain.mixin_of [record, in dvdring]
BezoutDomain.pack [definition, in dvdring]
BezoutDomain.Pack [constructor, in dvdring]
BezoutDomain.ringType [definition, in dvdring]
BezoutDomain.sort [projection, in dvdring]
BezoutDomain.type [record, in dvdring]
BezoutDomain.unitRingType [definition, in dvdring]
BezoutDomain.zmodType [definition, in dvdring]
BezoutKrull1 [section, in kaplansky]
BezoutKrull1.krull1 [variable, in kaplansky]
BezoutKrull1.R [variable, in kaplansky]
bezoutMixin [definition, in edr]
bezoutP [lemma, in dvdring]
BezoutStronglyDiscrete [section, in stronglydiscrete]
BezoutStronglyDiscrete.R [variable, in stronglydiscrete]
bezoutType [definition, in edr]
Bezout_step_mx00 [lemma, in dvdring]
Bezout_stepE [lemma, in dvdring]
Bezout_step [definition, in dvdring]
Bezout_mx [definition, in dvdring]
Bezout_hermite.R [variable, in kaplansky]
Bezout_hermite [section, in kaplansky]
bezout_coherentType [definition, in coherent]
bezout_coherentMixin [definition, in coherent]
bezout_stronglyDiscreteType [definition, in stronglydiscrete]
bezout_stronglyDiscreteMixin [definition, in stronglydiscrete]
bezout_edrP [lemma, in edr]
bezout_edr [definition, in edr]
BigOp [section, in ssrcomplements]
BigOp.R [variable, in ssrcomplements]
BigOp.T [variable, in ssrcomplements]
big_gcdr_def [lemma, in dvdring]
big_gcdrP [lemma, in dvdring]
big_dvdr_gcdr [lemma, in dvdring]
big_dvdr [lemma, in dvdring]
BinetCauchy [lemma, in binetcauchy]
BinetCauchy [section, in binetcauchy]
binetcauchy [library]
BinetCauchy.A [variable, in binetcauchy]
BinetCauchy.B [variable, in binetcauchy]
BinetCauchy.k [variable, in binetcauchy]
BinetCauchy.l [variable, in binetcauchy]
BinetCauchy.R [variable, in binetcauchy]
BinetCauchy.Z [variable, in binetcauchy]
bmember [definition, in stronglydiscrete]
bmember_correct [lemma, in stronglydiscrete]
bool [section, in refinements]
bool_if [definition, in refinements]


C

cap_wr [definition, in coherent]
cap_wl [definition, in coherent]
cast [abbreviation, in refinements]
cast0 [lemma, in binetcauchy]
cast1 [lemma, in binetcauchy]
char_diag_block_mx [lemma, in mxstructure]
char_poly_triangular_mx [lemma, in mxstructure]
char_poly_mx_triangular_mx [lemma, in mxstructure]
char_block_mx [lemma, in ssrcomplements]
codom_perm [lemma, in binetcauchy]
coherent [library]
coherentMixin [definition, in edr]
CoherentRing [module, in coherent]
CoherentRingTheory [section, in coherent]
CoherentRingTheory.R [variable, in coherent]
_ .-ker (mxpresentation_scope) [notation, in coherent]
_ %| _ (mxpresentation_scope) [notation, in coherent]
CoherentRing.base [projection, in coherent]
CoherentRing.choiceType [definition, in coherent]
CoherentRing.class [definition, in coherent]
CoherentRing.Class [constructor, in coherent]
CoherentRing.ClassDef [section, in coherent]
CoherentRing.ClassDef.cT [variable, in coherent]
CoherentRing.ClassDef.T [variable, in coherent]
CoherentRing.class_of [record, in coherent]
CoherentRing.clone [definition, in coherent]
CoherentRing.comRingType [definition, in coherent]
CoherentRing.comUnitRingType [definition, in coherent]
CoherentRing.dim_ker [projection, in coherent]
CoherentRing.eqType [definition, in coherent]
CoherentRing.Exports [module, in coherent]
CoherentRing.Exports.CoherentRingMixin [abbreviation, in coherent]
CoherentRing.Exports.CoherentRingType [abbreviation, in coherent]
CoherentRing.Exports.coherentRingType [abbreviation, in coherent]
[ coherentRingType of _ ] (form_scope) [notation, in coherent]
[ coherentRingType of _ for _ ] (form_scope) [notation, in coherent]
CoherentRing.idomainType [definition, in coherent]
CoherentRing.ker [projection, in coherent]
CoherentRing.mixin [projection, in coherent]
CoherentRing.Mixin [constructor, in coherent]
CoherentRing.mixin_of [record, in coherent]
CoherentRing.pack [definition, in coherent]
CoherentRing.Pack [constructor, in coherent]
CoherentRing.ringType [definition, in coherent]
CoherentRing.sort [projection, in coherent]
CoherentRing.stronglyDiscreteType [definition, in coherent]
CoherentRing.type [record, in coherent]
CoherentRing.unitRingType [definition, in coherent]
CoherentRing.zmodType [definition, in coherent]
coherentType [definition, in edr]
coker [definition, in fpmod]
cokerK [lemma, in fpmod]
cokermx [definition, in edr]
cokerP [lemma, in fpmod]
coker_eq0 [lemma, in fpmod]
colE [lemma, in coherent]
col_id_mulmx [lemma, in ssrcomplements]
col_0mx [lemma, in ssrcomplements]
col_flat_mx [lemma, in ssrcomplements]
col_ebase_unit [lemma, in edr]
col_ebase [definition, in edr]
combine_mx_inv [lemma, in dvdring]
combine_stepE [lemma, in dvdring]
combine_step [definition, in dvdring]
combine_mx [definition, in dvdring]
complements [section, in similar]
Composable [projection, in refinements]
composable [record, in refinements]
Composable [constructor, in refinements]
composable [inductive, in refinements]
composableE [lemma, in refinements]
composable_imply_id1 [lemma, in refinements]
composable_imply [lemma, in refinements]
composable_comp [instance, in refinements]
composable_rid1 [lemma, in refinements]
composable_proper [instance, in refinements]
composable_sub_proper [instance, in refinements]
composable_lock [lemma, in refinements]
comp_eql [lemma, in hrel]
comp_eqr [lemma, in hrel]
comp_hrel_eq_proper [instance, in hrel]
comp_hrel_sub_proper [instance, in hrel]
comp_hrelP [lemma, in hrel]
comp_hrel [definition, in hrel]
congr_eqd [lemma, in dvdring]
coprimep_factor [lemma, in ssrcomplements]
coprimer [definition, in dvdring]
coprimerP [lemma, in kaplansky]
coprimer_pexpr [lemma, in dvdring]
coprimer_pexpl [lemma, in dvdring]
coprimer_expr [lemma, in dvdring]
coprimer_expl [lemma, in dvdring]
coprimer_dvdr [lemma, in dvdring]
coprimer_dvdl [lemma, in dvdring]
coprimer_mull [lemma, in dvdring]
coprimer_mulr [lemma, in dvdring]
coprimer_sym [lemma, in dvdring]
coprimer_gdco [lemma, in kaplansky]


D

detAB_weight [lemma, in binetcauchy]
detmx2 [lemma, in kaplansky]
det_diag_mx_seq [lemma, in mxstructure]
det_diag_mx_seq_truncated [lemma, in mxstructure]
det_diag_block [lemma, in mxstructure]
det_triangular_mx [lemma, in mxstructure]
det2 [lemma, in minor]
diag [definition, in edr]
diag_mx_seq_filter0 [lemma, in mxstructure]
diag_mx_dvdring.R [variable, in mxstructure]
diag_mx_dvdring [section, in mxstructure]
diag_mx_idomain.R [variable, in mxstructure]
diag_mx_idomain [section, in mxstructure]
diag_mx_seq_comRingType.R [variable, in mxstructure]
diag_mx_seq_comRingType [section, in mxstructure]
diag_mx_seq2.R [variable, in mxstructure]
diag_mx_seq2 [section, in mxstructure]
diag_mx_seq_scale [lemma, in mxstructure]
diag_mx_seq_eq0 [lemma, in mxstructure]
diag_mx_seq0 [lemma, in mxstructure]
diag_mx_seq_take_min [lemma, in mxstructure]
diag_mx_seq_taker [lemma, in mxstructure]
diag_mx_seq_takel [lemma, in mxstructure]
diag_mx_seq_deltar [lemma, in mxstructure]
diag_mx_seq_deltal [lemma, in mxstructure]
diag_block_mx_seq [lemma, in mxstructure]
diag_mx_seq_block [lemma, in mxstructure]
diag_mx_seq_block_mx [lemma, in mxstructure]
diag_mx_seq_cat [lemma, in mxstructure]
diag_mx_seq_cons [lemma, in mxstructure]
diag_mx_seq_nil [lemma, in mxstructure]
diag_mx_seq [definition, in mxstructure]
diag_mx_seq.R [variable, in mxstructure]
diag_mx_seq [section, in mxstructure]
diag_block_comUnitRingType.R [variable, in mxstructure]
diag_block_comUnitRingType [section, in mxstructure]
diag_block_comRingType.R [variable, in mxstructure]
diag_block_comRingType [section, in mxstructure]
diag_block_ringType2.R [variable, in mxstructure]
diag_block_ringType2 [section, in mxstructure]
diag_block_mx0 [lemma, in mxstructure]
diag_block_mx [definition, in mxstructure]
diag_block_mx_rec [definition, in mxstructure]
diag_block_ringType.R [variable, in mxstructure]
diag_block_ringType [section, in mxstructure]
diag_neq0 [lemma, in edr]
diag_mx [definition, in edr]
diag0 [lemma, in edr]
dim_int [definition, in coherent]
dim_ker_c [definition, in coherent]
dim_ker [definition, in coherent]
divid [definition, in stronglydiscrete]
dividK [lemma, in stronglydiscrete]
divmx [definition, in coherent]
divmxK [lemma, in coherent]
divr [definition, in dvdring]
divr_mulKl [lemma, in dvdring]
divr_mulKr [lemma, in dvdring]
dsum [definition, in fpmod]
dsum_is_coproduct [lemma, in fpmod]
dsum_is_product [lemma, in fpmod]
dvdmx [definition, in coherent]
dvdmxB [lemma, in coherent]
dvdmxBl [lemma, in coherent]
dvdmxBr [lemma, in coherent]
dvdmxD [lemma, in coherent]
dvdmxDl [lemma, in coherent]
dvdmxDr [lemma, in coherent]
dvdmxMl [lemma, in coherent]
dvdmxMr [lemma, in coherent]
dvdmxN [lemma, in coherent]
dvdmxP [lemma, in coherent]
dvdmx_morphism [lemma, in fpmod]
dvdmx_trans [lemma, in coherent]
dvdmx_refl [lemma, in coherent]
dvdmx0 [lemma, in coherent]
dvdNmx [lemma, in coherent]
dvdNr [lemma, in dvdring]
dvdr [definition, in dvdring]
DvdRing [section, in similar]
DvdRing [module, in dvdring]
dvdring [library]
DvdRingTheory [section, in dvdring]
DvdRingTheory.R [variable, in dvdring]
DvdRing.base [projection, in dvdring]
DvdRing.choiceType [definition, in dvdring]
DvdRing.class [definition, in dvdring]
DvdRing.Class [constructor, in dvdring]
DvdRing.ClassDef [section, in dvdring]
DvdRing.ClassDef.cT [variable, in dvdring]
DvdRing.ClassDef.T [variable, in dvdring]
DvdRing.class_of [record, in dvdring]
DvdRing.clone [definition, in dvdring]
DvdRing.comRingType [definition, in dvdring]
DvdRing.comUnitRingType [definition, in dvdring]
DvdRing.div [projection, in dvdring]
DvdRing.DivDvd [constructor, in dvdring]
DvdRing.DivNDvd [constructor, in dvdring]
DvdRing.div_spec [inductive, in dvdring]
DvdRing.eqType [definition, in dvdring]
DvdRing.Exports [module, in dvdring]
DvdRing.Exports.DvdRingMixin [abbreviation, in dvdring]
DvdRing.Exports.DvdRingType [abbreviation, in dvdring]
DvdRing.Exports.dvdRingType [abbreviation, in dvdring]
[ dvdRingType of _ ] (form_scope) [notation, in dvdring]
[ dvdRingType of _ for _ ] (form_scope) [notation, in dvdring]
DvdRing.idomainType [definition, in dvdring]
DvdRing.mixin [projection, in dvdring]
DvdRing.Mixin [constructor, in dvdring]
DvdRing.mixin_of [record, in dvdring]
DvdRing.pack [definition, in dvdring]
DvdRing.Pack [constructor, in dvdring]
DvdRing.R [variable, in similar]
DvdRing.ringType [definition, in dvdring]
DvdRing.sort [projection, in dvdring]
DvdRing.type [record, in dvdring]
DvdRing.unitRingType [definition, in dvdring]
DvdRing.zmodType [definition, in dvdring]
dvdrN [lemma, in dvdring]
dvdrNN [lemma, in dvdring]
dvdrP [lemma, in dvdring]
dvdrr [lemma, in dvdring]
dvdrU [lemma, in dvdring]
dvdr_mod [lemma, in dvdring]
dvdr_coprime [lemma, in dvdring]
dvdr_mem_lcms [lemma, in dvdring]
dvdr_lcms [lemma, in dvdring]
dvdr_mem_gcds [lemma, in dvdring]
dvdr_gcds [lemma, in dvdring]
dvdr_lcm_idl [lemma, in dvdring]
dvdr_lcm_idr [lemma, in dvdring]
dvdr_gcdr_lcmr [lemma, in dvdring]
dvdr_lcmr [lemma, in dvdring]
dvdr_lcml [lemma, in dvdring]
dvdr_lcm [lemma, in dvdring]
dvdr_gcd_mul [lemma, in dvdring]
dvdr_gcdr [lemma, in dvdring]
dvdr_gcdl [lemma, in dvdring]
dvdr_gcd [lemma, in dvdring]
dvdr_row_mx [lemma, in dvdring]
dvdr_col_mx [lemma, in dvdring]
dvdr_drsubmx [lemma, in dvdring]
dvdr_dlsubmx [lemma, in dvdring]
dvdr_ursubmx [lemma, in dvdring]
dvdr_ulsubmx [lemma, in dvdring]
dvdr_lsubmx [lemma, in dvdring]
dvdr_rsubmx [lemma, in dvdring]
dvdr_dsubmx [lemma, in dvdring]
dvdr_usubmx [lemma, in dvdring]
dvdr_mulmxl [lemma, in dvdring]
dvdr_mulmxr [lemma, in dvdring]
dvdr_mull_l [lemma, in dvdring]
dvdr_mulr_l [lemma, in dvdring]
dvdr_mul2l [lemma, in dvdring]
dvdr_mul2r [lemma, in dvdring]
dvdr_mul [lemma, in dvdring]
dvdr_mulr [lemma, in dvdring]
dvdr_mull [lemma, in dvdring]
dvdr_add_eq [lemma, in dvdring]
dvdr_addr [lemma, in dvdring]
dvdr_addl [lemma, in dvdring]
dvdr_sub [lemma, in dvdring]
dvdr_add [lemma, in dvdring]
dvdr_trans [lemma, in dvdring]
dvdr0 [lemma, in dvdring]
dvdr1 [lemma, in dvdring]
dvdUr [lemma, in dvdring]
dvd_quot_mx [lemma, in fpmod]
dvd_col_mxu [lemma, in coherent]
dvd_col_mxl [lemma, in coherent]
dvd_col_mxP [lemma, in coherent]
dvd_mx_col [lemma, in coherent]
dvd_ker_mod_1 [lemma, in coherent]
dvd_ker_mod_ker [lemma, in coherent]
dvd_ker [lemma, in coherent]
dvd0mx [lemma, in coherent]
dvd0r [lemma, in dvdring]
dvd1mx [lemma, in coherent]
dvd1r [lemma, in dvdring]


E

edivr [definition, in dvdring]
edivrP [lemma, in dvdring]
EDR [module, in edr]
edr [library]
EDR_Theory.Unicity [section, in edr]
EDR_Theory.Preunicity.widen_minr [variable, in edr]
EDR_Theory.Preunicity.widen_minl [variable, in edr]
EDR_Theory.Preunicity.HAs [variable, in edr]
EDR_Theory.Preunicity.Hs [variable, in edr]
EDR_Theory.Preunicity.Hk [variable, in edr]
EDR_Theory.Preunicity.A [variable, in edr]
EDR_Theory.Preunicity.k [variable, in edr]
EDR_Theory.Preunicity.n [variable, in edr]
EDR_Theory.Preunicity.m [variable, in edr]
EDR_Theory.Preunicity.s [variable, in edr]
EDR_Theory.Preunicity [section, in edr]
EDR_Theory.snf_coherent.defs.M [variable, in edr]
EDR_Theory.snf_coherent.defs.n [variable, in edr]
EDR_Theory.snf_coherent.defs.m [variable, in edr]
EDR_Theory.snf_coherent.defs [section, in edr]
EDR_Theory.snf_coherent [section, in edr]
EDR_Theory.R [variable, in edr]
EDR_Theory [section, in edr]
EDR.base [projection, in edr]
EDR.choiceType [definition, in edr]
EDR.class [definition, in edr]
EDR.Class [constructor, in edr]
EDR.ClassDef [section, in edr]
EDR.ClassDef.cT [variable, in edr]
EDR.ClassDef.T [variable, in edr]
EDR.class_of [record, in edr]
EDR.clone [definition, in edr]
EDR.comRingType [definition, in edr]
EDR.comUnitRingType [definition, in edr]
EDR.dvdRingType [definition, in edr]
EDR.eqType [definition, in edr]
EDR.Exports [module, in edr]
EDR.Exports.EDRMixin [abbreviation, in edr]
EDR.Exports.EDRType [abbreviation, in edr]
EDR.Exports.edrType [abbreviation, in edr]
[ edrType of _ ] (form_scope) [notation, in edr]
[ edrType of _ for _ ] (form_scope) [notation, in edr]
EDR.idomainType [definition, in edr]
EDR.mixin [projection, in edr]
EDR.Mixin [constructor, in edr]
EDR.mixin_of [record, in edr]
EDR.pack [definition, in edr]
EDR.Pack [constructor, in edr]
EDR.ringType [definition, in edr]
EDR.smith [projection, in edr]
EDR.SmithSpec [constructor, in edr]
EDR.smith_spec [inductive, in edr]
EDR.sort [projection, in edr]
EDR.type [record, in edr]
EDR.unitRingType [definition, in edr]
EDR.zmodType [definition, in edr]
egcdr [definition, in dvdring]
egcdrP [lemma, in dvdring]
EgcdrSpec [constructor, in dvdring]
EgcdrSpec [constructor, in kaplansky]
egcdr_spec [inductive, in dvdring]
egcdr3 [definition, in kaplansky]
egcdr3P [lemma, in kaplansky]
egcdr3_spec [inductive, in kaplansky]
enorm [definition, in dvdring]
enorm_eq0 [lemma, in dvdring]
enorm_mul [lemma, in dvdring]
enorm0_lt [lemma, in dvdring]
epi [lemma, in fpmod]
epimorphism [definition, in fpmod]
Epimorphism [constructor, in fpmod]
epimorphism_of [record, in fpmod]
epiP [lemma, in fpmod]
EpiTheory [section, in fpmod]
EpiTheory.Epi1 [section, in fpmod]
EpiTheory.Epi1.M [variable, in fpmod]
EpiTheory.Epi1.N [variable, in fpmod]
EpiTheory.R [variable, in fpmod]
epi_coker [lemma, in fpmod]
epi_of_coker [definition, in fpmod]
epi_of_iso [definition, in fpmod]
epi_of [definition, in fpmod]
eqd [definition, in dvdring]
eqdd [lemma, in dvdring]
eqdP [lemma, in dvdring]
eqdr0 [lemma, in dvdring]
eqd_equiv [lemma, in similar]
eqd_lcml [lemma, in dvdring]
eqd_lcmr [lemma, in dvdring]
eqd_gcd [lemma, in dvdring]
eqd_big_mul1 [lemma, in dvdring]
eqd_big_mul [lemma, in dvdring]
eqd_mull [lemma, in dvdring]
eqd_mulr [lemma, in dvdring]
eqd_rtrans [lemma, in dvdring]
eqd_ltrans [lemma, in dvdring]
eqd_dvdl [lemma, in dvdring]
eqd_dvdr [lemma, in dvdring]
eqd_dvd [lemma, in dvdring]
eqd_mul2r [lemma, in dvdring]
eqd_mul2l [lemma, in dvdring]
eqd_mul [lemma, in dvdring]
eqd_trans [lemma, in dvdring]
eqd_sym [lemma, in dvdring]
eqd_def [lemma, in dvdring]
eqd_seq_gcdr [lemma, in edr]
eqd0r [lemma, in dvdring]
eqd1 [lemma, in dvdring]
EqHrel [constructor, in hrel]
eqid [definition, in stronglydiscrete]
eqidP [lemma, in stronglydiscrete]
eqid_mulidAl [lemma, in stronglydiscrete]
eqid_tr_mxvec [lemma, in stronglydiscrete]
eqid_scaleid [lemma, in stronglydiscrete]
eqid_trans [lemma, in stronglydiscrete]
eqid_sym [lemma, in stronglydiscrete]
eqid_refl [lemma, in stronglydiscrete]
eqid_eq0 [lemma, in stronglydiscrete]
eqmor [definition, in fpmod]
eqmorMl [lemma, in fpmod]
eqmorMr [lemma, in fpmod]
eqmorxx [lemma, in fpmod]
eqmor_mono [lemma, in fpmod]
eqmor_epi [lemma, in fpmod]
eqmor_rtrans [lemma, in fpmod]
eqmor_ltrans [lemma, in fpmod]
eqmor_trans [lemma, in fpmod]
eqmor_sym [lemma, in fpmod]
eqmor_refl [lemma, in fpmod]
equivalent [definition, in similar]
EquivalentDef [section, in similar]
EquivalentDef.R [variable, in similar]
equiv_diag_block [lemma, in similar]
equiv_cast [lemma, in similar]
equiv_dgblockmx [lemma, in similar]
equiv_drblockmx [lemma, in similar]
equiv_ulblockmx [lemma, in similar]
equiv_trans [lemma, in similar]
equiv_sym [lemma, in similar]
equiv_refl [lemma, in similar]
equiv0l [lemma, in similar]
equiv0r [lemma, in similar]
eq_hrel_equiv [instance, in hrel]
eq_hrelLR [lemma, in hrel]
eq_hrelRL [lemma, in hrel]
eq_hrel [inductive, in hrel]
eq_eqd [lemma, in dvdring]
euclid [lemma, in dvdring]
EuclideanDomain [module, in dvdring]
EuclideanDomainTheory [section, in dvdring]
EuclideanDomainTheory.R [variable, in dvdring]
EuclideanDomain.base [projection, in dvdring]
EuclideanDomain.bezoutDomainType [definition, in dvdring]
EuclideanDomain.choiceType [definition, in dvdring]
EuclideanDomain.class [definition, in dvdring]
EuclideanDomain.Class [constructor, in dvdring]
EuclideanDomain.ClassDef [section, in dvdring]
EuclideanDomain.ClassDef.cT [variable, in dvdring]
EuclideanDomain.ClassDef.T [variable, in dvdring]
EuclideanDomain.class_of [record, in dvdring]
EuclideanDomain.clone [definition, in dvdring]
EuclideanDomain.comRingType [definition, in dvdring]
EuclideanDomain.comUnitRingType [definition, in dvdring]
EuclideanDomain.dvdRingType [definition, in dvdring]
EuclideanDomain.ediv [projection, in dvdring]
EuclideanDomain.EdivrSpec [constructor, in dvdring]
EuclideanDomain.edivr_spec [inductive, in dvdring]
EuclideanDomain.enorm [projection, in dvdring]
EuclideanDomain.eqType [definition, in dvdring]
EuclideanDomain.EuclidBezoutMixin [definition, in dvdring]
EuclideanDomain.EuclidDvdMixin [definition, in dvdring]
EuclideanDomain.EuclidGCDMixin [definition, in dvdring]
EuclideanDomain.EuclidGcdMixin [definition, in dvdring]
EuclideanDomain.EuclidPIDMixin [definition, in dvdring]
EuclideanDomain.Exports [module, in dvdring]
EuclideanDomain.Exports.EuclidBezoutMixin [abbreviation, in dvdring]
EuclideanDomain.Exports.EuclidDomainMixin [abbreviation, in dvdring]
EuclideanDomain.Exports.EuclidDomainType [abbreviation, in dvdring]
EuclideanDomain.Exports.euclidDomainType [abbreviation, in dvdring]
EuclideanDomain.Exports.EuclidDvdMixin [abbreviation, in dvdring]
EuclideanDomain.Exports.EuclidGCDMixin [abbreviation, in dvdring]
EuclideanDomain.Exports.EuclidGcdMixin [abbreviation, in dvdring]
EuclideanDomain.Exports.EuclidPIDMixin [abbreviation, in dvdring]
[ euclidDomainType of _ ] (form_scope) [notation, in dvdring]
[ euclidDomainType of _ for _ ] (form_scope) [notation, in dvdring]
EuclideanDomain.gcdDomainType [definition, in dvdring]
EuclideanDomain.idomainType [definition, in dvdring]
EuclideanDomain.mixin [projection, in dvdring]
EuclideanDomain.Mixin [constructor, in dvdring]
EuclideanDomain.Mixins [module, in dvdring]
EuclideanDomain.Mixins.acc_gcdP [lemma, in dvdring]
EuclideanDomain.Mixins.acc_gcd [definition, in dvdring]
EuclideanDomain.Mixins.div [definition, in dvdring]
EuclideanDomain.Mixins.dvd_mod [lemma, in dvdring]
EuclideanDomain.Mixins.ediv [abbreviation, in dvdring]
EuclideanDomain.Mixins.edivP [lemma, in dvdring]
EuclideanDomain.Mixins.egcd [definition, in dvdring]
EuclideanDomain.Mixins.egcdP [lemma, in dvdring]
EuclideanDomain.Mixins.egcd_recP [lemma, in dvdring]
EuclideanDomain.Mixins.egcd_rec [definition, in dvdring]
EuclideanDomain.Mixins.EuclidBezout [definition, in dvdring]
EuclideanDomain.Mixins.EuclidDvd [definition, in dvdring]
EuclideanDomain.Mixins.euclidDvdRing [definition, in dvdring]
EuclideanDomain.Mixins.EuclidGcd [definition, in dvdring]
EuclideanDomain.Mixins.EuclidGCD [definition, in dvdring]
EuclideanDomain.Mixins.EuclidPID [definition, in dvdring]
EuclideanDomain.Mixins.gcd [definition, in dvdring]
EuclideanDomain.Mixins.GCD [definition, in dvdring]
EuclideanDomain.Mixins.gcdP [lemma, in dvdring]
EuclideanDomain.Mixins.GCDP [lemma, in dvdring]
EuclideanDomain.Mixins.gcdrE [lemma, in dvdring]
EuclideanDomain.Mixins.leq_norm [lemma, in dvdring]
EuclideanDomain.Mixins.ltn_norm [lemma, in dvdring]
EuclideanDomain.Mixins.Mixins [section, in dvdring]
EuclideanDomain.Mixins.Mixins.cR [variable, in dvdring]
EuclideanDomain.Mixins.Mixins.dvdM [variable, in dvdring]
EuclideanDomain.Mixins.Mixins.gcdM [variable, in dvdring]
EuclideanDomain.Mixins.Mixins.mR [variable, in dvdring]
EuclideanDomain.Mixins.Mixins.R [variable, in dvdring]
_ %% _ (ring_scope) [notation, in dvdring]
_ %/ _ (ring_scope) [notation, in dvdring]
EuclideanDomain.Mixins.modr0 [lemma, in dvdring]
EuclideanDomain.Mixins.mod_spec [lemma, in dvdring]
EuclideanDomain.Mixins.mod_eq0 [lemma, in dvdring]
EuclideanDomain.Mixins.mod0r [lemma, in dvdring]
EuclideanDomain.Mixins.norm [abbreviation, in dvdring]
EuclideanDomain.Mixins.norm_eq0 [lemma, in dvdring]
EuclideanDomain.Mixins.norm_mul [lemma, in dvdring]
EuclideanDomain.Mixins.norm0_lt [lemma, in dvdring]
EuclideanDomain.Mixins.odiv [definition, in dvdring]
EuclideanDomain.Mixins.odivP [lemma, in dvdring]
EuclideanDomain.Mixins.odiv_def [lemma, in dvdring]
EuclideanDomain.Mixins.R_gcdDomain [definition, in dvdring]
EuclideanDomain.Mixins.R_idom [definition, in dvdring]
EuclideanDomain.Mixins.R_comunit [definition, in dvdring]
EuclideanDomain.Mixins.R_unit [definition, in dvdring]
EuclideanDomain.Mixins.R_com [definition, in dvdring]
EuclideanDomain.Mixins.R_ring [definition, in dvdring]
EuclideanDomain.Mixins.R_zmod [definition, in dvdring]
EuclideanDomain.Mixins.R_choiceType [definition, in dvdring]
EuclideanDomain.Mixins.R_eqType [definition, in dvdring]
EuclideanDomain.Mixins.sdvdr_wf [lemma, in dvdring]
EuclideanDomain.Mixins.tool [lemma, in dvdring]
EuclideanDomain.mixin_of [record, in dvdring]
EuclideanDomain.pack [definition, in dvdring]
EuclideanDomain.Pack [constructor, in dvdring]
EuclideanDomain.pidType [definition, in dvdring]
EuclideanDomain.ringType [definition, in dvdring]
EuclideanDomain.sort [projection, in dvdring]
EuclideanDomain.type [record, in dvdring]
EuclideanDomain.unitRingType [definition, in dvdring]
EuclideanDomain.zmodType [definition, in dvdring]
euclidEDRMixin [definition, in smith]
euclidEDRType [definition, in smith]
euclid_gcdl [lemma, in dvdring]
euclid_gcdr [lemma, in dvdring]
euclid_inv [lemma, in dvdring]
exp_diag_block_cons [lemma, in mxstructure]
exp_diag_block_S [lemma, in mxstructure]
exp_block_mx [lemma, in ssrcomplements]
ext_block [lemma, in mxstructure]


F

factor [definition, in fpmod]
factorP [lemma, in fpmod]
factor_proof [lemma, in fpmod]
Field [section, in similar]
Field.m [variable, in similar]
Field.n [variable, in similar]
Field.R [variable, in similar]
fpmod [record, in fpmod]
FPmod [constructor, in fpmod]
fpmod [library]
fpmod_of [definition, in fpmod]
from_good_to_perm [lemma, in binetcauchy]
fun_hrel [definition, in hrel]
fz_tilt_0 [lemma, in binetcauchy]


G

gather_by_strictness [lemma, in binetcauchy]
GCD [definition, in dvdring]
GcdDomain [module, in dvdring]
GCDDomainTheory [section, in dvdring]
GCDDomainTheory.R [variable, in dvdring]
GcdDomain.base [projection, in dvdring]
GcdDomain.choiceType [definition, in dvdring]
GcdDomain.class [definition, in dvdring]
GcdDomain.Class [constructor, in dvdring]
GcdDomain.ClassDef [section, in dvdring]
GcdDomain.ClassDef.cT [variable, in dvdring]
GcdDomain.ClassDef.T [variable, in dvdring]
GcdDomain.class_of [record, in dvdring]
GcdDomain.clone [definition, in dvdring]
GcdDomain.comRingType [definition, in dvdring]
GcdDomain.comUnitRingType [definition, in dvdring]
GcdDomain.dvdRingType [definition, in dvdring]
GcdDomain.eqType [definition, in dvdring]
GcdDomain.Exports [module, in dvdring]
GcdDomain.Exports.GcdDomainMixin [abbreviation, in dvdring]
GcdDomain.Exports.GcdDomainType [abbreviation, in dvdring]
GcdDomain.Exports.gcdDomainType [abbreviation, in dvdring]
[ gcdDomainType of _ ] (form_scope) [notation, in dvdring]
[ gcdDomainType of _ for _ ] (form_scope) [notation, in dvdring]
GcdDomain.gcdr [projection, in dvdring]
GcdDomain.idomainType [definition, in dvdring]
GcdDomain.mixin [projection, in dvdring]
GcdDomain.Mixin [constructor, in dvdring]
GcdDomain.mixin_of [record, in dvdring]
GcdDomain.pack [definition, in dvdring]
GcdDomain.Pack [constructor, in dvdring]
GcdDomain.ringType [definition, in dvdring]
GcdDomain.sort [projection, in dvdring]
GcdDomain.type [record, in dvdring]
GcdDomain.unitRingType [definition, in dvdring]
GcdDomain.zmodType [definition, in dvdring]
gcdMixin [definition, in edr]
gcdr [definition, in dvdring]
gcdrA [lemma, in dvdring]
gcdrAC [lemma, in dvdring]
gcdrC [lemma, in dvdring]
gcdrCA [lemma, in dvdring]
gcdr_addl_mul [lemma, in dvdring]
gcdr_addl_l [lemma, in dvdring]
gcdr_addr_l [lemma, in dvdring]
gcdr_addl_r [lemma, in dvdring]
gcdr_addr_r [lemma, in dvdring]
gcdr_mul2l [lemma, in dvdring]
gcdr_mul2r [lemma, in dvdring]
gcdr_def [lemma, in dvdring]
gcdr_eq0 [lemma, in dvdring]
gcdr0 [lemma, in dvdring]
gcdr1 [lemma, in dvdring]
gcdsr [definition, in dvdring]
gcdsr_cons [lemma, in dvdring]
gcdsr0 [lemma, in dvdring]
gcdType [definition, in edr]
gcd_edrP [lemma, in edr]
gcd_edr [definition, in edr]
gcd0r [lemma, in dvdring]
gcd1r [lemma, in dvdring]
gdcoEDRMixin [definition, in kaplansky]
gdcoEDRType [definition, in kaplansky]
GdcoSpec [constructor, in kaplansky]
GdcoSpec0 [constructor, in kaplansky]
gdco_smithP [lemma, in kaplansky]
gdco_smith [definition, in kaplansky]
gdco_kapP [lemma, in kaplansky]
gdco_kap [definition, in kaplansky]
gdco_adequate [lemma, in kaplansky]
gdco_spec [inductive, in kaplansky]
getparam [record, in refinements]
getparam [inductive, in refinements]
getparam_some [lemma, in refinements]
getparam_None [instance, in refinements]
getparam_if [lemma, in refinements]
getparam_map [lemma, in refinements]
getparam_nth [lemma, in refinements]
getparam_size [lemma, in refinements]
getparam_iter [lemma, in refinements]
getparam_foldl [lemma, in refinements]
getparam_foldr [lemma, in refinements]
getparam_rcons [lemma, in refinements]
getparam_cons [lemma, in refinements]
getparam_nil [instance, in refinements]
getparam_sum_rect [lemma, in refinements]
getparam_inr [lemma, in refinements]
getparam_inl [lemma, in refinements]
getparam_snd [lemma, in refinements]
getparam_fst [lemma, in refinements]
getparam_pair [lemma, in refinements]
getparam_abstr [lemma, in refinements]
getparam_eq [lemma, in refinements]
getparam_proper [instance, in refinements]
getparam_sub_proper [instance, in refinements]
getparam_rel [projection, in refinements]
getparam_rel [constructor, in refinements]
getparam_key [lemma, in refinements]
get_param [lemma, in refinements]
good [definition, in binetcauchy]
goodP [lemma, in binetcauchy]
GUARD [section, in dvdring]
guarded [definition, in dvdring]
GUARD.A [variable, in dvdring]
GUARD.P [variable, in dvdring]


H

hermite [definition, in kaplansky]
hermite10 [lemma, in kaplansky]
HeterogeneousRelations [section, in hrel]
_ \o _ (rel_scope) [notation, in hrel]
_ <=> _ (rel_scope) [notation, in hrel]
_ <= _ (rel_scope) [notation, in hrel]
homology [definition, in fpmod]
homology_dvd [lemma, in fpmod]
homology_alt_pres [definition, in fpmod]
horner_mx_diag_block [lemma, in mxstructure]
hrel [library]
hrespectful [definition, in hrel]
hrespectful_proper [instance, in hrel]
hrespectful_sub_proper [instance, in hrel]


I

idm [definition, in fpmod]
idm_iso [definition, in fpmod]
id_param [lemma, in refinements]
ImprovePivotQecSpec [constructor, in smith]
ImprovePivotRecSpec [constructor, in smithpid]
ImprovePivotSpec [constructor, in smith]
ImprovePivotSpec [constructor, in smithpid]
improve_pivotP [lemma, in smith]
improve_pivot_spec [inductive, in smith]
improve_pivot_recP [lemma, in smith]
improve_pivot_recR [definition, in smith]
improve_pivot_rec_spec [inductive, in smith]
improve_pivot [definition, in smith]
improve_pivot_rec [definition, in smith]
improve_pivotP [lemma, in smithpid]
improve_pivot_spec [inductive, in smithpid]
improve_pivot_recP [lemma, in smithpid]
improve_pivot_rec_spec [inductive, in smithpid]
improve_pivot [definition, in smithpid]
improve_pivot_rec [definition, in smithpid]
injm [definition, in fpmod]
inj_widen_ord [lemma, in minor]
inj_lift [lemma, in minor]
inj_strictf_ffun [lemma, in binetcauchy]
inj_strictf [lemma, in binetcauchy]
inj1 [definition, in fpmod]
inj1_proj1 [lemma, in fpmod]
inj1_proj2 [lemma, in fpmod]
inj1_mono [definition, in fpmod]
inj1_is_mono [lemma, in fpmod]
inj1_proof [lemma, in fpmod]
inj2 [definition, in fpmod]
inj2_proj2 [lemma, in fpmod]
inj2_proj1 [lemma, in fpmod]
inj2_mono [definition, in fpmod]
inj2_is_mono [lemma, in fpmod]
inj2_proof [lemma, in fpmod]
IntersectionCoherent [section, in coherent]
IntersectionCoherent.cap [variable, in coherent]
IntersectionCoherent.cap_spec [variable, in coherent]
IntersectionCoherent.dim_cap [variable, in coherent]
IntersectionCoherent.R [variable, in coherent]
IntSpec [constructor, in stronglydiscrete]
int_coherentType [definition, in coherent]
int_coherentMixin [definition, in coherent]
int_spec [inductive, in stronglydiscrete]
invmor [definition, in fpmod]
invmx_diag_block [lemma, in mxstructure]
invmx_block [lemma, in ssrcomplements]
inv_g_of_fx_inj [lemma, in binetcauchy]
inv_g_of_fxE [lemma, in binetcauchy]
inv_g_of_fx [definition, in binetcauchy]
irredr [definition, in dvdring]
irredrP [lemma, in dvdring]
irredr_primer [lemma, in dvdring]
irredr_coprimer [lemma, in dvdring]
irredr_dvd [lemma, in dvdring]
isom [definition, in fpmod]
isomorphism [definition, in fpmod]
Isomorphism [constructor, in fpmod]
isomorphisms [definition, in fpmod]
isomorphisms_idm [lemma, in fpmod]
isomorphism_of [record, in fpmod]
isoP [lemma, in fpmod]
IsoTheory [section, in fpmod]
IsoTheory.M [variable, in fpmod]
IsoTheory.N [variable, in fpmod]
IsoTheory.R [variable, in fpmod]
_ ^^-1 [notation, in fpmod]
iso_smithm [lemma, in fpmod]
iso_coker_eq0 [lemma, in fpmod]
iso_kernel_eq0 [lemma, in fpmod]
iso_of_isom [definition, in fpmod]
iso_of_me [definition, in fpmod]
iso_of_kc [definition, in fpmod]
is_triangular_mx [definition, in mxstructure]
is_coker [definition, in fpmod]
is_kernel [definition, in fpmod]
is_epi [definition, in fpmod]
is_mono [definition, in fpmod]


K

kaplansky [library]
Kaplansky_necc.c [variable, in kaplansky]
Kaplansky_necc.b [variable, in kaplansky]
Kaplansky_necc.a [variable, in kaplansky]
Kaplansky_necc.R [variable, in kaplansky]
Kaplansky_necc [section, in kaplansky]
Kaplansky_suff.kapP [variable, in kaplansky]
Kaplansky_suff.kap [variable, in kaplansky]
Kaplansky_suff.R [variable, in kaplansky]
Kaplansky_suff [section, in kaplansky]
kapP [lemma, in kaplansky]
kapW [definition, in kaplansky]
kapWP [lemma, in kaplansky]
kap_smithP [lemma, in kaplansky]
kap_smith [definition, in kaplansky]
ker [definition, in coherent]
kerAK [lemma, in coherent]
kerE [lemma, in coherent]
kerK [lemma, in coherent]
kermod [definition, in fpmod]
kermx [definition, in edr]
kermxP [lemma, in edr]
kernel [definition, in fpmod]
KernelAndCo [section, in fpmod]
KernelAndCo.M [variable, in fpmod]
KernelAndCo.N [variable, in fpmod]
KernelAndCo.phi [variable, in fpmod]
KernelAndCo.R [variable, in fpmod]
kernelK [lemma, in fpmod]
kernelP [lemma, in fpmod]
kernel_eq0 [lemma, in fpmod]
kerP [lemma, in coherent]
kerP_subproof [lemma, in coherent]
ker_c_intP [lemma, in coherent]
ker_c_int [definition, in coherent]
ker_cP [lemma, in coherent]
ker_c [definition, in coherent]
ker_col.ker_colP [variable, in coherent]
ker_col.ker_col [variable, in coherent]
ker_col.dim_ker_col [variable, in coherent]
ker_col.R [variable, in coherent]
ker_col [section, in coherent]
ker_mod1 [lemma, in coherent]
ker_modK [lemma, in coherent]
ker_mod [definition, in coherent]
ker1 [lemma, in coherent]
krull1EDRMixin [definition, in kaplansky]
krull1EDRType [definition, in kaplansky]
krull1_smithP [lemma, in kaplansky]
krull1_smith [definition, in kaplansky]
krull1_gdcoP [lemma, in kaplansky]
krull1_gdco [definition, in kaplansky]
krull1_adequate [lemma, in kaplansky]
krull1_factor [lemma, in kaplansky]


L

lcmr [definition, in dvdring]
lcmrA [lemma, in dvdring]
lcmrAC [lemma, in dvdring]
lcmrC [lemma, in dvdring]
lcmrCA [lemma, in dvdring]
lcmr_mulr [lemma, in dvdring]
lcmr_mull [lemma, in dvdring]
lcmr_mul2l [lemma, in dvdring]
lcmr_mul2r [lemma, in dvdring]
lcmr0 [lemma, in dvdring]
lcmr1 [lemma, in dvdring]
lcmsr [definition, in dvdring]
lcmsr_cons [lemma, in dvdring]
lcmsr0 [lemma, in dvdring]
lcm0r [lemma, in dvdring]
lcm1r [lemma, in dvdring]
left_mono [lemma, in fpmod]
leq_enorm [lemma, in dvdring]
lift [definition, in fpmod]
lifting [section, in minor]
lift_predS [lemma, in minor]
lift_pred0 [lemma, in minor]
lift_pred_widen_ord [lemma, in minor]
lift_pred [definition, in minor]
lift_mono [lemma, in fpmod]
lift_epi [lemma, in fpmod]
lift_subproof [lemma, in fpmod]
linv_surj [lemma, in fpmod]
lower_triangular_mxP [lemma, in mxstructure]
lower_triangular_mx [definition, in mxstructure]
lower_part_mx [definition, in mxstructure]
ltn_enorm [lemma, in dvdring]
lt_wf2 [lemma, in dvdring]


M

Matrix [section, in ssrcomplements]
matrix_of_morphism [projection, in fpmod]
Matrix.matrix_comUnitRingType.R [variable, in ssrcomplements]
Matrix.matrix_comUnitRingType [section, in ssrcomplements]
Matrix.matrix_ringType.R [variable, in ssrcomplements]
Matrix.matrix_ringType [section, in ssrcomplements]
Matrix.matrix_raw_type.T [variable, in ssrcomplements]
Matrix.matrix_raw_type [section, in ssrcomplements]
member [definition, in stronglydiscrete]
memberE [lemma, in stronglydiscrete]
memberP [lemma, in stronglydiscrete]
member_subid [lemma, in stronglydiscrete]
member_in [lemma, in stronglydiscrete]
member_specP [lemma, in stronglydiscrete]
member_spec [definition, in stronglydiscrete]
mem_same_codom [lemma, in binetcauchy]
minor [definition, in minor]
minor [library]
minorn [lemma, in minor]
minor_char_poly_mx.R [variable, in minor]
minor_char_poly_mx [section, in minor]
minor_lift_block [lemma, in minor]
minor_eq [lemma, in minor]
minor_g_not_injective [lemma, in minor]
minor_f_not_injective [lemma, in minor]
minor_alternate_g [lemma, in minor]
minor_alternate_f [lemma, in minor]
minor_ltn_eq0r [lemma, in minor]
minor_ltn_eq0l [lemma, in minor]
minor_theory.R [variable, in minor]
minor_theory [section, in minor]
minor_def.R [variable, in minor]
minor_def [section, in minor]
minor_eq0r [lemma, in edr]
minor_eq0l [lemma, in edr]
minor_diag_mx_seq [lemma, in edr]
minor1 [lemma, in minor]
minor2 [lemma, in minor]
modr [definition, in dvdring]
modr_spec [lemma, in dvdring]
modr_eq0 [lemma, in dvdring]
modr0 [lemma, in dvdring]
mod0r [lemma, in dvdring]
mono [lemma, in fpmod]
MonoEpi [section, in fpmod]
MonoEpi.M [variable, in fpmod]
MonoEpi.N [variable, in fpmod]
MonoEpi.R [variable, in fpmod]
monomorphism [definition, in fpmod]
Monomorphism [constructor, in fpmod]
monomorphism_of [record, in fpmod]
monoP [lemma, in fpmod]
MonoTheory [section, in fpmod]
MonoTheory.Mono1 [section, in fpmod]
MonoTheory.Mono1.M [variable, in fpmod]
MonoTheory.Mono1.n [variable, in fpmod]
MonoTheory.Mono1.N [variable, in fpmod]
MonoTheory.Mono1.X [variable, in fpmod]
MonoTheory.R [variable, in fpmod]
mono_ker [lemma, in fpmod]
mono_of_kernel [definition, in fpmod]
mono_of_iso [definition, in fpmod]
mono_of_mx [definition, in fpmod]
mono_of [definition, in fpmod]
Morphism [constructor, in fpmod]
morphismDef [section, in fpmod]
morphismDef.R [variable, in fpmod]
morphismProperties [section, in fpmod]
morphismProperties.M [variable, in fpmod]
morphismProperties.N [variable, in fpmod]
morphismProperties.phi [variable, in fpmod]
morphismProperties.R [variable, in fpmod]
morphismTheory [section, in fpmod]
morphismTheory.category [section, in fpmod]
morphismTheory.category.defs [section, in fpmod]
morphismTheory.category.defs.K [variable, in fpmod]
morphismTheory.category.defs.M [variable, in fpmod]
morphismTheory.category.defs.N [variable, in fpmod]
morphismTheory.category.theory [section, in fpmod]
morphismTheory.category.theory.M [variable, in fpmod]
morphismTheory.category.theory.N [variable, in fpmod]
morphismTheory.category.theory.P [variable, in fpmod]
morphismTheory.category.theory.Q [variable, in fpmod]
_ %= _ (mxpresentation_scope) [notation, in fpmod]
_ ** _ (mxpresentation_scope) [notation, in fpmod]
morphismTheory.equality [section, in fpmod]
morphismTheory.equality.M [variable, in fpmod]
morphismTheory.equality.N [variable, in fpmod]
morphismTheory.general [section, in fpmod]
morphismTheory.general.K [variable, in fpmod]
morphismTheory.general.M [variable, in fpmod]
morphismTheory.general.n [variable, in fpmod]
morphismTheory.general.N [variable, in fpmod]
morphismTheory.general.X [variable, in fpmod]
morphismTheory.R [variable, in fpmod]
morphismTheory.zmodType [section, in fpmod]
morphismTheory.zmodType.M [variable, in fpmod]
morphismTheory.zmodType.N [variable, in fpmod]
morphism_of_iso [projection, in fpmod]
morphism_of_epi [projection, in fpmod]
morphism_of_mono [projection, in fpmod]
morphism_zmodType [definition, in fpmod]
morphism_zmodMixin [definition, in fpmod]
morphism_choiceType [definition, in fpmod]
morphism_choiceMixin [definition, in fpmod]
morphism_eqType [definition, in fpmod]
morphism_eqMixin [definition, in fpmod]
morphism_subType [definition, in fpmod]
morphism_of [record, in fpmod]
Morphism1 [definition, in fpmod]
morphism1_subproof [lemma, in fpmod]
mor_of_mx_inj [lemma, in fpmod]
mor_of_mx [definition, in fpmod]
mor_of_mx_proof [lemma, in fpmod]
mulepi_eq0 [lemma, in fpmod]
mulid [definition, in stronglydiscrete]
mulidC [lemma, in stronglydiscrete]
mulid_congr [lemma, in stronglydiscrete]
mulid_addidr [lemma, in stronglydiscrete]
mulid0 [lemma, in stronglydiscrete]
mulkmor [lemma, in fpmod]
mulmono_eq0 [lemma, in fpmod]
mulmor [definition, in fpmod]
mulmorA [lemma, in fpmod]
mulmorBl [lemma, in fpmod]
mulmorBr [lemma, in fpmod]
mulmorc [lemma, in fpmod]
mulmorDl [lemma, in fpmod]
mulmorDr [lemma, in fpmod]
mulmorN [lemma, in fpmod]
mulmorV [lemma, in fpmod]
mulmor_proof [lemma, in fpmod]
mulmor0 [lemma, in fpmod]
mulmor1 [lemma, in fpmod]
mulmor11 [lemma, in fpmod]
mulmxKV_kermx [lemma, in edr]
mulmx_diag_block [lemma, in mxstructure]
mulmx_lsub [lemma, in ssrcomplements]
mulmx_rsub [lemma, in ssrcomplements]
mulmx_coker [lemma, in edr]
mulmx_diag_mx [lemma, in edr]
mulmx_ebase [lemma, in edr]
mulNmor [lemma, in fpmod]
mulr_lcml [lemma, in dvdring]
mulr_lcmr [lemma, in dvdring]
mulr_lcm_gcd [lemma, in dvdring]
mulr_gcdl [lemma, in dvdring]
mulr_gcdr [lemma, in dvdring]
mulVmor [lemma, in fpmod]
mul_diag_mx_seq_eq0 [lemma, in mxstructure]
mul_mx_diag_seq_min [lemma, in mxstructure]
mul_copid_mx_diag [lemma, in mxstructure]
mul_diag_mx_copid [lemma, in mxstructure]
mul_diag_mx_pid [lemma, in mxstructure]
mul_pid_mx_diag [lemma, in mxstructure]
mul_klift [lemma, in fpmod]
mul_lift [lemma, in fpmod]
mul_kermx [lemma, in edr]
mul0id [lemma, in stronglydiscrete]
mul0mor [lemma, in fpmod]
mul1mor [lemma, in fpmod]
mxrank [definition, in edr]
mxrank_leq_col [lemma, in edr]
mxrank_leq_row [lemma, in edr]
mxrank_leq_col_row [lemma, in edr]
mxrank0 [lemma, in edr]
mxstructure [library]
mxvec0 [lemma, in stronglydiscrete]
mx2 [definition, in kaplansky]
Mx2 [section, in kaplansky]
mx2_E11 [lemma, in kaplansky]
mx2_E10 [lemma, in kaplansky]
mx2_E01 [lemma, in kaplansky]
mx2_E00 [lemma, in kaplansky]
Mx2.R [variable, in kaplansky]


N

nbgen [projection, in fpmod]
nbrel [projection, in fpmod]
Notations [module, in dvdring]
_ %/? _ (ring_scope) [notation, in dvdring]
%/?%R (ring_scope) [notation, in dvdring]
_ %| _ (ring_scope) [notation, in dvdring]
%|%R (ring_scope) [notation, in dvdring]
_ %= _ (ring_scope) [notation, in dvdring]
%=R (ring_scope) [notation, in dvdring]
_ %<| _ [notation, in dvdring]
%<|R [notation, in dvdring]
nth_change_default [lemma, in binetcauchy]


O

odivr [definition, in dvdring]
odivrP [lemma, in dvdring]
odivrr [lemma, in dvdring]
odivr_some [lemma, in dvdring]
odivr_mul2r [lemma, in dvdring]
odivr_mul2l [lemma, in dvdring]
odivr_mulKr [lemma, in dvdring]
odivr_mulrK [lemma, in dvdring]
odivr0 [lemma, in dvdring]
odivr1 [lemma, in dvdring]
odiv0r [lemma, in dvdring]
ofun_hrel [definition, in hrel]
ohrel [definition, in refinements]
one_step [lemma, in binetcauchy]
oppmor [definition, in fpmod]
oppmor_proof [lemma, in fpmod]


P

param [record, in refinements]
param [inductive, in refinements]
paramE [lemma, in refinements]
Parametricity [section, in refinements]
paramP [lemma, in refinements]
paramR [lemma, in refinements]
param_eq_succ [instance, in refinements]
param_eq_zero [instance, in refinements]
param_nat [section, in refinements]
param_option [section, in refinements]
param_if [instance, in refinements]
param_seq [section, in refinements]
param_inr [instance, in refinements]
param_inl [instance, in refinements]
param_snd [instance, in refinements]
param_fst [instance, in refinements]
param_pair [instance, in refinements]
param_abstr2 [lemma, in refinements]
param_abstr [lemma, in refinements]
param_trans [lemma, in refinements]
param_id [lemma, in refinements]
param_apply [instance, in refinements]
param_proper [instance, in refinements]
param_sub_proper [instance, in refinements]
param_eq [lemma, in refinements]
param_rel [projection, in refinements]
param_rel [constructor, in refinements]
param_key [lemma, in refinements]
path_ordered_nth [lemma, in binetcauchy]
path_drop [lemma, in binetcauchy]
perm_fE [lemma, in binetcauchy]
perm_f [definition, in binetcauchy]
PID [module, in dvdring]
pidEDRMixin [definition, in smithpid]
pidEDRMixin [definition, in kaplansky]
pidEDRType [definition, in smithpid]
pidEDRType [definition, in kaplansky]
PIDTheory [section, in dvdring]
PIDTheory.R [variable, in dvdring]
pid_smithP [lemma, in kaplansky]
pid_smith [definition, in kaplansky]
pid_gdco [lemma, in kaplansky]
PID.base [projection, in dvdring]
PID.bezoutDomainType [definition, in dvdring]
PID.choiceType [definition, in dvdring]
PID.class [definition, in dvdring]
PID.Class [constructor, in dvdring]
PID.ClassDef [section, in dvdring]
PID.ClassDef.cT [variable, in dvdring]
PID.ClassDef.T [variable, in dvdring]
PID.class_of [record, in dvdring]
PID.clone [definition, in dvdring]
PID.comRingType [definition, in dvdring]
PID.comUnitRingType [definition, in dvdring]
PID.dvdRingType [definition, in dvdring]
PID.eqType [definition, in dvdring]
PID.Exports [module, in dvdring]
PID.Exports.PIDMixin [abbreviation, in dvdring]
PID.Exports.PIDType [abbreviation, in dvdring]
PID.Exports.pidType [abbreviation, in dvdring]
[ pidType of _ ] (form_scope) [notation, in dvdring]
[ pidType of _ for _ ] (form_scope) [notation, in dvdring]
PID.gcdDomainType [definition, in dvdring]
PID.idomainType [definition, in dvdring]
PID.mixin [projection, in dvdring]
PID.Mixin [constructor, in dvdring]
PID.mixin_of [record, in dvdring]
PID.pack [definition, in dvdring]
PID.Pack [constructor, in dvdring]
PID.ringType [definition, in dvdring]
PID.sort [projection, in dvdring]
PID.type [record, in dvdring]
PID.unitRingType [definition, in dvdring]
PID.zmodType [definition, in dvdring]
pminor [definition, in minor]
pminor_char_poly_mx_monic [lemma, in minor]
Poly [section, in ssrcomplements]
Poly.R [variable, in ssrcomplements]
pres [projection, in fpmod]
primer [definition, in dvdring]
principal [definition, in dvdring]
principal_w2_correct [lemma, in dvdring]
principal_w2 [definition, in dvdring]
principal_w1_correct [lemma, in dvdring]
principal_w1 [definition, in dvdring]
principal_gen_dvd [lemma, in dvdring]
principal_gen [definition, in dvdring]
prod [section, in refinements]
prod_hrel [definition, in refinements]
prod_seq_count [lemma, in ssrcomplements]
prod_minor_seq [lemma, in edr]
proj1 [definition, in fpmod]
proj1_epi [definition, in fpmod]
proj1_is_epi [lemma, in fpmod]
proj1_proof [lemma, in fpmod]
proj2 [definition, in fpmod]
proj2_epi [definition, in fpmod]
proj2_is_epi [lemma, in fpmod]
proj2_proof [definition, in fpmod]


Q

quot_by [definition, in fpmod]


R

Refinements [module, in refinements]
refinements [library]
Refinements.Op [module, in refinements]
Refinements.Op.add [record, in refinements]
Refinements.Op.add [inductive, in refinements]
Refinements.Op.add_op [projection, in refinements]
Refinements.Op.add_op [constructor, in refinements]
Refinements.Op.block [record, in refinements]
Refinements.Op.block [inductive, in refinements]
Refinements.Op.block_mx [projection, in refinements]
Refinements.Op.block_mx [constructor, in refinements]
Refinements.Op.castmx [projection, in refinements]
Refinements.Op.castmx [constructor, in refinements]
Refinements.Op.cast_op [projection, in refinements]
Refinements.Op.cast_class [record, in refinements]
Refinements.Op.cast_op [constructor, in refinements]
Refinements.Op.cast_class [inductive, in refinements]
Refinements.Op.col [projection, in refinements]
Refinements.Op.col [constructor, in refinements]
Refinements.Op.col_perm [projection, in refinements]
Refinements.Op.col_perm_class [record, in refinements]
Refinements.Op.col_perm [constructor, in refinements]
Refinements.Op.col_perm_class [inductive, in refinements]
Refinements.Op.col_class [record, in refinements]
Refinements.Op.col_class [inductive, in refinements]
Refinements.Op.col_mx [projection, in refinements]
Refinements.Op.col_mx_class [record, in refinements]
Refinements.Op.col_mx [constructor, in refinements]
Refinements.Op.col_mx_class [inductive, in refinements]
Refinements.Op.col' [projection, in refinements]
Refinements.Op.col' [constructor, in refinements]
Refinements.Op.col'_class [record, in refinements]
Refinements.Op.col'_class [inductive, in refinements]
Refinements.Op.const_mx [projection, in refinements]
Refinements.Op.const_mx_class [record, in refinements]
Refinements.Op.const_mx [constructor, in refinements]
Refinements.Op.const_mx_class [inductive, in refinements]
Refinements.Op.div [record, in refinements]
Refinements.Op.div [inductive, in refinements]
Refinements.Op.div_op [projection, in refinements]
Refinements.Op.div_op [constructor, in refinements]
Refinements.Op.dlsub [record, in refinements]
Refinements.Op.dlsub [inductive, in refinements]
Refinements.Op.dlsubmx [projection, in refinements]
Refinements.Op.dlsubmx [constructor, in refinements]
Refinements.Op.drsub [record, in refinements]
Refinements.Op.drsub [inductive, in refinements]
Refinements.Op.drsubmx [projection, in refinements]
Refinements.Op.drsubmx [constructor, in refinements]
Refinements.Op.dsub [record, in refinements]
Refinements.Op.dsub [inductive, in refinements]
Refinements.Op.dsubmx [projection, in refinements]
Refinements.Op.dsubmx [constructor, in refinements]
Refinements.Op.dvd [record, in refinements]
Refinements.Op.dvd [inductive, in refinements]
Refinements.Op.dvd_op [projection, in refinements]
Refinements.Op.dvd_op [constructor, in refinements]
Refinements.Op.enorm_op [projection, in refinements]
Refinements.Op.enorm_of [record, in refinements]
Refinements.Op.enorm_op [constructor, in refinements]
Refinements.Op.enorm_of [inductive, in refinements]
Refinements.Op.eq [record, in refinements]
Refinements.Op.eq [inductive, in refinements]
Refinements.Op.eq_op [projection, in refinements]
Refinements.Op.eq_op [constructor, in refinements]
Refinements.Op.exp [record, in refinements]
Refinements.Op.exp [inductive, in refinements]
Refinements.Op.exp_op [projection, in refinements]
Refinements.Op.exp_op [constructor, in refinements]
Refinements.Op.find_pivot [projection, in refinements]
Refinements.Op.find_pivot_class [record, in refinements]
Refinements.Op.find_pivot [constructor, in refinements]
Refinements.Op.find_pivot_class [inductive, in refinements]
Refinements.Op.fun_of_matrix [projection, in refinements]
Refinements.Op.fun_of [record, in refinements]
Refinements.Op.fun_of_matrix [constructor, in refinements]
Refinements.Op.fun_of [inductive, in refinements]
Refinements.Op.hadd [record, in refinements]
Refinements.Op.hadd [inductive, in refinements]
Refinements.Op.hadd_op [projection, in refinements]
Refinements.Op.hadd_op [constructor, in refinements]
Refinements.Op.hcast [record, in refinements]
Refinements.Op.hcast [inductive, in refinements]
Refinements.Op.heq [record, in refinements]
Refinements.Op.heq [inductive, in refinements]
Refinements.Op.heq_op [projection, in refinements]
Refinements.Op.heq_op [constructor, in refinements]
Refinements.Op.hinv [record, in refinements]
Refinements.Op.hinv [inductive, in refinements]
Refinements.Op.hinv_op [projection, in refinements]
Refinements.Op.hinv_op [constructor, in refinements]
Refinements.Op.hmul [record, in refinements]
Refinements.Op.hmul [inductive, in refinements]
Refinements.Op.hmul_op [projection, in refinements]
Refinements.Op.hmul_op [constructor, in refinements]
Refinements.Op.hone [record, in refinements]
Refinements.Op.hone [inductive, in refinements]
Refinements.Op.hone_op [projection, in refinements]
Refinements.Op.hone_op [constructor, in refinements]
Refinements.Op.hopp [record, in refinements]
Refinements.Op.hopp [inductive, in refinements]
Refinements.Op.hopp_op [projection, in refinements]
Refinements.Op.hopp_op [constructor, in refinements]
Refinements.Op.hscale [record, in refinements]
Refinements.Op.hscale [inductive, in refinements]
Refinements.Op.hscale_op [projection, in refinements]
Refinements.Op.hscale_op [constructor, in refinements]
Refinements.Op.hsub [record, in refinements]
Refinements.Op.hsub [inductive, in refinements]
Refinements.Op.hsub_op [projection, in refinements]
Refinements.Op.hsub_op [constructor, in refinements]
Refinements.Op.hzero [record, in refinements]
Refinements.Op.hzero [inductive, in refinements]
Refinements.Op.hzero_op [projection, in refinements]
Refinements.Op.hzero_op [constructor, in refinements]
Refinements.Op.id_cast [instance, in refinements]
Refinements.Op.implem [projection, in refinements]
Refinements.Op.implem [constructor, in refinements]
Refinements.Op.implem_id [definition, in refinements]
Refinements.Op.implem_of [record, in refinements]
Refinements.Op.implem_of [inductive, in refinements]
Refinements.Op.inv [record, in refinements]
Refinements.Op.inv [inductive, in refinements]
Refinements.Op.inv_op [projection, in refinements]
Refinements.Op.inv_op [constructor, in refinements]
Refinements.Op.leq [record, in refinements]
Refinements.Op.leq [inductive, in refinements]
Refinements.Op.leq_op [projection, in refinements]
Refinements.Op.leq_op [constructor, in refinements]
Refinements.Op.lift0 [projection, in refinements]
Refinements.Op.lift0 [constructor, in refinements]
Refinements.Op.lift0mx_class [record, in refinements]
Refinements.Op.lift0mx_class [inductive, in refinements]
Refinements.Op.lift0_perm [projection, in refinements]
Refinements.Op.lift0_perm_class [record, in refinements]
Refinements.Op.lift0_perm [constructor, in refinements]
Refinements.Op.lift0_perm_class [inductive, in refinements]
Refinements.Op.lift0_mx [projection, in refinements]
Refinements.Op.lift0_mx [constructor, in refinements]
Refinements.Op.lift0_class [record, in refinements]
Refinements.Op.lift0_class [inductive, in refinements]
Refinements.Op.lsub [record, in refinements]
Refinements.Op.lsub [inductive, in refinements]
Refinements.Op.lsubmx [projection, in refinements]
Refinements.Op.lsubmx [constructor, in refinements]
Refinements.Op.lt [record, in refinements]
Refinements.Op.lt [inductive, in refinements]
Refinements.Op.lt_op [projection, in refinements]
Refinements.Op.lt_op [constructor, in refinements]
Refinements.Op.map_mx [projection, in refinements]
Refinements.Op.map_mx_class [record, in refinements]
Refinements.Op.map_mx [constructor, in refinements]
Refinements.Op.map_mx_class [inductive, in refinements]
Refinements.Op.mul [record, in refinements]
Refinements.Op.mul [inductive, in refinements]
Refinements.Op.mul_op [projection, in refinements]
Refinements.Op.mul_op [constructor, in refinements]
Refinements.Op.odvd [record, in refinements]
Refinements.Op.odvd [inductive, in refinements]
Refinements.Op.odvd_op [projection, in refinements]
Refinements.Op.odvd_op [constructor, in refinements]
Refinements.Op.one [record, in refinements]
Refinements.Op.one [inductive, in refinements]
Refinements.Op.one_op [projection, in refinements]
Refinements.Op.one_op [constructor, in refinements]
Refinements.Op.opp [record, in refinements]
Refinements.Op.opp [inductive, in refinements]
Refinements.Op.opp_op [projection, in refinements]
Refinements.Op.opp_op [constructor, in refinements]
Refinements.Op.row [projection, in refinements]
Refinements.Op.row [constructor, in refinements]
Refinements.Op.row_perm [projection, in refinements]
Refinements.Op.row_perm_class [record, in refinements]
Refinements.Op.row_perm [constructor, in refinements]
Refinements.Op.row_perm_class [inductive, in refinements]
Refinements.Op.row_class [record, in refinements]
Refinements.Op.row_class [inductive, in refinements]
Refinements.Op.row_mx [projection, in refinements]
Refinements.Op.row_mx_class [record, in refinements]
Refinements.Op.row_mx [constructor, in refinements]
Refinements.Op.row_mx_class [inductive, in refinements]
Refinements.Op.row' [projection, in refinements]
Refinements.Op.row' [constructor, in refinements]
Refinements.Op.row'_class [record, in refinements]
Refinements.Op.row'_class [inductive, in refinements]
Refinements.Op.rsub [record, in refinements]
Refinements.Op.rsub [inductive, in refinements]
Refinements.Op.rsubmx [projection, in refinements]
Refinements.Op.rsubmx [constructor, in refinements]
Refinements.Op.scalar_mx [projection, in refinements]
Refinements.Op.scalar_mx_class [record, in refinements]
Refinements.Op.scalar_mx [constructor, in refinements]
Refinements.Op.scalar_mx_class [inductive, in refinements]
Refinements.Op.scale [record, in refinements]
Refinements.Op.scale [inductive, in refinements]
Refinements.Op.scale_op [projection, in refinements]
Refinements.Op.scale_op [constructor, in refinements]
Refinements.Op.spec [projection, in refinements]
Refinements.Op.spec [constructor, in refinements]
Refinements.Op.spec_id [definition, in refinements]
Refinements.Op.spec_of [record, in refinements]
Refinements.Op.spec_of [inductive, in refinements]
Refinements.Op.sub [record, in refinements]
Refinements.Op.sub [inductive, in refinements]
Refinements.Op.sub_op [projection, in refinements]
Refinements.Op.sub_op [constructor, in refinements]
Refinements.Op.tperm [projection, in refinements]
Refinements.Op.tperm [constructor, in refinements]
Refinements.Op.tperm_class [record, in refinements]
Refinements.Op.tperm_class [inductive, in refinements]
Refinements.Op.transpose_op [projection, in refinements]
Refinements.Op.transpose_class [record, in refinements]
Refinements.Op.transpose_op [constructor, in refinements]
Refinements.Op.transpose_class [inductive, in refinements]
Refinements.Op.ulsub [record, in refinements]
Refinements.Op.ulsub [inductive, in refinements]
Refinements.Op.ulsubmx [projection, in refinements]
Refinements.Op.ulsubmx [constructor, in refinements]
Refinements.Op.ursub [record, in refinements]
Refinements.Op.ursub [inductive, in refinements]
Refinements.Op.ursubmx [projection, in refinements]
Refinements.Op.ursubmx [constructor, in refinements]
Refinements.Op.usub [record, in refinements]
Refinements.Op.usub [inductive, in refinements]
Refinements.Op.usubmx [projection, in refinements]
Refinements.Op.usubmx [constructor, in refinements]
Refinements.Op.xcol [projection, in refinements]
Refinements.Op.xcol [constructor, in refinements]
Refinements.Op.xcol_class [record, in refinements]
Refinements.Op.xcol_class [inductive, in refinements]
Refinements.Op.xrow [projection, in refinements]
Refinements.Op.xrow [constructor, in refinements]
Refinements.Op.xrow_class [record, in refinements]
Refinements.Op.xrow_class [inductive, in refinements]
Refinements.Op.zero [record, in refinements]
Refinements.Op.zero [inductive, in refinements]
Refinements.Op.zero_op [projection, in refinements]
Refinements.Op.zero_op [constructor, in refinements]
_ %| _ (computable_scope) [notation, in refinements]
_ <= _ (computable_scope) [notation, in refinements]
_ < _ (computable_scope) [notation, in refinements]
_ == _ (computable_scope) [notation, in refinements]
_ %/? _ (computable_scope) [notation, in refinements]
_ / _ (computable_scope) [notation, in refinements]
_ *: _ (computable_scope) [notation, in refinements]
_ * _ (computable_scope) [notation, in refinements]
_ ^ _ (computable_scope) [notation, in refinements]
_ - _ (computable_scope) [notation, in refinements]
_ + _ (computable_scope) [notation, in refinements]
_ ^-1 (computable_scope) [notation, in refinements]
- _ (computable_scope) [notation, in refinements]
1 (computable_scope) [notation, in refinements]
0 (computable_scope) [notation, in refinements]
_ ^T (hetero_computable_scope) [notation, in refinements]
_ == _ (hetero_computable_scope) [notation, in refinements]
_ *: _ (hetero_computable_scope) [notation, in refinements]
_ *m _ (hetero_computable_scope) [notation, in refinements]
_ ^-1 (hetero_computable_scope) [notation, in refinements]
_ - _ (hetero_computable_scope) [notation, in refinements]
- _ (hetero_computable_scope) [notation, in refinements]
_ + _ (hetero_computable_scope) [notation, in refinements]
1 (hetero_computable_scope) [notation, in refinements]
0 (hetero_computable_scope) [notation, in refinements]
*m%HC [notation, in refinements]
*%C [notation, in refinements]
*:%C [notation, in refinements]
*:%HC [notation, in refinements]
+%C [notation, in refinements]
+%HC [notation, in refinements]
-%C [notation, in refinements]
-%HC [notation, in refinements]
==%HC [notation, in refinements]
reindex_with_tilt [lemma, in binetcauchy]
right_epi [lemma, in fpmod]
rinv_inj [lemma, in fpmod]
row_id_mulmx [lemma, in ssrcomplements]
row_thin_mx [lemma, in ssrcomplements]
row_ebase_unit [lemma, in edr]
row_ebase [definition, in edr]
row'_col'_triangular_mx [lemma, in mxstructure]
row'_col'_char_poly_mx [lemma, in ssrcomplements]
RPdiv [module, in similar]
RPdiv [module, in ssrcomplements]
RPdiv.add_id [lemma, in similar]
RPdiv.add_id [lemma, in ssrcomplements]
RPdiv.expr_rev [lemma, in similar]
RPdiv.expr_rev [lemma, in ssrcomplements]
RPdiv.id_converse [definition, in similar]
RPdiv.id_converse_def [definition, in similar]
RPdiv.id_converse [definition, in ssrcomplements]
RPdiv.id_converse_def [definition, in ssrcomplements]
RPdiv.ltn_rmodp_l [lemma, in similar]
RPdiv.ltn_rmodp_l [lemma, in ssrcomplements]
RPdiv.mon [module, in similar]
RPdiv.mon [module, in ssrcomplements]
RPdiv.monic_map_inj [lemma, in similar]
RPdiv.monic_map_inj [lemma, in ssrcomplements]
RPdiv.mon.MonicDivisor [section, in similar]
RPdiv.mon.MonicDivisor [section, in ssrcomplements]
RPdiv.mon.MonicDivisor.d [variable, in similar]
RPdiv.mon.MonicDivisor.d [variable, in ssrcomplements]
RPdiv.mon.MonicDivisor.mond [variable, in similar]
RPdiv.mon.MonicDivisor.mond [variable, in ssrcomplements]
RPdiv.mon.MonicDivisor.R [variable, in similar]
RPdiv.mon.MonicDivisor.R [variable, in ssrcomplements]
RPdiv.mon.rdivp_l_eq [lemma, in similar]
RPdiv.mon.rdivp_l_eq [lemma, in ssrcomplements]
RPdiv.phi [definition, in similar]
RPdiv.phi [definition, in ssrcomplements]
RPdiv.phiK [lemma, in similar]
RPdiv.phiK [lemma, in ssrcomplements]
RPdiv.phi_bij [lemma, in similar]
RPdiv.phi_invK [lemma, in similar]
RPdiv.phi_inv [definition, in similar]
RPdiv.phi_rmorphism [definition, in similar]
RPdiv.phi_is_rmorphism [lemma, in similar]
RPdiv.phi_bij [lemma, in ssrcomplements]
RPdiv.phi_invK [lemma, in ssrcomplements]
RPdiv.phi_inv [definition, in ssrcomplements]
RPdiv.phi_rmorphism [definition, in ssrcomplements]
RPdiv.phi_is_rmorphism [lemma, in ssrcomplements]
RPdiv.rdivp_l [definition, in similar]
RPdiv.rdivp_l [definition, in ssrcomplements]
RPdiv.rdvdp_l [definition, in similar]
RPdiv.rdvdp_l [definition, in ssrcomplements]
RPdiv.redivp_l [definition, in similar]
RPdiv.redivp_l [definition, in ssrcomplements]
RPdiv.RingPseudoDivision [section, in similar]
RPdiv.RingPseudoDivision [section, in ssrcomplements]
RPdiv.RingPseudoDivision.R [variable, in similar]
RPdiv.RingPseudoDivision.R [variable, in ssrcomplements]
RPdiv.rmodp_l [definition, in similar]
RPdiv.rmodp_l [definition, in ssrcomplements]
RPdiv.rmultp_l [definition, in similar]
RPdiv.rmultp_l [definition, in ssrcomplements]
RPdiv.rscalp_l [definition, in similar]
RPdiv.rscalp_l [definition, in ssrcomplements]


S

same_codomP [lemma, in binetcauchy]
same_codom [definition, in binetcauchy]
same_codomb [definition, in binetcauchy]
scalar_diag_block_mx [lemma, in mxstructure]
scale_mulidr [lemma, in stronglydiscrete]
scale_trmx [lemma, in stronglydiscrete]
scale_mxvec [lemma, in stronglydiscrete]
scale_addid [lemma, in stronglydiscrete]
sdvdr [definition, in dvdring]
sdvdrNW [lemma, in dvdring]
sdvdrW [lemma, in dvdring]
sdvdr_ind [definition, in dvdring]
sdvdr_rec [definition, in dvdring]
sdvdr_rect [definition, in dvdring]
sdvdr_wf [lemma, in dvdring]
sdvdr_def [lemma, in dvdring]
sdvdr0 [lemma, in dvdring]
sdvd_Bezout_step2 [lemma, in smithpid]
sdvd_Bezout_step [lemma, in dvdring]
sdvd0r [lemma, in dvdring]
Seq [section, in ssrcomplements]
Seqeqtype [section, in ssrcomplements]
Seqeqtype.leT [variable, in ssrcomplements]
Seqeqtype.leT_tr [variable, in ssrcomplements]
Seqeqtype.T [variable, in ssrcomplements]
seq_hrel [definition, in refinements]
Seq.f [variable, in ssrcomplements]
Seq.T1 [variable, in ssrcomplements]
Seq.T2 [variable, in ssrcomplements]
Seq.T3 [variable, in ssrcomplements]
seq2_ind [lemma, in similar]
seq2_ind [lemma, in ssrcomplements]
set_param [lemma, in refinements]
sign_tilt2 [lemma, in binetcauchy]
sig_tilt [lemma, in binetcauchy]
similar [definition, in similar]
similar [library]
SimilarDef [section, in similar]
SimilarDef.R [variable, in similar]
similar_char_poly [lemma, in similar]
similar_mxminpoly [lemma, in similar]
similar_fundamental [lemma, in similar]
similar_equiv [lemma, in similar]
similar_diag_block [lemma, in similar]
similar_horner [lemma, in similar]
similar_poly [lemma, in similar]
similar_exp [lemma, in similar]
similar_dgblockmx [lemma, in similar]
similar_drblockmx [lemma, in similar]
similar_ulblockmx [lemma, in similar]
similar_diag_mx_seq [lemma, in similar]
similar_cast [lemma, in similar]
similar_det [lemma, in similar]
similar_refl [lemma, in similar]
similar_trans [lemma, in similar]
similar_sym [lemma, in similar]
similar0 [lemma, in similar]
simplmx [variable, in kaplansky]
size_tool [lemma, in minor]
size_Smith [lemma, in smith]
size_sum_big [lemma, in mxstructure]
size_sum_big_cons [lemma, in mxstructure]
size_sum [definition, in mxstructure]
size_sum_rec [definition, in mxstructure]
size_Smith [lemma, in smithpid]
Smith [definition, in smith]
Smith [definition, in smithpid]
smith [definition, in edr]
smith [library]
smithm [definition, in fpmod]
smithmxn [definition, in kaplansky]
smithmxnP [lemma, in kaplansky]
smithmxn_recP [lemma, in kaplansky]
smithmxn_rec [definition, in kaplansky]
smithm_inv [definition, in fpmod]
SmithP [lemma, in smith]
SmithP [lemma, in smithpid]
smithP [lemma, in edr]
smithpid [library]
smith_theory.find_pivotP [variable, in smith]
smith_theory.find2P [variable, in smith]
smith_theory.find1P [variable, in smith]
smith_theory.find_pivot [variable, in smith]
smith_theory.find2 [variable, in smith]
smith_theory.find1 [variable, in smith]
'M_ _ (type_scope) [notation, in smith]
'M_ ( _ ) (type_scope) [notation, in smith]
'M_ ( _ , _ ) (type_scope) [notation, in smith]
smith_theory.E [variable, in smith]
smith_theory [section, in smith]
smith_def.Bezout_step [variable, in smith]
smith_def.find_pivot [variable, in smith]
smith_def.find2 [variable, in smith]
smith_def.find1 [variable, in smith]
'I_ _ (type_scope) [notation, in smith]
'M[A]_ ( _ ) [notation, in smith]
'M[A]_ ( _ , _ ) [notation, in smith]
smith_def.ordA [variable, in smith]
smith_def.mxA [variable, in smith]
smith_def.A [variable, in smith]
smith_def [section, in smith]
smith_def.find_pivotP [variable, in smithpid]
smith_def.find_pivot [variable, in smithpid]
smith_def.find2P [variable, in smithpid]
smith_def.find1P [variable, in smithpid]
smith_def.find2 [variable, in smithpid]
smith_def.find1 [variable, in smithpid]
smith_def.R [variable, in smithpid]
smith_def [section, in smithpid]
smith_iso [definition, in fpmod]
smith_inv_subproof [lemma, in fpmod]
smith_subproof [lemma, in fpmod]
smith_fpmod.Q [variable, in fpmod]
smith_fpmod.P [variable, in fpmod]
smith_fpmod.D [variable, in fpmod]
smith_fpmod.M [variable, in fpmod]
smith_fpmod.R [variable, in fpmod]
smith_fpmod [section, in fpmod]
Smith_unicity [lemma, in edr]
Smith_gcdr_spec [lemma, in edr]
smith_seq [definition, in edr]
smith_spec [definition, in edr]
smith1xn [definition, in kaplansky]
smith1xnP [lemma, in kaplansky]
smith2xn [definition, in kaplansky]
smith2xnP [lemma, in kaplansky]
Smith2x2 [section, in kaplansky]
Smith2x2_correctness.smith2x2P [variable, in kaplansky]
Smith2x2_correctness.smith2x2 [variable, in kaplansky]
Smith2x2_correctness.R [variable, in kaplansky]
Smith2x2_correctness [section, in kaplansky]
Smith2x2.R [variable, in kaplansky]
Smith2x2.smith2x2 [variable, in kaplansky]
sorted_nth0 [lemma, in dvdring]
sorted_cons [lemma, in dvdring]
sorted_dvd0r [lemma, in dvdring]
sorted_take [lemma, in ssrcomplements]
sorted_drop [lemma, in ssrcomplements]
sorted_ordered_nth_gen [lemma, in binetcauchy]
sorted_ordered_nth [lemma, in binetcauchy]
sorted_enum [lemma, in binetcauchy]
source [definition, in fpmod]
source_of_mx [definition, in fpmod]
split_andb [lemma, in fpmod]
split_sumZ_fs [lemma, in binetcauchy]
split_sumZ_sf [lemma, in binetcauchy]
SquareTriangular [section, in mxstructure]
SquareTriangular.R [variable, in mxstructure]
SquareTriangular2 [section, in mxstructure]
SquareTriangular2.R [variable, in mxstructure]
ssrcomplements [library]
step_weight [lemma, in binetcauchy]
strictf [definition, in binetcauchy]
strictf_uniq [lemma, in binetcauchy]
strictf_lift [lemma, in binetcauchy]
strict_from_fP [lemma, in binetcauchy]
strict_from_f [definition, in binetcauchy]
strict_fromP [lemma, in binetcauchy]
strict_from [definition, in binetcauchy]
StronglyDiscrete [module, in stronglydiscrete]
stronglydiscrete [library]
stronglyDiscreteMixin [definition, in edr]
StronglyDiscreteTheory [section, in stronglydiscrete]
StronglyDiscreteTheory.IdealTheory [section, in stronglydiscrete]
StronglyDiscreteTheory.IdealTheory.IdealIntersection [section, in stronglydiscrete]
StronglyDiscreteTheory.IdealTheory.IdealIntersection.cap_size [variable, in stronglydiscrete]
_ :=: _ (ideal_scope) [notation, in stronglydiscrete]
_ == _ (ideal_scope) [notation, in stronglydiscrete]
_ <= _ <= _ (ideal_scope) [notation, in stronglydiscrete]
_ <= _ (ideal_scope) [notation, in stronglydiscrete]
_ *i _ [notation, in stronglydiscrete]
_ +i _ [notation, in stronglydiscrete]
StronglyDiscreteTheory.R [variable, in stronglydiscrete]
stronglyDiscreteType [definition, in edr]
StronglyDiscrete.base [projection, in stronglydiscrete]
StronglyDiscrete.choiceType [definition, in stronglydiscrete]
StronglyDiscrete.class [definition, in stronglydiscrete]
StronglyDiscrete.Class [constructor, in stronglydiscrete]
StronglyDiscrete.ClassDef [section, in stronglydiscrete]
StronglyDiscrete.ClassDef.cT [variable, in stronglydiscrete]
StronglyDiscrete.ClassDef.T [variable, in stronglydiscrete]
StronglyDiscrete.class_of [record, in stronglydiscrete]
StronglyDiscrete.clone [definition, in stronglydiscrete]
StronglyDiscrete.comRingType [definition, in stronglydiscrete]
StronglyDiscrete.comUnitRingType [definition, in stronglydiscrete]
StronglyDiscrete.eqType [definition, in stronglydiscrete]
StronglyDiscrete.Exports [module, in stronglydiscrete]
StronglyDiscrete.Exports.StronglyDiscreteMixin [abbreviation, in stronglydiscrete]
StronglyDiscrete.Exports.StronglyDiscreteType [abbreviation, in stronglydiscrete]
StronglyDiscrete.Exports.stronglyDiscreteType [abbreviation, in stronglydiscrete]
[ stronglyDiscreteType of _ ] (form_scope) [notation, in stronglydiscrete]
[ stronglyDiscreteType of _ for _ ] (form_scope) [notation, in stronglydiscrete]
StronglyDiscrete.idomainType [definition, in stronglydiscrete]
StronglyDiscrete.member [projection, in stronglydiscrete]
StronglyDiscrete.Member [constructor, in stronglydiscrete]
StronglyDiscrete.member_spec [inductive, in stronglydiscrete]
StronglyDiscrete.mixin [projection, in stronglydiscrete]
StronglyDiscrete.Mixin [constructor, in stronglydiscrete]
StronglyDiscrete.mixin_of [record, in stronglydiscrete]
StronglyDiscrete.NMember [constructor, in stronglydiscrete]
StronglyDiscrete.pack [definition, in stronglydiscrete]
StronglyDiscrete.Pack [constructor, in stronglydiscrete]
StronglyDiscrete.ringType [definition, in stronglydiscrete]
StronglyDiscrete.sort [projection, in stronglydiscrete]
StronglyDiscrete.type [record, in stronglydiscrete]
StronglyDiscrete.unitRingType [definition, in stronglydiscrete]
StronglyDiscrete.zmodType [definition, in stronglydiscrete]
subeqid_refl [lemma, in stronglydiscrete]
subid [definition, in stronglydiscrete]
subidMl [lemma, in stronglydiscrete]
subidP [lemma, in stronglydiscrete]
subid_mulid_congr [lemma, in stronglydiscrete]
subid_mulC [lemma, in stronglydiscrete]
subid_tr_mxvec [lemma, in stronglydiscrete]
subid_scaleid [lemma, in stronglydiscrete]
subid_addid_congr [lemma, in stronglydiscrete]
subid_addAr [lemma, in stronglydiscrete]
subid_addAl [lemma, in stronglydiscrete]
subid_addC [lemma, in stronglydiscrete]
subid_castmxr [lemma, in stronglydiscrete]
subid_castmxl [lemma, in stronglydiscrete]
subid_memberP [lemma, in stronglydiscrete]
subid_le0 [lemma, in stronglydiscrete]
subid_trans [lemma, in stronglydiscrete]
subid_refl [lemma, in stronglydiscrete]
subid_colP [lemma, in stronglydiscrete]
subid1 [lemma, in stronglydiscrete]
submatrix [definition, in minor]
submatrix_char_poly_mx [lemma, in minor]
submatrix_char_poly_mx.R [variable, in minor]
submatrix_char_poly_mx [section, in minor]
submatrix_scalar_mx [lemma, in minor]
submatrix_mul [lemma, in minor]
submatrix_sub [lemma, in minor]
submatrix_opp [lemma, in minor]
submatrix_add [lemma, in minor]
submatrix_scale [lemma, in minor]
submatrix_lift_block [lemma, in minor]
submatrix_eq [lemma, in minor]
submatrix_theory.R [variable, in minor]
submatrix_theory [section, in minor]
submatrix_map_mx [lemma, in minor]
submatrix_def.B [variable, in minor]
submatrix_def.A [variable, in minor]
submatrix_def [section, in minor]
submatrix0 [lemma, in minor]
subrid [lemma, in stronglydiscrete]
sub_submatrix [lemma, in minor]
sub_hresp_comp [lemma, in hrel]
sub_hrel_partial_order [instance, in hrel]
sub_hrel_proper [instance, in hrel]
sub_hrel_partialorder [instance, in hrel]
sub_eql [lemma, in hrel]
sub_Truer [lemma, in hrel]
sub_Falsel [lemma, in hrel]
sub_hrel [definition, in hrel]
sub_kermxP [lemma, in coherent]
sub_mulidr [lemma, in stronglydiscrete]
sub_mulidl [lemma, in stronglydiscrete]
sub_addidr [lemma, in stronglydiscrete]
sub_addidl [lemma, in stronglydiscrete]
sub_addid0l [lemma, in stronglydiscrete]
sub_add0lid [lemma, in stronglydiscrete]
sub_addid0r [lemma, in stronglydiscrete]
sub_add0rid [lemma, in stronglydiscrete]
sub0id [lemma, in stronglydiscrete]
sum [section, in refinements]
sum_elim [definition, in refinements]
sum_hrel [definition, in refinements]
sum_bad [lemma, in binetcauchy]
surgery [lemma, in kaplansky]
surgery2 [lemma, in kaplansky]
surjm [definition, in fpmod]


T

target [definition, in fpmod]
theory [section, in fpmod]
theory.dsum [section, in fpmod]
theory.dsum.M [variable, in fpmod]
theory.dsum.N [variable, in fpmod]
theory.homology [section, in fpmod]
theory.homology.M [variable, in fpmod]
theory.homology.mul_phi_psi [variable, in fpmod]
theory.homology.N [variable, in fpmod]
theory.homology.P [variable, in fpmod]
theory.homology.phi [variable, in fpmod]
theory.homology.psi [variable, in fpmod]
theory.R [variable, in fpmod]
_ %/ _ [notation, in fpmod]
tilt [definition, in binetcauchy]
tiltK [lemma, in binetcauchy]
tilt_inj [lemma, in binetcauchy]
tilt_bij [lemma, in binetcauchy]
tool_nth [lemma, in binetcauchy]
trans_ltn [lemma, in binetcauchy]
Triangular [section, in mxstructure]
TriangularBlock [section, in mxstructure]
TriangularBlock.Adl [variable, in mxstructure]
TriangularBlock.Adr [variable, in mxstructure]
TriangularBlock.Aul [variable, in mxstructure]
TriangularBlock.Aur [variable, in mxstructure]
TriangularBlock.m1 [variable, in mxstructure]
TriangularBlock.m2 [variable, in mxstructure]
TriangularBlock.n1 [variable, in mxstructure]
TriangularBlock.n2 [variable, in mxstructure]
TriangularBlock.R [variable, in mxstructure]
Triangular.R [variable, in mxstructure]
trivial_param [lemma, in refinements]
trmx_eq0 [lemma, in stronglydiscrete]
tr_copid_mx [lemma, in mxstructure]
tr_diag_mx_seq [lemma, in mxstructure]
tr_diag_block_mx [lemma, in mxstructure]


U

unitd1 [lemma, in dvdring]
unitmxEE [definition, in smith]
unitmxEE [definition, in smithpid]
unitmx_diag_block [lemma, in mxstructure]
unitrmxE [lemma, in smith]
unitrmxE [lemma, in smithpid]
unit_Bezout_mx [lemma, in dvdring]
upper_triangular_diag_block [lemma, in mxstructure]
upper_triangular_block [lemma, in mxstructure]
upper_triangular_block_mxul [lemma, in mxstructure]
upper_triangular_block_mxdr [lemma, in mxstructure]
upper_triangular_block_mxdl [lemma, in mxstructure]
upper_triangular_mx0 [lemma, in mxstructure]
upper_triangular_mxP [lemma, in mxstructure]
upper_triangular_mx [definition, in mxstructure]
upper_part_mx [definition, in mxstructure]


W

weight [definition, in binetcauchy]
widen_ord_eq [lemma, in minor]
wl [lemma, in coherent]
wr [lemma, in coherent]


Z

zeromor [definition, in fpmod]
zeromor_proof [lemma, in fpmod]


other

_ .( _ , _ ) (computable_scope) [notation, in refinements]
_ %/? _ (computable_scope) [notation, in refinements]
_ %| _ (computable_scope) [notation, in refinements]
_ >= _ (computable_scope) [notation, in refinements]
_ > _ (computable_scope) [notation, in refinements]
_ <= _ (computable_scope) [notation, in refinements]
_ < _ (computable_scope) [notation, in refinements]
_ == _ (computable_scope) [notation, in refinements]
_ / _ (computable_scope) [notation, in refinements]
_ *: _ (computable_scope) [notation, in refinements]
_ * _ (computable_scope) [notation, in refinements]
_ ^ _ (computable_scope) [notation, in refinements]
_ - _ (computable_scope) [notation, in refinements]
_ + _ (computable_scope) [notation, in refinements]
_ ^-1 (computable_scope) [notation, in refinements]
- _ (computable_scope) [notation, in refinements]
1 (computable_scope) [notation, in refinements]
0 (computable_scope) [notation, in refinements]
_ ^T (hetero_computable_scope) [notation, in refinements]
_ *: _ (hetero_computable_scope) [notation, in refinements]
_ *m _ (hetero_computable_scope) [notation, in refinements]
_ %:M (hetero_computable_scope) [notation, in refinements]
_ == _ (hetero_computable_scope) [notation, in refinements]
_ - _ (hetero_computable_scope) [notation, in refinements]
_ + _ (hetero_computable_scope) [notation, in refinements]
- _ (hetero_computable_scope) [notation, in refinements]
1 (hetero_computable_scope) [notation, in refinements]
0 (hetero_computable_scope) [notation, in refinements]
_ == _ (ideal_scope) [notation, in stronglydiscrete]
_ <= _ <= _ (ideal_scope) [notation, in stronglydiscrete]
_ <= _ (ideal_scope) [notation, in stronglydiscrete]
_ ^^-1 (mxpresentation_scope) [notation, in fpmod]
_ %| _ (mxpresentation_scope) [notation, in coherent]
_ .-ker (mxpresentation_scope) [notation, in coherent]
_ + _ (rel_scope) [notation, in refinements]
_ * _ (rel_scope) [notation, in refinements]
_ ==> _ (rel_scope) [notation, in hrel]
_ <=> _ (rel_scope) [notation, in hrel]
_ <= _ (rel_scope) [notation, in hrel]
_ \o _ (rel_scope) [notation, in hrel]
_ != _ %[mod _ ] (ring_scope) [notation, in dvdring]
_ <> _ %[mod _ ] (ring_scope) [notation, in dvdring]
_ == _ %[mod _ ] (ring_scope) [notation, in dvdring]
_ = _ %[mod _ ] (ring_scope) [notation, in dvdring]
_ %% _ (ring_scope) [notation, in dvdring]
_ %/ _ (ring_scope) [notation, in dvdring]
'Aut ( _ ) (type_scope) [notation, in fpmod]
'Iso ( _ , _ ) (type_scope) [notation, in fpmod]
'Epi ( _ , _ ) (type_scope) [notation, in fpmod]
'Mono ( _ , _ ) (type_scope) [notation, in fpmod]
'End ( _ ) (type_scope) [notation, in fpmod]
'Mor ( _ , _ ) (type_scope) [notation, in fpmod]
_ %/ _ [notation, in fpmod]
_ %= _ [notation, in fpmod]
_ ** _ [notation, in fpmod]
_ %:mor [notation, in fpmod]
_ %:m [notation, in fpmod]
_ *i _ [notation, in stronglydiscrete]
_ +i _ [notation, in stronglydiscrete]
*m%HC [notation, in refinements]
*%C [notation, in refinements]
*:%C [notation, in refinements]
*:%HC [notation, in refinements]
+%C [notation, in refinements]
+%HC [notation, in refinements]
-%C [notation, in refinements]
-%HC [notation, in refinements]
[Epi of _ ] [notation, in fpmod]
[Iso of _ ] [notation, in fpmod]
[Mono of _ ] [notation, in fpmod]
{ fpmod _ } [notation, in fpmod]



Notation Index

B

[ bezoutDomainType of _ ] (form_scope) [in dvdring]
[ bezoutDomainType of _ for _ ] (form_scope) [in dvdring]


C

_ .-ker (mxpresentation_scope) [in coherent]
_ %| _ (mxpresentation_scope) [in coherent]
[ coherentRingType of _ ] (form_scope) [in coherent]
[ coherentRingType of _ for _ ] (form_scope) [in coherent]


D

[ dvdRingType of _ ] (form_scope) [in dvdring]
[ dvdRingType of _ for _ ] (form_scope) [in dvdring]


E

[ edrType of _ ] (form_scope) [in edr]
[ edrType of _ for _ ] (form_scope) [in edr]
[ euclidDomainType of _ ] (form_scope) [in dvdring]
[ euclidDomainType of _ for _ ] (form_scope) [in dvdring]
_ %% _ (ring_scope) [in dvdring]
_ %/ _ (ring_scope) [in dvdring]


G

[ gcdDomainType of _ ] (form_scope) [in dvdring]
[ gcdDomainType of _ for _ ] (form_scope) [in dvdring]


H

_ \o _ (rel_scope) [in hrel]
_ <=> _ (rel_scope) [in hrel]
_ <= _ (rel_scope) [in hrel]


I

_ ^^-1 [in fpmod]


M

_ %= _ (mxpresentation_scope) [in fpmod]
_ ** _ (mxpresentation_scope) [in fpmod]


N

_ %/? _ (ring_scope) [in dvdring]
%/?%R (ring_scope) [in dvdring]
_ %| _ (ring_scope) [in dvdring]
%|%R (ring_scope) [in dvdring]
_ %= _ (ring_scope) [in dvdring]
%=R (ring_scope) [in dvdring]
_ %<| _ [in dvdring]
%<|R [in dvdring]


P

[ pidType of _ ] (form_scope) [in dvdring]
[ pidType of _ for _ ] (form_scope) [in dvdring]


R

_ %| _ (computable_scope) [in refinements]
_ <= _ (computable_scope) [in refinements]
_ < _ (computable_scope) [in refinements]
_ == _ (computable_scope) [in refinements]
_ %/? _ (computable_scope) [in refinements]
_ / _ (computable_scope) [in refinements]
_ *: _ (computable_scope) [in refinements]
_ * _ (computable_scope) [in refinements]
_ ^ _ (computable_scope) [in refinements]
_ - _ (computable_scope) [in refinements]
_ + _ (computable_scope) [in refinements]
_ ^-1 (computable_scope) [in refinements]
- _ (computable_scope) [in refinements]
1 (computable_scope) [in refinements]
0 (computable_scope) [in refinements]
_ ^T (hetero_computable_scope) [in refinements]
_ == _ (hetero_computable_scope) [in refinements]
_ *: _ (hetero_computable_scope) [in refinements]
_ *m _ (hetero_computable_scope) [in refinements]
_ ^-1 (hetero_computable_scope) [in refinements]
_ - _ (hetero_computable_scope) [in refinements]
- _ (hetero_computable_scope) [in refinements]
_ + _ (hetero_computable_scope) [in refinements]
1 (hetero_computable_scope) [in refinements]
0 (hetero_computable_scope) [in refinements]
*m%HC [in refinements]
*%C [in refinements]
*:%C [in refinements]
*:%HC [in refinements]
+%C [in refinements]
+%HC [in refinements]
-%C [in refinements]
-%HC [in refinements]
==%HC [in refinements]


S

'M_ _ (type_scope) [in smith]
'M_ ( _ ) (type_scope) [in smith]
'M_ ( _ , _ ) (type_scope) [in smith]
'I_ _ (type_scope) [in smith]
'M[A]_ ( _ ) [in smith]
'M[A]_ ( _ , _ ) [in smith]
_ :=: _ (ideal_scope) [in stronglydiscrete]
_ == _ (ideal_scope) [in stronglydiscrete]
_ <= _ <= _ (ideal_scope) [in stronglydiscrete]
_ <= _ (ideal_scope) [in stronglydiscrete]
_ *i _ [in stronglydiscrete]
_ +i _ [in stronglydiscrete]
[ stronglyDiscreteType of _ ] (form_scope) [in stronglydiscrete]
[ stronglyDiscreteType of _ for _ ] (form_scope) [in stronglydiscrete]


T

_ %/ _ [in fpmod]


other

_ .( _ , _ ) (computable_scope) [in refinements]
_ %/? _ (computable_scope) [in refinements]
_ %| _ (computable_scope) [in refinements]
_ >= _ (computable_scope) [in refinements]
_ > _ (computable_scope) [in refinements]
_ <= _ (computable_scope) [in refinements]
_ < _ (computable_scope) [in refinements]
_ == _ (computable_scope) [in refinements]
_ / _ (computable_scope) [in refinements]
_ *: _ (computable_scope) [in refinements]
_ * _ (computable_scope) [in refinements]
_ ^ _ (computable_scope) [in refinements]
_ - _ (computable_scope) [in refinements]
_ + _ (computable_scope) [in refinements]
_ ^-1 (computable_scope) [in refinements]
- _ (computable_scope) [in refinements]
1 (computable_scope) [in refinements]
0 (computable_scope) [in refinements]
_ ^T (hetero_computable_scope) [in refinements]
_ *: _ (hetero_computable_scope) [in refinements]
_ *m _ (hetero_computable_scope) [in refinements]
_ %:M (hetero_computable_scope) [in refinements]
_ == _ (hetero_computable_scope) [in refinements]
_ - _ (hetero_computable_scope) [in refinements]
_ + _ (hetero_computable_scope) [in refinements]
- _ (hetero_computable_scope) [in refinements]
1 (hetero_computable_scope) [in refinements]
0 (hetero_computable_scope) [in refinements]
_ == _ (ideal_scope) [in stronglydiscrete]
_ <= _ <= _ (ideal_scope) [in stronglydiscrete]
_ <= _ (ideal_scope) [in stronglydiscrete]
_ ^^-1 (mxpresentation_scope) [in fpmod]
_ %| _ (mxpresentation_scope) [in coherent]
_ .-ker (mxpresentation_scope) [in coherent]
_ + _ (rel_scope) [in refinements]
_ * _ (rel_scope) [in refinements]
_ ==> _ (rel_scope) [in hrel]
_ <=> _ (rel_scope) [in hrel]
_ <= _ (rel_scope) [in hrel]
_ \o _ (rel_scope) [in hrel]
_ != _ %[mod _ ] (ring_scope) [in dvdring]
_ <> _ %[mod _ ] (ring_scope) [in dvdring]
_ == _ %[mod _ ] (ring_scope) [in dvdring]
_ = _ %[mod _ ] (ring_scope) [in dvdring]
_ %% _ (ring_scope) [in dvdring]
_ %/ _ (ring_scope) [in dvdring]
'Aut ( _ ) (type_scope) [in fpmod]
'Iso ( _ , _ ) (type_scope) [in fpmod]
'Epi ( _ , _ ) (type_scope) [in fpmod]
'Mono ( _ , _ ) (type_scope) [in fpmod]
'End ( _ ) (type_scope) [in fpmod]
'Mor ( _ , _ ) (type_scope) [in fpmod]
_ %/ _ [in fpmod]
_ %= _ [in fpmod]
_ ** _ [in fpmod]
_ %:mor [in fpmod]
_ %:m [in fpmod]
_ *i _ [in stronglydiscrete]
_ +i _ [in stronglydiscrete]
*m%HC [in refinements]
*%C [in refinements]
*:%C [in refinements]
*:%HC [in refinements]
+%C [in refinements]
+%HC [in refinements]
-%C [in refinements]
-%HC [in refinements]
[Epi of _ ] [in fpmod]
[Iso of _ ] [in fpmod]
[Mono of _ ] [in fpmod]
{ fpmod _ } [in fpmod]



Module Index

A

AlgOp [in refinements]


B

BezoutDomain [in dvdring]
BezoutDomain.Exports [in dvdring]


C

CoherentRing [in coherent]
CoherentRing.Exports [in coherent]


D

DvdRing [in dvdring]
DvdRing.Exports [in dvdring]


E

EDR [in edr]
EDR.Exports [in edr]
EuclideanDomain [in dvdring]
EuclideanDomain.Exports [in dvdring]
EuclideanDomain.Mixins [in dvdring]


G

GcdDomain [in dvdring]
GcdDomain.Exports [in dvdring]


N

Notations [in dvdring]


P

PID [in dvdring]
PID.Exports [in dvdring]


R

Refinements [in refinements]
Refinements.Op [in refinements]
RPdiv [in similar]
RPdiv [in ssrcomplements]
RPdiv.mon [in similar]
RPdiv.mon [in ssrcomplements]


S

StronglyDiscrete [in stronglydiscrete]
StronglyDiscrete.Exports [in stronglydiscrete]



Variable Index

A

AdequacyEDR.gdco [in kaplansky]
AdequacyEDR.gdcoP [in kaplansky]
AdequacyEDR.R [in kaplansky]
AdequacyGdco.R [in kaplansky]
AdequacyPID.R [in kaplansky]


B

BezoutCoherent.R [in coherent]
BezoutDomainTheory.R [in dvdring]
BezoutDomain.ClassDef.cT [in dvdring]
BezoutDomain.ClassDef.T [in dvdring]
BezoutKrull1.krull1 [in kaplansky]
BezoutKrull1.R [in kaplansky]
BezoutStronglyDiscrete.R [in stronglydiscrete]
Bezout_hermite.R [in kaplansky]
BigOp.R [in ssrcomplements]
BigOp.T [in ssrcomplements]
BinetCauchy.A [in binetcauchy]
BinetCauchy.B [in binetcauchy]
BinetCauchy.k [in binetcauchy]
BinetCauchy.l [in binetcauchy]
BinetCauchy.R [in binetcauchy]
BinetCauchy.Z [in binetcauchy]


C

CoherentRingTheory.R [in coherent]
CoherentRing.ClassDef.cT [in coherent]
CoherentRing.ClassDef.T [in coherent]


D

diag_mx_dvdring.R [in mxstructure]
diag_mx_idomain.R [in mxstructure]
diag_mx_seq_comRingType.R [in mxstructure]
diag_mx_seq2.R [in mxstructure]
diag_mx_seq.R [in mxstructure]
diag_block_comUnitRingType.R [in mxstructure]
diag_block_comRingType.R [in mxstructure]
diag_block_ringType2.R [in mxstructure]
diag_block_ringType.R [in mxstructure]
DvdRingTheory.R [in dvdring]
DvdRing.ClassDef.cT [in dvdring]
DvdRing.ClassDef.T [in dvdring]
DvdRing.R [in similar]


E

EDR_Theory.Preunicity.widen_minr [in edr]
EDR_Theory.Preunicity.widen_minl [in edr]
EDR_Theory.Preunicity.HAs [in edr]
EDR_Theory.Preunicity.Hs [in edr]
EDR_Theory.Preunicity.Hk [in edr]
EDR_Theory.Preunicity.A [in edr]
EDR_Theory.Preunicity.k [in edr]
EDR_Theory.Preunicity.n [in edr]
EDR_Theory.Preunicity.m [in edr]
EDR_Theory.Preunicity.s [in edr]
EDR_Theory.snf_coherent.defs.M [in edr]
EDR_Theory.snf_coherent.defs.n [in edr]
EDR_Theory.snf_coherent.defs.m [in edr]
EDR_Theory.R [in edr]
EDR.ClassDef.cT [in edr]
EDR.ClassDef.T [in edr]
EpiTheory.Epi1.M [in fpmod]
EpiTheory.Epi1.N [in fpmod]
EpiTheory.R [in fpmod]
EquivalentDef.R [in similar]
EuclideanDomainTheory.R [in dvdring]
EuclideanDomain.ClassDef.cT [in dvdring]
EuclideanDomain.ClassDef.T [in dvdring]
EuclideanDomain.Mixins.Mixins.cR [in dvdring]
EuclideanDomain.Mixins.Mixins.dvdM [in dvdring]
EuclideanDomain.Mixins.Mixins.gcdM [in dvdring]
EuclideanDomain.Mixins.Mixins.mR [in dvdring]
EuclideanDomain.Mixins.Mixins.R [in dvdring]


F

Field.m [in similar]
Field.n [in similar]
Field.R [in similar]


G

GCDDomainTheory.R [in dvdring]
GcdDomain.ClassDef.cT [in dvdring]
GcdDomain.ClassDef.T [in dvdring]
GUARD.A [in dvdring]
GUARD.P [in dvdring]


I

IntersectionCoherent.cap [in coherent]
IntersectionCoherent.cap_spec [in coherent]
IntersectionCoherent.dim_cap [in coherent]
IntersectionCoherent.R [in coherent]
IsoTheory.M [in fpmod]
IsoTheory.N [in fpmod]
IsoTheory.R [in fpmod]


K

Kaplansky_necc.c [in kaplansky]
Kaplansky_necc.b [in kaplansky]
Kaplansky_necc.a [in kaplansky]
Kaplansky_necc.R [in kaplansky]
Kaplansky_suff.kapP [in kaplansky]
Kaplansky_suff.kap [in kaplansky]
Kaplansky_suff.R [in kaplansky]
KernelAndCo.M [in fpmod]
KernelAndCo.N [in fpmod]
KernelAndCo.phi [in fpmod]
KernelAndCo.R [in fpmod]
ker_col.ker_colP [in coherent]
ker_col.ker_col [in coherent]
ker_col.dim_ker_col [in coherent]
ker_col.R [in coherent]


M

Matrix.matrix_comUnitRingType.R [in ssrcomplements]
Matrix.matrix_ringType.R [in ssrcomplements]
Matrix.matrix_raw_type.T [in ssrcomplements]
minor_char_poly_mx.R [in minor]
minor_theory.R [in minor]
minor_def.R [in minor]
MonoEpi.M [in fpmod]
MonoEpi.N [in fpmod]
MonoEpi.R [in fpmod]
MonoTheory.Mono1.M [in fpmod]
MonoTheory.Mono1.n [in fpmod]
MonoTheory.Mono1.N [in fpmod]
MonoTheory.Mono1.X [in fpmod]
MonoTheory.R [in fpmod]
morphismDef.R [in fpmod]
morphismProperties.M [in fpmod]
morphismProperties.N [in fpmod]
morphismProperties.phi [in fpmod]
morphismProperties.R [in fpmod]
morphismTheory.category.defs.K [in fpmod]
morphismTheory.category.defs.M [in fpmod]
morphismTheory.category.defs.N [in fpmod]
morphismTheory.category.theory.M [in fpmod]
morphismTheory.category.theory.N [in fpmod]
morphismTheory.category.theory.P [in fpmod]
morphismTheory.category.theory.Q [in fpmod]
morphismTheory.equality.M [in fpmod]
morphismTheory.equality.N [in fpmod]
morphismTheory.general.K [in fpmod]
morphismTheory.general.M [in fpmod]
morphismTheory.general.n [in fpmod]
morphismTheory.general.N [in fpmod]
morphismTheory.general.X [in fpmod]
morphismTheory.R [in fpmod]
morphismTheory.zmodType.M [in fpmod]
morphismTheory.zmodType.N [in fpmod]
Mx2.R [in kaplansky]


P

PIDTheory.R [in dvdring]
PID.ClassDef.cT [in dvdring]
PID.ClassDef.T [in dvdring]
Poly.R [in ssrcomplements]


R

RPdiv.mon.MonicDivisor.d [in similar]
RPdiv.mon.MonicDivisor.d [in ssrcomplements]
RPdiv.mon.MonicDivisor.mond [in similar]
RPdiv.mon.MonicDivisor.mond [in ssrcomplements]
RPdiv.mon.MonicDivisor.R [in similar]
RPdiv.mon.MonicDivisor.R [in ssrcomplements]
RPdiv.RingPseudoDivision.R [in similar]
RPdiv.RingPseudoDivision.R [in ssrcomplements]


S

Seqeqtype.leT [in ssrcomplements]
Seqeqtype.leT_tr [in ssrcomplements]
Seqeqtype.T [in ssrcomplements]
Seq.f [in ssrcomplements]
Seq.T1 [in ssrcomplements]
Seq.T2 [in ssrcomplements]
Seq.T3 [in ssrcomplements]
SimilarDef.R [in similar]
simplmx [in kaplansky]
smith_theory.find_pivotP [in smith]
smith_theory.find2P [in smith]
smith_theory.find1P [in smith]
smith_theory.find_pivot [in smith]
smith_theory.find2 [in smith]
smith_theory.find1 [in smith]
smith_theory.E [in smith]
smith_def.Bezout_step [in smith]
smith_def.find_pivot [in smith]
smith_def.find2 [in smith]
smith_def.find1 [in smith]
smith_def.ordA [in smith]
smith_def.mxA [in smith]
smith_def.A [in smith]
smith_def.find_pivotP [in smithpid]
smith_def.find_pivot [in smithpid]
smith_def.find2P [in smithpid]
smith_def.find1P [in smithpid]
smith_def.find2 [in smithpid]
smith_def.find1 [in smithpid]
smith_def.R [in smithpid]
smith_fpmod.Q [in fpmod]
smith_fpmod.P [in fpmod]
smith_fpmod.D [in fpmod]
smith_fpmod.M [in fpmod]
smith_fpmod.R [in fpmod]
Smith2x2_correctness.smith2x2P [in kaplansky]
Smith2x2_correctness.smith2x2 [in kaplansky]
Smith2x2_correctness.R [in kaplansky]
Smith2x2.R [in kaplansky]
Smith2x2.smith2x2 [in kaplansky]
SquareTriangular.R [in mxstructure]
SquareTriangular2.R [in mxstructure]
StronglyDiscreteTheory.IdealTheory.IdealIntersection.cap_size [in stronglydiscrete]
StronglyDiscreteTheory.R [in stronglydiscrete]
StronglyDiscrete.ClassDef.cT [in stronglydiscrete]
StronglyDiscrete.ClassDef.T [in stronglydiscrete]
submatrix_char_poly_mx.R [in minor]
submatrix_theory.R [in minor]
submatrix_def.B [in minor]
submatrix_def.A [in minor]


T

theory.dsum.M [in fpmod]
theory.dsum.N [in fpmod]
theory.homology.M [in fpmod]
theory.homology.mul_phi_psi [in fpmod]
theory.homology.N [in fpmod]
theory.homology.P [in fpmod]
theory.homology.phi [in fpmod]
theory.homology.psi [in fpmod]
theory.R [in fpmod]
TriangularBlock.Adl [in mxstructure]
TriangularBlock.Adr [in mxstructure]
TriangularBlock.Aul [in mxstructure]
TriangularBlock.Aur [in mxstructure]
TriangularBlock.m1 [in mxstructure]
TriangularBlock.m2 [in mxstructure]
TriangularBlock.n1 [in mxstructure]
TriangularBlock.n2 [in mxstructure]
TriangularBlock.R [in mxstructure]
Triangular.R [in mxstructure]



Library Index

B

binetcauchy


C

coherent


D

dvdring


E

edr


F

fpmod


H

hrel


K

kaplansky


M

minor
mxstructure


R

refinements


S

similar
smith
smithpid
ssrcomplements
stronglydiscrete



Lemma Index

A

addidC [in stronglydiscrete]
addid_congr [in stronglydiscrete]
addid_addA [in stronglydiscrete]
addid0 [in stronglydiscrete]
addmA_subproof [in fpmod]
addmC_subproof [in fpmod]
addmor_proof [in fpmod]
addNm_subproof [in fpmod]
add_diag_block [in mxstructure]
add_addir [in stronglydiscrete]
add_addil [in stronglydiscrete]
add0id [in stronglydiscrete]
add0m_subproof [in fpmod]
adequate_gdco [in kaplansky]


B

bcap_spec [in coherent]
bcap_int [in coherent]
bcap_wrP [in coherent]
bcap_wlP [in coherent]
bezoutP [in dvdring]
Bezout_step_mx00 [in dvdring]
Bezout_stepE [in dvdring]
bezout_edrP [in edr]
big_gcdr_def [in dvdring]
big_gcdrP [in dvdring]
big_dvdr_gcdr [in dvdring]
big_dvdr [in dvdring]
BinetCauchy [in binetcauchy]
bmember_correct [in stronglydiscrete]


C

cast0 [in binetcauchy]
cast1 [in binetcauchy]
char_diag_block_mx [in mxstructure]
char_poly_triangular_mx [in mxstructure]
char_poly_mx_triangular_mx [in mxstructure]
char_block_mx [in ssrcomplements]
codom_perm [in binetcauchy]
cokerK [in fpmod]
cokerP [in fpmod]
coker_eq0 [in fpmod]
colE [in coherent]
col_id_mulmx [in ssrcomplements]
col_0mx [in ssrcomplements]
col_flat_mx [in ssrcomplements]
col_ebase_unit [in edr]
combine_mx_inv [in dvdring]
combine_stepE [in dvdring]
composableE [in refinements]
composable_imply_id1 [in refinements]
composable_imply [in refinements]
composable_rid1 [in refinements]
composable_lock [in refinements]
comp_eql [in hrel]
comp_eqr [in hrel]
comp_hrelP [in hrel]
congr_eqd [in dvdring]
coprimep_factor [in ssrcomplements]
coprimerP [in kaplansky]
coprimer_pexpr [in dvdring]
coprimer_pexpl [in dvdring]
coprimer_expr [in dvdring]
coprimer_expl [in dvdring]
coprimer_dvdr [in dvdring]
coprimer_dvdl [in dvdring]
coprimer_mull [in dvdring]
coprimer_mulr [in dvdring]
coprimer_sym [in dvdring]
coprimer_gdco [in kaplansky]


D

detAB_weight [in binetcauchy]
detmx2 [in kaplansky]
det_diag_mx_seq [in mxstructure]
det_diag_mx_seq_truncated [in mxstructure]
det_diag_block [in mxstructure]
det_triangular_mx [in mxstructure]
det2 [in minor]
diag_mx_seq_filter0 [in mxstructure]
diag_mx_seq_scale [in mxstructure]
diag_mx_seq_eq0 [in mxstructure]
diag_mx_seq0 [in mxstructure]
diag_mx_seq_take_min [in mxstructure]
diag_mx_seq_taker [in mxstructure]
diag_mx_seq_takel [in mxstructure]
diag_mx_seq_deltar [in mxstructure]
diag_mx_seq_deltal [in mxstructure]
diag_block_mx_seq [in mxstructure]
diag_mx_seq_block [in mxstructure]
diag_mx_seq_block_mx [in mxstructure]
diag_mx_seq_cat [in mxstructure]
diag_mx_seq_cons [in mxstructure]
diag_mx_seq_nil [in mxstructure]
diag_block_mx0 [in mxstructure]
diag_neq0 [in edr]
diag0 [in edr]
dividK [in stronglydiscrete]
divmxK [in coherent]
divr_mulKl [in dvdring]
divr_mulKr [in dvdring]
dsum_is_coproduct [in fpmod]
dsum_is_product [in fpmod]
dvdmxB [in coherent]
dvdmxBl [in coherent]
dvdmxBr [in coherent]
dvdmxD [in coherent]
dvdmxDl [in coherent]
dvdmxDr [in coherent]
dvdmxMl [in coherent]
dvdmxMr [in coherent]
dvdmxN [in coherent]
dvdmxP [in coherent]
dvdmx_morphism [in fpmod]
dvdmx_trans [in coherent]
dvdmx_refl [in coherent]
dvdmx0 [in coherent]
dvdNmx [in coherent]
dvdNr [in dvdring]
dvdrN [in dvdring]
dvdrNN [in dvdring]
dvdrP [in dvdring]
dvdrr [in dvdring]
dvdrU [in dvdring]
dvdr_mod [in dvdring]
dvdr_coprime [in dvdring]
dvdr_mem_lcms [in dvdring]
dvdr_lcms [in dvdring]
dvdr_mem_gcds [in dvdring]
dvdr_gcds [in dvdring]
dvdr_lcm_idl [in dvdring]
dvdr_lcm_idr [in dvdring]
dvdr_gcdr_lcmr [in dvdring]
dvdr_lcmr [in dvdring]
dvdr_lcml [in dvdring]
dvdr_lcm [in dvdring]
dvdr_gcd_mul [in dvdring]
dvdr_gcdr [in dvdring]
dvdr_gcdl [in dvdring]
dvdr_gcd [in dvdring]
dvdr_row_mx [in dvdring]
dvdr_col_mx [in dvdring]
dvdr_drsubmx [in dvdring]
dvdr_dlsubmx [in dvdring]
dvdr_ursubmx [in dvdring]
dvdr_ulsubmx [in dvdring]
dvdr_lsubmx [in dvdring]
dvdr_rsubmx [in dvdring]
dvdr_dsubmx [in dvdring]
dvdr_usubmx [in dvdring]
dvdr_mulmxl [in dvdring]
dvdr_mulmxr [in dvdring]
dvdr_mull_l [in dvdring]
dvdr_mulr_l [in dvdring]
dvdr_mul2l [in dvdring]
dvdr_mul2r [in dvdring]
dvdr_mul [in dvdring]
dvdr_mulr [in dvdring]
dvdr_mull [in dvdring]
dvdr_add_eq [in dvdring]
dvdr_addr [in dvdring]
dvdr_addl [in dvdring]
dvdr_sub [in dvdring]
dvdr_add [in dvdring]
dvdr_trans [in dvdring]
dvdr0 [in dvdring]
dvdr1 [in dvdring]
dvdUr [in dvdring]
dvd_quot_mx [in fpmod]
dvd_col_mxu [in coherent]
dvd_col_mxl [in coherent]
dvd_col_mxP [in coherent]
dvd_mx_col [in coherent]
dvd_ker_mod_1 [in coherent]
dvd_ker_mod_ker [in coherent]
dvd_ker [in coherent]
dvd0mx [in coherent]
dvd0r [in dvdring]
dvd1mx [in coherent]
dvd1r [in dvdring]


E

edivrP [in dvdring]
egcdrP [in dvdring]
egcdr3P [in kaplansky]
enorm_eq0 [in dvdring]
enorm_mul [in dvdring]
enorm0_lt [in dvdring]
epi [in fpmod]
epiP [in fpmod]
epi_coker [in fpmod]
eqdd [in dvdring]
eqdP [in dvdring]
eqdr0 [in dvdring]
eqd_equiv [in similar]
eqd_lcml [in dvdring]
eqd_lcmr [in dvdring]
eqd_gcd [in dvdring]
eqd_big_mul1 [in dvdring]
eqd_big_mul [in dvdring]
eqd_mull [in dvdring]
eqd_mulr [in dvdring]
eqd_rtrans [in dvdring]
eqd_ltrans [in dvdring]
eqd_dvdl [in dvdring]
eqd_dvdr [in dvdring]
eqd_dvd [in dvdring]
eqd_mul2r [in dvdring]
eqd_mul2l [in dvdring]
eqd_mul [in dvdring]
eqd_trans [in dvdring]
eqd_sym [in dvdring]
eqd_def [in dvdring]
eqd_seq_gcdr [in edr]
eqd0r [in dvdring]
eqd1 [in dvdring]
eqidP [in stronglydiscrete]
eqid_mulidAl [in stronglydiscrete]
eqid_tr_mxvec [in stronglydiscrete]
eqid_scaleid [in stronglydiscrete]
eqid_trans [in stronglydiscrete]
eqid_sym [in stronglydiscrete]
eqid_refl [in stronglydiscrete]
eqid_eq0 [in stronglydiscrete]
eqmorMl [in fpmod]
eqmorMr [in fpmod]
eqmorxx [in fpmod]
eqmor_mono [in fpmod]
eqmor_epi [in fpmod]
eqmor_rtrans [in fpmod]
eqmor_ltrans [in fpmod]
eqmor_trans [in fpmod]
eqmor_sym [in fpmod]
eqmor_refl [in fpmod]
equiv_diag_block [in similar]
equiv_cast [in similar]
equiv_dgblockmx [in similar]
equiv_drblockmx [in similar]
equiv_ulblockmx [in similar]
equiv_trans [in similar]
equiv_sym [in similar]
equiv_refl [in similar]
equiv0l [in similar]
equiv0r [in similar]
eq_hrelLR [in hrel]
eq_hrelRL [in hrel]
eq_eqd [in dvdring]
euclid [in dvdring]
EuclideanDomain.Mixins.acc_gcdP [in dvdring]
EuclideanDomain.Mixins.dvd_mod [in dvdring]
EuclideanDomain.Mixins.edivP [in dvdring]
EuclideanDomain.Mixins.egcdP [in dvdring]
EuclideanDomain.Mixins.egcd_recP [in dvdring]
EuclideanDomain.Mixins.gcdP [in dvdring]
EuclideanDomain.Mixins.GCDP [in dvdring]
EuclideanDomain.Mixins.gcdrE [in dvdring]
EuclideanDomain.Mixins.leq_norm [in dvdring]
EuclideanDomain.Mixins.ltn_norm [in dvdring]
EuclideanDomain.Mixins.modr0 [in dvdring]
EuclideanDomain.Mixins.mod_spec [in dvdring]
EuclideanDomain.Mixins.mod_eq0 [in dvdring]
EuclideanDomain.Mixins.mod0r [in dvdring]
EuclideanDomain.Mixins.norm_eq0 [in dvdring]
EuclideanDomain.Mixins.norm_mul [in dvdring]
EuclideanDomain.Mixins.norm0_lt [in dvdring]
EuclideanDomain.Mixins.odivP [in dvdring]
EuclideanDomain.Mixins.odiv_def [in dvdring]
EuclideanDomain.Mixins.sdvdr_wf [in dvdring]
EuclideanDomain.Mixins.tool [in dvdring]
euclid_gcdl [in dvdring]
euclid_gcdr [in dvdring]
euclid_inv [in dvdring]
exp_diag_block_cons [in mxstructure]
exp_diag_block_S [in mxstructure]
exp_block_mx [in ssrcomplements]
ext_block [in mxstructure]


F

factorP [in fpmod]
factor_proof [in fpmod]
from_good_to_perm [in binetcauchy]
fz_tilt_0 [in binetcauchy]


G

gather_by_strictness [in binetcauchy]
gcdrA [in dvdring]
gcdrAC [in dvdring]
gcdrC [in dvdring]
gcdrCA [in dvdring]
gcdr_addl_mul [in dvdring]
gcdr_addl_l [in dvdring]
gcdr_addr_l [in dvdring]
gcdr_addl_r [in dvdring]
gcdr_addr_r [in dvdring]
gcdr_mul2l [in dvdring]
gcdr_mul2r [in dvdring]
gcdr_def [in dvdring]
gcdr_eq0 [in dvdring]
gcdr0 [in dvdring]
gcdr1 [in dvdring]
gcdsr_cons [in dvdring]
gcdsr0 [in dvdring]
gcd_edrP [in edr]
gcd0r [in dvdring]
gcd1r [in dvdring]
gdco_smithP [in kaplansky]
gdco_kapP [in kaplansky]
gdco_adequate [in kaplansky]
getparam_some [in refinements]
getparam_if [in refinements]
getparam_map [in refinements]
getparam_nth [in refinements]
getparam_size [in refinements]
getparam_iter [in refinements]
getparam_foldl [in refinements]
getparam_foldr [in refinements]
getparam_rcons [in refinements]
getparam_cons [in refinements]
getparam_sum_rect [in refinements]
getparam_inr [in refinements]
getparam_inl [in refinements]
getparam_snd [in refinements]
getparam_fst [in refinements]
getparam_pair [in refinements]
getparam_abstr [in refinements]
getparam_eq [in refinements]
getparam_key [in refinements]
get_param [in refinements]
goodP [in binetcauchy]


H

hermite10 [in kaplansky]
homology_dvd [in fpmod]
horner_mx_diag_block [in mxstructure]


I

id_param [in refinements]
improve_pivotP [in smith]
improve_pivot_recP [in smith]
improve_pivotP [in smithpid]
improve_pivot_recP [in smithpid]
inj_widen_ord [in minor]
inj_lift [in minor]
inj_strictf_ffun [in binetcauchy]
inj_strictf [in binetcauchy]
inj1_proj1 [in fpmod]
inj1_proj2 [in fpmod]
inj1_is_mono [in fpmod]
inj1_proof [in fpmod]
inj2_proj2 [in fpmod]
inj2_proj1 [in fpmod]
inj2_is_mono [in fpmod]
inj2_proof [in fpmod]
invmx_diag_block [in mxstructure]
invmx_block [in ssrcomplements]
inv_g_of_fx_inj [in binetcauchy]
inv_g_of_fxE [in binetcauchy]
irredrP [in dvdring]
irredr_primer [in dvdring]
irredr_coprimer [in dvdring]
irredr_dvd [in dvdring]
isomorphisms_idm [in fpmod]
isoP [in fpmod]
iso_smithm [in fpmod]
iso_coker_eq0 [in fpmod]
iso_kernel_eq0 [in fpmod]


K

kapP [in kaplansky]
kapWP [in kaplansky]
kap_smithP [in kaplansky]
kerAK [in coherent]
kerE [in coherent]
kerK [in coherent]
kermxP [in edr]
kernelK [in fpmod]
kernelP [in fpmod]
kernel_eq0 [in fpmod]
kerP [in coherent]
kerP_subproof [in coherent]
ker_c_intP [in coherent]
ker_cP [in coherent]
ker_mod1 [in coherent]
ker_modK [in coherent]
ker1 [in coherent]
krull1_smithP [in kaplansky]
krull1_gdcoP [in kaplansky]
krull1_adequate [in kaplansky]
krull1_factor [in kaplansky]


L

lcmrA [in dvdring]
lcmrAC [in dvdring]
lcmrC [in dvdring]
lcmrCA [in dvdring]
lcmr_mulr [in dvdring]
lcmr_mull [in dvdring]
lcmr_mul2l [in dvdring]
lcmr_mul2r [in dvdring]
lcmr0 [in dvdring]
lcmr1 [in dvdring]
lcmsr_cons [in dvdring]
lcmsr0 [in dvdring]
lcm0r [in dvdring]
lcm1r [in dvdring]
left_mono [in fpmod]
leq_enorm [in dvdring]
lift_predS [in minor]
lift_pred0 [in minor]
lift_pred_widen_ord [in minor]
lift_mono [in fpmod]
lift_epi [in fpmod]
lift_subproof [in fpmod]
linv_surj [in fpmod]
lower_triangular_mxP [in mxstructure]
ltn_enorm [in dvdring]
lt_wf2 [in dvdring]


M

memberE [in stronglydiscrete]
memberP [in stronglydiscrete]
member_subid [in stronglydiscrete]
member_in [in stronglydiscrete]
member_specP [in stronglydiscrete]
mem_same_codom [in binetcauchy]
minorn [in minor]
minor_lift_block [in minor]
minor_eq [in minor]
minor_g_not_injective [in minor]
minor_f_not_injective [in minor]
minor_alternate_g [in minor]
minor_alternate_f [in minor]
minor_ltn_eq0r [in minor]
minor_ltn_eq0l [in minor]
minor_eq0r [in edr]
minor_eq0l [in edr]
minor_diag_mx_seq [in edr]
minor1 [in minor]
minor2 [in minor]
modr_spec [in dvdring]
modr_eq0 [in dvdring]
modr0 [in dvdring]
mod0r [in dvdring]
mono [in fpmod]
monoP [in fpmod]
mono_ker [in fpmod]
morphism1_subproof [in fpmod]
mor_of_mx_inj [in fpmod]
mor_of_mx_proof [in fpmod]
mulepi_eq0 [in fpmod]
mulidC [in stronglydiscrete]
mulid_congr [in stronglydiscrete]
mulid_addidr [in stronglydiscrete]
mulid0 [in stronglydiscrete]
mulkmor [in fpmod]
mulmono_eq0 [in fpmod]
mulmorA [in fpmod]
mulmorBl [in fpmod]
mulmorBr [in fpmod]
mulmorc [in fpmod]
mulmorDl [in fpmod]
mulmorDr [in fpmod]
mulmorN [in fpmod]
mulmorV [in fpmod]
mulmor_proof [in fpmod]
mulmor0 [in fpmod]
mulmor1 [in fpmod]
mulmor11 [in fpmod]
mulmxKV_kermx [in edr]
mulmx_diag_block [in mxstructure]
mulmx_lsub [in ssrcomplements]
mulmx_rsub [in ssrcomplements]
mulmx_coker [in edr]
mulmx_diag_mx [in edr]
mulmx_ebase [in edr]
mulNmor [in fpmod]
mulr_lcml [in dvdring]
mulr_lcmr [in dvdring]
mulr_lcm_gcd [in dvdring]
mulr_gcdl [in dvdring]
mulr_gcdr [in dvdring]
mulVmor [in fpmod]
mul_diag_mx_seq_eq0 [in mxstructure]
mul_mx_diag_seq_min [in mxstructure]
mul_copid_mx_diag [in mxstructure]
mul_diag_mx_copid [in mxstructure]
mul_diag_mx_pid [in mxstructure]
mul_pid_mx_diag [in mxstructure]
mul_klift [in fpmod]
mul_lift [in fpmod]
mul_kermx [in edr]
mul0id [in stronglydiscrete]
mul0mor [in fpmod]
mul1mor [in fpmod]
mxrank_leq_col [in edr]
mxrank_leq_row [in edr]
mxrank_leq_col_row [in edr]
mxrank0 [in edr]
mxvec0 [in stronglydiscrete]
mx2_E11 [in kaplansky]
mx2_E10 [in kaplansky]
mx2_E01 [in kaplansky]
mx2_E00 [in kaplansky]


N

nth_change_default [in binetcauchy]


O

odivrP [in dvdring]
odivrr [in dvdring]
odivr_some [in dvdring]
odivr_mul2r [in dvdring]
odivr_mul2l [in dvdring]
odivr_mulKr [in dvdring]
odivr_mulrK [in dvdring]
odivr0 [in dvdring]
odivr1 [in dvdring]
odiv0r [in dvdring]
one_step [in binetcauchy]
oppmor_proof [in fpmod]


P

paramE [in refinements]
paramP [in refinements]
paramR [in refinements]
param_abstr2 [in refinements]
param_abstr [in refinements]
param_trans [in refinements]
param_id [in refinements]
param_eq [in refinements]
param_key [in refinements]
path_ordered_nth [in binetcauchy]
path_drop [in binetcauchy]
perm_fE [in binetcauchy]
pid_smithP [in kaplansky]
pid_gdco [in kaplansky]
pminor_char_poly_mx_monic [in minor]
principal_w2_correct [in dvdring]
principal_w1_correct [in dvdring]
principal_gen_dvd [in dvdring]
prod_seq_count [in ssrcomplements]
prod_minor_seq [in edr]
proj1_is_epi [in fpmod]
proj1_proof [in fpmod]
proj2_is_epi [in fpmod]


R

reindex_with_tilt [in binetcauchy]
right_epi [in fpmod]
rinv_inj [in fpmod]
row_id_mulmx [in ssrcomplements]
row_thin_mx [in ssrcomplements]
row_ebase_unit [in edr]
row'_col'_triangular_mx [in mxstructure]
row'_col'_char_poly_mx [in ssrcomplements]
RPdiv.add_id [in similar]
RPdiv.add_id [in ssrcomplements]
RPdiv.expr_rev [in similar]
RPdiv.expr_rev [in ssrcomplements]
RPdiv.ltn_rmodp_l [in similar]
RPdiv.ltn_rmodp_l [in ssrcomplements]
RPdiv.monic_map_inj [in similar]
RPdiv.monic_map_inj [in ssrcomplements]
RPdiv.mon.rdivp_l_eq [in similar]
RPdiv.mon.rdivp_l_eq [in ssrcomplements]
RPdiv.phiK [in similar]
RPdiv.phiK [in ssrcomplements]
RPdiv.phi_bij [in similar]
RPdiv.phi_invK [in similar]
RPdiv.phi_is_rmorphism [in similar]
RPdiv.phi_bij [in ssrcomplements]
RPdiv.phi_invK [in ssrcomplements]
RPdiv.phi_is_rmorphism [in ssrcomplements]


S

same_codomP [in binetcauchy]
scalar_diag_block_mx [in mxstructure]
scale_mulidr [in stronglydiscrete]
scale_trmx [in stronglydiscrete]
scale_mxvec [in stronglydiscrete]
scale_addid [in stronglydiscrete]
sdvdrNW [in dvdring]
sdvdrW [in dvdring]
sdvdr_wf [in dvdring]
sdvdr_def [in dvdring]
sdvdr0 [in dvdring]
sdvd_Bezout_step2 [in smithpid]
sdvd_Bezout_step [in dvdring]
sdvd0r [in dvdring]
seq2_ind [in similar]
seq2_ind [in ssrcomplements]
set_param [in refinements]
sign_tilt2 [in binetcauchy]
sig_tilt [in binetcauchy]
similar_char_poly [in similar]
similar_mxminpoly [in similar]
similar_fundamental [in similar]
similar_equiv [in similar]
similar_diag_block [in similar]
similar_horner [in similar]
similar_poly [in similar]
similar_exp [in similar]
similar_dgblockmx [in similar]
similar_drblockmx [in similar]
similar_ulblockmx [in similar]
similar_diag_mx_seq [in similar]
similar_cast [in similar]
similar_det [in similar]
similar_refl [in similar]
similar_trans [in similar]
similar_sym [in similar]
similar0 [in similar]
size_tool [in minor]
size_Smith [in smith]
size_sum_big [in mxstructure]
size_sum_big_cons [in mxstructure]
size_Smith [in smithpid]
smithmxnP [in kaplansky]
smithmxn_recP [in kaplansky]
SmithP [in smith]
SmithP [in smithpid]
smithP [in edr]
smith_inv_subproof [in fpmod]
smith_subproof [in fpmod]
Smith_unicity [in edr]
Smith_gcdr_spec [in edr]
smith1xnP [in kaplansky]
smith2xnP [in kaplansky]
sorted_nth0 [in dvdring]
sorted_cons [in dvdring]
sorted_dvd0r [in dvdring]
sorted_take [in ssrcomplements]
sorted_drop [in ssrcomplements]
sorted_ordered_nth_gen [in binetcauchy]
sorted_ordered_nth [in binetcauchy]
sorted_enum [in binetcauchy]
split_andb [in fpmod]
split_sumZ_fs [in binetcauchy]
split_sumZ_sf [in binetcauchy]
step_weight [in binetcauchy]
strictf_uniq [in binetcauchy]
strictf_lift [in binetcauchy]
strict_from_fP [in binetcauchy]
strict_fromP [in binetcauchy]
subeqid_refl [in stronglydiscrete]
subidMl [in stronglydiscrete]
subidP [in stronglydiscrete]
subid_mulid_congr [in stronglydiscrete]
subid_mulC [in stronglydiscrete]
subid_tr_mxvec [in stronglydiscrete]
subid_scaleid [in stronglydiscrete]
subid_addid_congr [in stronglydiscrete]
subid_addAr [in stronglydiscrete]
subid_addAl [in stronglydiscrete]
subid_addC [in stronglydiscrete]
subid_castmxr [in stronglydiscrete]
subid_castmxl [in stronglydiscrete]
subid_memberP [in stronglydiscrete]
subid_le0 [in stronglydiscrete]
subid_trans [in stronglydiscrete]
subid_refl [in stronglydiscrete]
subid_colP [in stronglydiscrete]
subid1 [in stronglydiscrete]
submatrix_char_poly_mx [in minor]
submatrix_scalar_mx [in minor]
submatrix_mul [in minor]
submatrix_sub [in minor]
submatrix_opp [in minor]
submatrix_add [in minor]
submatrix_scale [in minor]
submatrix_lift_block [in minor]
submatrix_eq [in minor]
submatrix_map_mx [in minor]
submatrix0 [in minor]
subrid [in stronglydiscrete]
sub_submatrix [in minor]
sub_hresp_comp [in hrel]
sub_eql [in hrel]
sub_Truer [in hrel]
sub_Falsel [in hrel]
sub_kermxP [in coherent]
sub_mulidr [in stronglydiscrete]
sub_mulidl [in stronglydiscrete]
sub_addidr [in stronglydiscrete]
sub_addidl [in stronglydiscrete]
sub_addid0l [in stronglydiscrete]
sub_add0lid [in stronglydiscrete]
sub_addid0r [in stronglydiscrete]
sub_add0rid [in stronglydiscrete]
sub0id [in stronglydiscrete]
sum_bad [in binetcauchy]
surgery [in kaplansky]
surgery2 [in kaplansky]


T

tiltK [in binetcauchy]
tilt_inj [in binetcauchy]
tilt_bij [in binetcauchy]
tool_nth [in binetcauchy]
trans_ltn [in binetcauchy]
trivial_param [in refinements]
trmx_eq0 [in stronglydiscrete]
tr_copid_mx [in mxstructure]
tr_diag_mx_seq [in mxstructure]
tr_diag_block_mx [in mxstructure]


U

unitd1 [in dvdring]
unitmx_diag_block [in mxstructure]
unitrmxE [in smith]
unitrmxE [in smithpid]
unit_Bezout_mx [in dvdring]
upper_triangular_diag_block [in mxstructure]
upper_triangular_block [in mxstructure]
upper_triangular_block_mxul [in mxstructure]
upper_triangular_block_mxdr [in mxstructure]
upper_triangular_block_mxdl [in mxstructure]
upper_triangular_mx0 [in mxstructure]
upper_triangular_mxP [in mxstructure]


W

widen_ord_eq [in minor]
wl [in coherent]
wr [in coherent]


Z

zeromor_proof [in fpmod]



Constructor Index

A

AdequateSpec [in kaplansky]
AdequateSpec0 [in kaplansky]


B

BezoutDomain.BezoutSpec [in dvdring]
BezoutDomain.Class [in dvdring]
BezoutDomain.Mixin [in dvdring]
BezoutDomain.Pack [in dvdring]


C

CoherentRing.Class [in coherent]
CoherentRing.Mixin [in coherent]
CoherentRing.Pack [in coherent]
Composable [in refinements]


D

DvdRing.Class [in dvdring]
DvdRing.DivDvd [in dvdring]
DvdRing.DivNDvd [in dvdring]
DvdRing.Mixin [in dvdring]
DvdRing.Pack [in dvdring]


E

EDR.Class [in edr]
EDR.Mixin [in edr]
EDR.Pack [in edr]
EDR.SmithSpec [in edr]
EgcdrSpec [in dvdring]
EgcdrSpec [in kaplansky]
Epimorphism [in fpmod]
EqHrel [in hrel]
EuclideanDomain.Class [in dvdring]
EuclideanDomain.EdivrSpec [in dvdring]
EuclideanDomain.Mixin [in dvdring]
EuclideanDomain.Pack [in dvdring]


F

FPmod [in fpmod]


G

GcdDomain.Class [in dvdring]
GcdDomain.Mixin [in dvdring]
GcdDomain.Pack [in dvdring]
GdcoSpec [in kaplansky]
GdcoSpec0 [in kaplansky]
getparam_rel [in refinements]


I

ImprovePivotQecSpec [in smith]
ImprovePivotRecSpec [in smithpid]
ImprovePivotSpec [in smith]
ImprovePivotSpec [in smithpid]
IntSpec [in stronglydiscrete]
Isomorphism [in fpmod]


M

Monomorphism [in fpmod]
Morphism [in fpmod]


P

param_rel [in refinements]
PID.Class [in dvdring]
PID.Mixin [in dvdring]
PID.Pack [in dvdring]


R

Refinements.Op.add_op [in refinements]
Refinements.Op.block_mx [in refinements]
Refinements.Op.castmx [in refinements]
Refinements.Op.cast_op [in refinements]
Refinements.Op.col [in refinements]
Refinements.Op.col_perm [in refinements]
Refinements.Op.col_mx [in refinements]
Refinements.Op.col' [in refinements]
Refinements.Op.const_mx [in refinements]
Refinements.Op.div_op [in refinements]
Refinements.Op.dlsubmx [in refinements]
Refinements.Op.drsubmx [in refinements]
Refinements.Op.dsubmx [in refinements]
Refinements.Op.dvd_op [in refinements]
Refinements.Op.enorm_op [in refinements]
Refinements.Op.eq_op [in refinements]
Refinements.Op.exp_op [in refinements]
Refinements.Op.find_pivot [in refinements]
Refinements.Op.fun_of_matrix [in refinements]
Refinements.Op.hadd_op [in refinements]
Refinements.Op.heq_op [in refinements]
Refinements.Op.hinv_op [in refinements]
Refinements.Op.hmul_op [in refinements]
Refinements.Op.hone_op [in refinements]
Refinements.Op.hopp_op [in refinements]
Refinements.Op.hscale_op [in refinements]
Refinements.Op.hsub_op [in refinements]
Refinements.Op.hzero_op [in refinements]
Refinements.Op.implem [in refinements]
Refinements.Op.inv_op [in refinements]
Refinements.Op.leq_op [in refinements]
Refinements.Op.lift0 [in refinements]
Refinements.Op.lift0_perm [in refinements]
Refinements.Op.lift0_mx [in refinements]
Refinements.Op.lsubmx [in refinements]
Refinements.Op.lt_op [in refinements]
Refinements.Op.map_mx [in refinements]
Refinements.Op.mul_op [in refinements]
Refinements.Op.odvd_op [in refinements]
Refinements.Op.one_op [in refinements]
Refinements.Op.opp_op [in refinements]
Refinements.Op.row [in refinements]
Refinements.Op.row_perm [in refinements]
Refinements.Op.row_mx [in refinements]
Refinements.Op.row' [in refinements]
Refinements.Op.rsubmx [in refinements]
Refinements.Op.scalar_mx [in refinements]
Refinements.Op.scale_op [in refinements]
Refinements.Op.spec [in refinements]
Refinements.Op.sub_op [in refinements]
Refinements.Op.tperm [in refinements]
Refinements.Op.transpose_op [in refinements]
Refinements.Op.ulsubmx [in refinements]
Refinements.Op.ursubmx [in refinements]
Refinements.Op.usubmx [in refinements]
Refinements.Op.xcol [in refinements]
Refinements.Op.xrow [in refinements]
Refinements.Op.zero_op [in refinements]


S

StronglyDiscrete.Class [in stronglydiscrete]
StronglyDiscrete.Member [in stronglydiscrete]
StronglyDiscrete.Mixin [in stronglydiscrete]
StronglyDiscrete.NMember [in stronglydiscrete]
StronglyDiscrete.Pack [in stronglydiscrete]



Projection Index

B

BezoutDomain.base [in dvdring]
BezoutDomain.bezout [in dvdring]
BezoutDomain.mixin [in dvdring]
BezoutDomain.sort [in dvdring]


C

CoherentRing.base [in coherent]
CoherentRing.dim_ker [in coherent]
CoherentRing.ker [in coherent]
CoherentRing.mixin [in coherent]
CoherentRing.sort [in coherent]
Composable [in refinements]


D

DvdRing.base [in dvdring]
DvdRing.div [in dvdring]
DvdRing.mixin [in dvdring]
DvdRing.sort [in dvdring]


E

EDR.base [in edr]
EDR.mixin [in edr]
EDR.smith [in edr]
EDR.sort [in edr]
EuclideanDomain.base [in dvdring]
EuclideanDomain.ediv [in dvdring]
EuclideanDomain.enorm [in dvdring]
EuclideanDomain.mixin [in dvdring]
EuclideanDomain.sort [in dvdring]


G

GcdDomain.base [in dvdring]
GcdDomain.gcdr [in dvdring]
GcdDomain.mixin [in dvdring]
GcdDomain.sort [in dvdring]
getparam_rel [in refinements]


M

matrix_of_morphism [in fpmod]
morphism_of_iso [in fpmod]
morphism_of_epi [in fpmod]
morphism_of_mono [in fpmod]


N

nbgen [in fpmod]
nbrel [in fpmod]


P

param_rel [in refinements]
PID.base [in dvdring]
PID.mixin [in dvdring]
PID.sort [in dvdring]
pres [in fpmod]


R

Refinements.Op.add_op [in refinements]
Refinements.Op.block_mx [in refinements]
Refinements.Op.castmx [in refinements]
Refinements.Op.cast_op [in refinements]
Refinements.Op.col [in refinements]
Refinements.Op.col_perm [in refinements]
Refinements.Op.col_mx [in refinements]
Refinements.Op.col' [in refinements]
Refinements.Op.const_mx [in refinements]
Refinements.Op.div_op [in refinements]
Refinements.Op.dlsubmx [in refinements]
Refinements.Op.drsubmx [in refinements]
Refinements.Op.dsubmx [in refinements]
Refinements.Op.dvd_op [in refinements]
Refinements.Op.enorm_op [in refinements]
Refinements.Op.eq_op [in refinements]
Refinements.Op.exp_op [in refinements]
Refinements.Op.find_pivot [in refinements]
Refinements.Op.fun_of_matrix [in refinements]
Refinements.Op.hadd_op [in refinements]
Refinements.Op.heq_op [in refinements]
Refinements.Op.hinv_op [in refinements]
Refinements.Op.hmul_op [in refinements]
Refinements.Op.hone_op [in refinements]
Refinements.Op.hopp_op [in refinements]
Refinements.Op.hscale_op [in refinements]
Refinements.Op.hsub_op [in refinements]
Refinements.Op.hzero_op [in refinements]
Refinements.Op.implem [in refinements]
Refinements.Op.inv_op [in refinements]
Refinements.Op.leq_op [in refinements]
Refinements.Op.lift0 [in refinements]
Refinements.Op.lift0_perm [in refinements]
Refinements.Op.lift0_mx [in refinements]
Refinements.Op.lsubmx [in refinements]
Refinements.Op.lt_op [in refinements]
Refinements.Op.map_mx [in refinements]
Refinements.Op.mul_op [in refinements]
Refinements.Op.odvd_op [in refinements]
Refinements.Op.one_op [in refinements]
Refinements.Op.opp_op [in refinements]
Refinements.Op.row [in refinements]
Refinements.Op.row_perm [in refinements]
Refinements.Op.row_mx [in refinements]
Refinements.Op.row' [in refinements]
Refinements.Op.rsubmx [in refinements]
Refinements.Op.scalar_mx [in refinements]
Refinements.Op.scale_op [in refinements]
Refinements.Op.spec [in refinements]
Refinements.Op.sub_op [in refinements]
Refinements.Op.tperm [in refinements]
Refinements.Op.transpose_op [in refinements]
Refinements.Op.ulsubmx [in refinements]
Refinements.Op.ursubmx [in refinements]
Refinements.Op.usubmx [in refinements]
Refinements.Op.xcol [in refinements]
Refinements.Op.xrow [in refinements]
Refinements.Op.zero_op [in refinements]


S

StronglyDiscrete.base [in stronglydiscrete]
StronglyDiscrete.member [in stronglydiscrete]
StronglyDiscrete.mixin [in stronglydiscrete]
StronglyDiscrete.sort [in stronglydiscrete]



Inductive Index

A

adequate_spec [in kaplansky]


B

BezoutDomain.bezout_spec [in dvdring]


C

composable [in refinements]


D

DvdRing.div_spec [in dvdring]


E

EDR.smith_spec [in edr]
egcdr_spec [in dvdring]
egcdr3_spec [in kaplansky]
eq_hrel [in hrel]
EuclideanDomain.edivr_spec [in dvdring]


G

gdco_spec [in kaplansky]
getparam [in refinements]


I

improve_pivot_spec [in smith]
improve_pivot_rec_spec [in smith]
improve_pivot_spec [in smithpid]
improve_pivot_rec_spec [in smithpid]
int_spec [in stronglydiscrete]


P

param [in refinements]


R

Refinements.Op.add [in refinements]
Refinements.Op.block [in refinements]
Refinements.Op.cast_class [in refinements]
Refinements.Op.col_perm_class [in refinements]
Refinements.Op.col_class [in refinements]
Refinements.Op.col_mx_class [in refinements]
Refinements.Op.col'_class [in refinements]
Refinements.Op.const_mx_class [in refinements]
Refinements.Op.div [in refinements]
Refinements.Op.dlsub [in refinements]
Refinements.Op.drsub [in refinements]
Refinements.Op.dsub [in refinements]
Refinements.Op.dvd [in refinements]
Refinements.Op.enorm_of [in refinements]
Refinements.Op.eq [in refinements]
Refinements.Op.exp [in refinements]
Refinements.Op.find_pivot_class [in refinements]
Refinements.Op.fun_of [in refinements]
Refinements.Op.hadd [in refinements]
Refinements.Op.hcast [in refinements]
Refinements.Op.heq [in refinements]
Refinements.Op.hinv [in refinements]
Refinements.Op.hmul [in refinements]
Refinements.Op.hone [in refinements]
Refinements.Op.hopp [in refinements]
Refinements.Op.hscale [in refinements]
Refinements.Op.hsub [in refinements]
Refinements.Op.hzero [in refinements]
Refinements.Op.implem_of [in refinements]
Refinements.Op.inv [in refinements]
Refinements.Op.leq [in refinements]
Refinements.Op.lift0mx_class [in refinements]
Refinements.Op.lift0_perm_class [in refinements]
Refinements.Op.lift0_class [in refinements]
Refinements.Op.lsub [in refinements]
Refinements.Op.lt [in refinements]
Refinements.Op.map_mx_class [in refinements]
Refinements.Op.mul [in refinements]
Refinements.Op.odvd [in refinements]
Refinements.Op.one [in refinements]
Refinements.Op.opp [in refinements]
Refinements.Op.row_perm_class [in refinements]
Refinements.Op.row_class [in refinements]
Refinements.Op.row_mx_class [in refinements]
Refinements.Op.row'_class [in refinements]
Refinements.Op.rsub [in refinements]
Refinements.Op.scalar_mx_class [in refinements]
Refinements.Op.scale [in refinements]
Refinements.Op.spec_of [in refinements]
Refinements.Op.sub [in refinements]
Refinements.Op.tperm_class [in refinements]
Refinements.Op.transpose_class [in refinements]
Refinements.Op.ulsub [in refinements]
Refinements.Op.ursub [in refinements]
Refinements.Op.usub [in refinements]
Refinements.Op.xcol_class [in refinements]
Refinements.Op.xrow_class [in refinements]
Refinements.Op.zero [in refinements]


S

StronglyDiscrete.member_spec [in stronglydiscrete]



Section Index

A

AdequacyEDR [in kaplansky]
AdequacyGdco [in kaplansky]
AdequacyPID [in kaplansky]
AlgOp.AlgOp [in refinements]


B

BezoutCoherent [in coherent]
BezoutDomainTheory [in dvdring]
BezoutDomainTheory.Bezout_mx [in dvdring]
BezoutDomain.ClassDef [in dvdring]
BezoutKrull1 [in kaplansky]
BezoutStronglyDiscrete [in stronglydiscrete]
Bezout_hermite [in kaplansky]
BigOp [in ssrcomplements]
BinetCauchy [in binetcauchy]
bool [in refinements]


C

CoherentRingTheory [in coherent]
CoherentRing.ClassDef [in coherent]
complements [in similar]


D

diag_mx_dvdring [in mxstructure]
diag_mx_idomain [in mxstructure]
diag_mx_seq_comRingType [in mxstructure]
diag_mx_seq2 [in mxstructure]
diag_mx_seq [in mxstructure]
diag_block_comUnitRingType [in mxstructure]
diag_block_comRingType [in mxstructure]
diag_block_ringType2 [in mxstructure]
diag_block_ringType [in mxstructure]
DvdRing [in similar]
DvdRingTheory [in dvdring]
DvdRing.ClassDef [in dvdring]


E

EDR_Theory.Unicity [in edr]
EDR_Theory.Preunicity [in edr]
EDR_Theory.snf_coherent.defs [in edr]
EDR_Theory.snf_coherent [in edr]
EDR_Theory [in edr]
EDR.ClassDef [in edr]
EpiTheory [in fpmod]
EpiTheory.Epi1 [in fpmod]
EquivalentDef [in similar]
EuclideanDomainTheory [in dvdring]
EuclideanDomain.ClassDef [in dvdring]
EuclideanDomain.Mixins.Mixins [in dvdring]


F

Field [in similar]


G

GCDDomainTheory [in dvdring]
GcdDomain.ClassDef [in dvdring]
GUARD [in dvdring]


H

HeterogeneousRelations [in hrel]


I

IntersectionCoherent [in coherent]
IsoTheory [in fpmod]


K

Kaplansky_necc [in kaplansky]
Kaplansky_suff [in kaplansky]
KernelAndCo [in fpmod]
ker_col [in coherent]


L

lifting [in minor]


M

Matrix [in ssrcomplements]
Matrix.matrix_comUnitRingType [in ssrcomplements]
Matrix.matrix_ringType [in ssrcomplements]
Matrix.matrix_raw_type [in ssrcomplements]
minor_char_poly_mx [in minor]
minor_theory [in minor]
minor_def [in minor]
MonoEpi [in fpmod]
MonoTheory [in fpmod]
MonoTheory.Mono1 [in fpmod]
morphismDef [in fpmod]
morphismProperties [in fpmod]
morphismTheory [in fpmod]
morphismTheory.category [in fpmod]
morphismTheory.category.defs [in fpmod]
morphismTheory.category.theory [in fpmod]
morphismTheory.equality [in fpmod]
morphismTheory.general [in fpmod]
morphismTheory.zmodType [in fpmod]
Mx2 [in kaplansky]


P

Parametricity [in refinements]
param_nat [in refinements]
param_option [in refinements]
param_seq [in refinements]
PIDTheory [in dvdring]
PID.ClassDef [in dvdring]
Poly [in ssrcomplements]
prod [in refinements]


R

RPdiv.mon.MonicDivisor [in similar]
RPdiv.mon.MonicDivisor [in ssrcomplements]
RPdiv.RingPseudoDivision [in similar]
RPdiv.RingPseudoDivision [in ssrcomplements]


S

Seq [in ssrcomplements]
Seqeqtype [in ssrcomplements]
SimilarDef [in similar]
smith_theory [in smith]
smith_def [in smith]
smith_def [in smithpid]
smith_fpmod [in fpmod]
Smith2x2 [in kaplansky]
Smith2x2_correctness [in kaplansky]
SquareTriangular [in mxstructure]
SquareTriangular2 [in mxstructure]
StronglyDiscreteTheory [in stronglydiscrete]
StronglyDiscreteTheory.IdealTheory [in stronglydiscrete]
StronglyDiscreteTheory.IdealTheory.IdealIntersection [in stronglydiscrete]
StronglyDiscrete.ClassDef [in stronglydiscrete]
submatrix_char_poly_mx [in minor]
submatrix_theory [in minor]
submatrix_def [in minor]
sum [in refinements]


T

theory [in fpmod]
theory.dsum [in fpmod]
theory.homology [in fpmod]
Triangular [in mxstructure]
TriangularBlock [in mxstructure]



Instance Index

C

composable_comp [in refinements]
composable_proper [in refinements]
composable_sub_proper [in refinements]
comp_hrel_eq_proper [in hrel]
comp_hrel_sub_proper [in hrel]


E

eq_hrel_equiv [in hrel]


G

getparam_None [in refinements]
getparam_nil [in refinements]
getparam_proper [in refinements]
getparam_sub_proper [in refinements]


H

hrespectful_proper [in hrel]
hrespectful_sub_proper [in hrel]


P

param_eq_succ [in refinements]
param_eq_zero [in refinements]
param_if [in refinements]
param_inr [in refinements]
param_inl [in refinements]
param_snd [in refinements]
param_fst [in refinements]
param_pair [in refinements]
param_apply [in refinements]
param_proper [in refinements]
param_sub_proper [in refinements]


R

Refinements.Op.id_cast [in refinements]


S

sub_hrel_partial_order [in hrel]
sub_hrel_proper [in hrel]
sub_hrel_partialorder [in hrel]



Abbreviation Index

B

BezoutDomain.Exports.BezoutDomainMixin [in dvdring]
BezoutDomain.Exports.BezoutDomainType [in dvdring]
BezoutDomain.Exports.bezoutDomainType [in dvdring]


C

cast [in refinements]
CoherentRing.Exports.CoherentRingMixin [in coherent]
CoherentRing.Exports.CoherentRingType [in coherent]
CoherentRing.Exports.coherentRingType [in coherent]


D

DvdRing.Exports.DvdRingMixin [in dvdring]
DvdRing.Exports.DvdRingType [in dvdring]
DvdRing.Exports.dvdRingType [in dvdring]


E

EDR.Exports.EDRMixin [in edr]
EDR.Exports.EDRType [in edr]
EDR.Exports.edrType [in edr]
EuclideanDomain.Exports.EuclidBezoutMixin [in dvdring]
EuclideanDomain.Exports.EuclidDomainMixin [in dvdring]
EuclideanDomain.Exports.EuclidDomainType [in dvdring]
EuclideanDomain.Exports.euclidDomainType [in dvdring]
EuclideanDomain.Exports.EuclidDvdMixin [in dvdring]
EuclideanDomain.Exports.EuclidGCDMixin [in dvdring]
EuclideanDomain.Exports.EuclidGcdMixin [in dvdring]
EuclideanDomain.Exports.EuclidPIDMixin [in dvdring]
EuclideanDomain.Mixins.ediv [in dvdring]
EuclideanDomain.Mixins.norm [in dvdring]


G

GcdDomain.Exports.GcdDomainMixin [in dvdring]
GcdDomain.Exports.GcdDomainType [in dvdring]
GcdDomain.Exports.gcdDomainType [in dvdring]


P

PID.Exports.PIDMixin [in dvdring]
PID.Exports.PIDType [in dvdring]
PID.Exports.pidType [in dvdring]


S

StronglyDiscrete.Exports.StronglyDiscreteMixin [in stronglydiscrete]
StronglyDiscrete.Exports.StronglyDiscreteType [in stronglydiscrete]
StronglyDiscrete.Exports.stronglyDiscreteType [in stronglydiscrete]



Definition Index

A

Acc_rect_dep [in smithpid]
ACC_GCD [in dvdring]
acc_dep [in dvdring]
addid [in stronglydiscrete]
addmor [in fpmod]
AlgOp.divr [in refinements]
AlgOp.subr [in refinements]


B

bcap [in coherent]
bcap_wr [in coherent]
bcap_wl [in coherent]
bdim_cap [in coherent]
bezout [in dvdring]
BezoutDomain.choiceType [in dvdring]
BezoutDomain.class [in dvdring]
BezoutDomain.clone [in dvdring]
BezoutDomain.comRingType [in dvdring]
BezoutDomain.comUnitRingType [in dvdring]
BezoutDomain.dvdRingType [in dvdring]
BezoutDomain.eqType [in dvdring]
BezoutDomain.gcdDomainType [in dvdring]
BezoutDomain.idomainType [in dvdring]
BezoutDomain.pack [in dvdring]
BezoutDomain.ringType [in dvdring]
BezoutDomain.unitRingType [in dvdring]
BezoutDomain.zmodType [in dvdring]
bezoutMixin [in edr]
bezoutType [in edr]
Bezout_step [in dvdring]
Bezout_mx [in dvdring]
bezout_coherentType [in coherent]
bezout_coherentMixin [in coherent]
bezout_stronglyDiscreteType [in stronglydiscrete]
bezout_stronglyDiscreteMixin [in stronglydiscrete]
bezout_edr [in edr]
bmember [in stronglydiscrete]
bool_if [in refinements]


C

cap_wr [in coherent]
cap_wl [in coherent]
coherentMixin [in edr]
CoherentRing.choiceType [in coherent]
CoherentRing.class [in coherent]
CoherentRing.clone [in coherent]
CoherentRing.comRingType [in coherent]
CoherentRing.comUnitRingType [in coherent]
CoherentRing.eqType [in coherent]
CoherentRing.idomainType [in coherent]
CoherentRing.pack [in coherent]
CoherentRing.ringType [in coherent]
CoherentRing.stronglyDiscreteType [in coherent]
CoherentRing.unitRingType [in coherent]
CoherentRing.zmodType [in coherent]
coherentType [in edr]
coker [in fpmod]
cokermx [in edr]
col_ebase [in edr]
combine_step [in dvdring]
combine_mx [in dvdring]
comp_hrel [in hrel]
coprimer [in dvdring]


D

diag [in edr]
diag_mx_seq [in mxstructure]
diag_block_mx [in mxstructure]
diag_block_mx_rec [in mxstructure]
diag_mx [in edr]
dim_int [in coherent]
dim_ker_c [in coherent]
dim_ker [in coherent]
divid [in stronglydiscrete]
divmx [in coherent]
divr [in dvdring]
dsum [in fpmod]
dvdmx [in coherent]
dvdr [in dvdring]
DvdRing.choiceType [in dvdring]
DvdRing.class [in dvdring]
DvdRing.clone [in dvdring]
DvdRing.comRingType [in dvdring]
DvdRing.comUnitRingType [in dvdring]
DvdRing.eqType [in dvdring]
DvdRing.idomainType [in dvdring]
DvdRing.pack [in dvdring]
DvdRing.ringType [in dvdring]
DvdRing.unitRingType [in dvdring]
DvdRing.zmodType [in dvdring]


E

edivr [in dvdring]
EDR.choiceType [in edr]
EDR.class [in edr]
EDR.clone [in edr]
EDR.comRingType [in edr]
EDR.comUnitRingType [in edr]
EDR.dvdRingType [in edr]
EDR.eqType [in edr]
EDR.idomainType [in edr]
EDR.pack [in edr]
EDR.ringType [in edr]
EDR.unitRingType [in edr]
EDR.zmodType [in edr]
egcdr [in dvdring]
egcdr3 [in kaplansky]
enorm [in dvdring]
epimorphism [in fpmod]
epi_of_coker [in fpmod]
epi_of_iso [in fpmod]
epi_of [in fpmod]
eqd [in dvdring]
eqid [in stronglydiscrete]
eqmor [in fpmod]
equivalent [in similar]
EuclideanDomain.bezoutDomainType [in dvdring]
EuclideanDomain.choiceType [in dvdring]
EuclideanDomain.class [in dvdring]
EuclideanDomain.clone [in dvdring]
EuclideanDomain.comRingType [in dvdring]
EuclideanDomain.comUnitRingType [in dvdring]
EuclideanDomain.dvdRingType [in dvdring]
EuclideanDomain.eqType [in dvdring]
EuclideanDomain.EuclidBezoutMixin [in dvdring]
EuclideanDomain.EuclidDvdMixin [in dvdring]
EuclideanDomain.EuclidGCDMixin [in dvdring]
EuclideanDomain.EuclidGcdMixin [in dvdring]
EuclideanDomain.EuclidPIDMixin [in dvdring]
EuclideanDomain.gcdDomainType [in dvdring]
EuclideanDomain.idomainType [in dvdring]
EuclideanDomain.Mixins.acc_gcd [in dvdring]
EuclideanDomain.Mixins.div [in dvdring]
EuclideanDomain.Mixins.egcd [in dvdring]
EuclideanDomain.Mixins.egcd_rec [in dvdring]
EuclideanDomain.Mixins.EuclidBezout [in dvdring]
EuclideanDomain.Mixins.EuclidDvd [in dvdring]
EuclideanDomain.Mixins.euclidDvdRing [in dvdring]
EuclideanDomain.Mixins.EuclidGcd [in dvdring]
EuclideanDomain.Mixins.EuclidGCD [in dvdring]
EuclideanDomain.Mixins.EuclidPID [in dvdring]
EuclideanDomain.Mixins.gcd [in dvdring]
EuclideanDomain.Mixins.GCD [in dvdring]
EuclideanDomain.Mixins.odiv [in dvdring]
EuclideanDomain.Mixins.R_gcdDomain [in dvdring]
EuclideanDomain.Mixins.R_idom [in dvdring]
EuclideanDomain.Mixins.R_comunit [in dvdring]
EuclideanDomain.Mixins.R_unit [in dvdring]
EuclideanDomain.Mixins.R_com [in dvdring]
EuclideanDomain.Mixins.R_ring [in dvdring]
EuclideanDomain.Mixins.R_zmod [in dvdring]
EuclideanDomain.Mixins.R_choiceType [in dvdring]
EuclideanDomain.Mixins.R_eqType [in dvdring]
EuclideanDomain.pack [in dvdring]
EuclideanDomain.pidType [in dvdring]
EuclideanDomain.ringType [in dvdring]
EuclideanDomain.unitRingType [in dvdring]
EuclideanDomain.zmodType [in dvdring]
euclidEDRMixin [in smith]
euclidEDRType [in smith]


F

factor [in fpmod]
fpmod_of [in fpmod]
fun_hrel [in hrel]


G

GCD [in dvdring]
GcdDomain.choiceType [in dvdring]
GcdDomain.class [in dvdring]
GcdDomain.clone [in dvdring]
GcdDomain.comRingType [in dvdring]
GcdDomain.comUnitRingType [in dvdring]
GcdDomain.dvdRingType [in dvdring]
GcdDomain.eqType [in dvdring]
GcdDomain.idomainType [in dvdring]
GcdDomain.pack [in dvdring]
GcdDomain.ringType [in dvdring]
GcdDomain.unitRingType [in dvdring]
GcdDomain.zmodType [in dvdring]
gcdMixin [in edr]
gcdr [in dvdring]
gcdsr [in dvdring]
gcdType [in edr]
gcd_edr [in edr]
gdcoEDRMixin [in kaplansky]
gdcoEDRType [in kaplansky]
gdco_smith [in kaplansky]
gdco_kap [in kaplansky]
good [in binetcauchy]
guarded [in dvdring]


H

hermite [in kaplansky]
homology [in fpmod]
homology_alt_pres [in fpmod]
hrespectful [in hrel]


I

idm [in fpmod]
idm_iso [in fpmod]
improve_pivot_recR [in smith]
improve_pivot [in smith]
improve_pivot_rec [in smith]
improve_pivot [in smithpid]
improve_pivot_rec [in smithpid]
injm [in fpmod]
inj1 [in fpmod]
inj1_mono [in fpmod]
inj2 [in fpmod]
inj2_mono [in fpmod]
int_coherentType [in coherent]
int_coherentMixin [in coherent]
invmor [in fpmod]
inv_g_of_fx [in binetcauchy]
irredr [in dvdring]
isom [in fpmod]
isomorphism [in fpmod]
isomorphisms [in fpmod]
iso_of_isom [in fpmod]
iso_of_me [in fpmod]
iso_of_kc [in fpmod]
is_triangular_mx [in mxstructure]
is_coker [in fpmod]
is_kernel [in fpmod]
is_epi [in fpmod]
is_mono [in fpmod]


K

kapW [in kaplansky]
kap_smith [in kaplansky]
ker [in coherent]
kermod [in fpmod]
kermx [in edr]
kernel [in fpmod]
ker_c_int [in coherent]
ker_c [in coherent]
ker_mod [in coherent]
krull1EDRMixin [in kaplansky]
krull1EDRType [in kaplansky]
krull1_smith [in kaplansky]
krull1_gdco [in kaplansky]


L

lcmr [in dvdring]
lcmsr [in dvdring]
lift [in fpmod]
lift_pred [in minor]
lower_triangular_mx [in mxstructure]
lower_part_mx [in mxstructure]


M

member [in stronglydiscrete]
member_spec [in stronglydiscrete]
minor [in minor]
modr [in dvdring]
monomorphism [in fpmod]
mono_of_kernel [in fpmod]
mono_of_iso [in fpmod]
mono_of_mx [in fpmod]
mono_of [in fpmod]
morphism_zmodType [in fpmod]
morphism_zmodMixin [in fpmod]
morphism_choiceType [in fpmod]
morphism_choiceMixin [in fpmod]
morphism_eqType [in fpmod]
morphism_eqMixin [in fpmod]
morphism_subType [in fpmod]
Morphism1 [in fpmod]
mor_of_mx [in fpmod]
mulid [in stronglydiscrete]
mulmor [in fpmod]
mxrank [in edr]
mx2 [in kaplansky]


O

odivr [in dvdring]
ofun_hrel [in hrel]
ohrel [in refinements]
oppmor [in fpmod]


P

perm_f [in binetcauchy]
pidEDRMixin [in smithpid]
pidEDRMixin [in kaplansky]
pidEDRType [in smithpid]
pidEDRType [in kaplansky]
pid_smith [in kaplansky]
PID.bezoutDomainType [in dvdring]
PID.choiceType [in dvdring]
PID.class [in dvdring]
PID.clone [in dvdring]
PID.comRingType [in dvdring]
PID.comUnitRingType [in dvdring]
PID.dvdRingType [in dvdring]
PID.eqType [in dvdring]
PID.gcdDomainType [in dvdring]
PID.idomainType [in dvdring]
PID.pack [in dvdring]
PID.ringType [in dvdring]
PID.unitRingType [in dvdring]
PID.zmodType [in dvdring]
pminor [in minor]
primer [in dvdring]
principal [in dvdring]
principal_w2 [in dvdring]
principal_w1 [in dvdring]
principal_gen [in dvdring]
prod_hrel [in refinements]
proj1 [in fpmod]
proj1_epi [in fpmod]
proj2 [in fpmod]
proj2_epi [in fpmod]
proj2_proof [in fpmod]


Q

quot_by [in fpmod]


R

Refinements.Op.implem_id [in refinements]
Refinements.Op.spec_id [in refinements]
row_ebase [in edr]
RPdiv.id_converse [in similar]
RPdiv.id_converse_def [in similar]
RPdiv.id_converse [in ssrcomplements]
RPdiv.id_converse_def [in ssrcomplements]
RPdiv.phi [in similar]
RPdiv.phi [in ssrcomplements]
RPdiv.phi_inv [in similar]
RPdiv.phi_rmorphism [in similar]
RPdiv.phi_inv [in ssrcomplements]
RPdiv.phi_rmorphism [in ssrcomplements]
RPdiv.rdivp_l [in similar]
RPdiv.rdivp_l [in ssrcomplements]
RPdiv.rdvdp_l [in similar]
RPdiv.rdvdp_l [in ssrcomplements]
RPdiv.redivp_l [in similar]
RPdiv.redivp_l [in ssrcomplements]
RPdiv.rmodp_l [in similar]
RPdiv.rmodp_l [in ssrcomplements]
RPdiv.rmultp_l [in similar]
RPdiv.rmultp_l [in ssrcomplements]
RPdiv.rscalp_l [in similar]
RPdiv.rscalp_l [in ssrcomplements]


S

same_codom [in binetcauchy]
same_codomb [in binetcauchy]
sdvdr [in dvdring]
sdvdr_ind [in dvdring]
sdvdr_rec [in dvdring]
sdvdr_rect [in dvdring]
seq_hrel [in refinements]
similar [in similar]
size_sum [in mxstructure]
size_sum_rec [in mxstructure]
Smith [in smith]
Smith [in smithpid]
smith [in edr]
smithm [in fpmod]
smithmxn [in kaplansky]
smithmxn_rec [in kaplansky]
smithm_inv [in fpmod]
smith_iso [in fpmod]
smith_seq [in edr]
smith_spec [in edr]
smith1xn [in kaplansky]
smith2xn [in kaplansky]
source [in fpmod]
source_of_mx [in fpmod]
strictf [in binetcauchy]
strict_from_f [in binetcauchy]
strict_from [in binetcauchy]
stronglyDiscreteMixin [in edr]
stronglyDiscreteType [in edr]
StronglyDiscrete.choiceType [in stronglydiscrete]
StronglyDiscrete.class [in stronglydiscrete]
StronglyDiscrete.clone [in stronglydiscrete]
StronglyDiscrete.comRingType [in stronglydiscrete]
StronglyDiscrete.comUnitRingType [in stronglydiscrete]
StronglyDiscrete.eqType [in stronglydiscrete]
StronglyDiscrete.idomainType [in stronglydiscrete]
StronglyDiscrete.pack [in stronglydiscrete]
StronglyDiscrete.ringType [in stronglydiscrete]
StronglyDiscrete.unitRingType [in stronglydiscrete]
StronglyDiscrete.zmodType [in stronglydiscrete]
subid [in stronglydiscrete]
submatrix [in minor]
sub_hrel [in hrel]
sum_elim [in refinements]
sum_hrel [in refinements]
surjm [in fpmod]


T

target [in fpmod]
tilt [in binetcauchy]


U

unitmxEE [in smith]
unitmxEE [in smithpid]
upper_triangular_mx [in mxstructure]
upper_part_mx [in mxstructure]


W

weight [in binetcauchy]


Z

zeromor [in fpmod]



Record Index

B

BezoutDomain.class_of [in dvdring]
BezoutDomain.mixin_of [in dvdring]
BezoutDomain.type [in dvdring]


C

CoherentRing.class_of [in coherent]
CoherentRing.mixin_of [in coherent]
CoherentRing.type [in coherent]
composable [in refinements]


D

DvdRing.class_of [in dvdring]
DvdRing.mixin_of [in dvdring]
DvdRing.type [in dvdring]


E

EDR.class_of [in edr]
EDR.mixin_of [in edr]
EDR.type [in edr]
epimorphism_of [in fpmod]
EuclideanDomain.class_of [in dvdring]
EuclideanDomain.mixin_of [in dvdring]
EuclideanDomain.type [in dvdring]


F

fpmod [in fpmod]


G

GcdDomain.class_of [in dvdring]
GcdDomain.mixin_of [in dvdring]
GcdDomain.type [in dvdring]
getparam [in refinements]


I

isomorphism_of [in fpmod]


M

monomorphism_of [in fpmod]
morphism_of [in fpmod]


P

param [in refinements]
PID.class_of [in dvdring]
PID.mixin_of [in dvdring]
PID.type [in dvdring]


R

Refinements.Op.add [in refinements]
Refinements.Op.block [in refinements]
Refinements.Op.cast_class [in refinements]
Refinements.Op.col_perm_class [in refinements]
Refinements.Op.col_class [in refinements]
Refinements.Op.col_mx_class [in refinements]
Refinements.Op.col'_class [in refinements]
Refinements.Op.const_mx_class [in refinements]
Refinements.Op.div [in refinements]
Refinements.Op.dlsub [in refinements]
Refinements.Op.drsub [in refinements]
Refinements.Op.dsub [in refinements]
Refinements.Op.dvd [in refinements]
Refinements.Op.enorm_of [in refinements]
Refinements.Op.eq [in refinements]
Refinements.Op.exp [in refinements]
Refinements.Op.find_pivot_class [in refinements]
Refinements.Op.fun_of [in refinements]
Refinements.Op.hadd [in refinements]
Refinements.Op.hcast [in refinements]
Refinements.Op.heq [in refinements]
Refinements.Op.hinv [in refinements]
Refinements.Op.hmul [in refinements]
Refinements.Op.hone [in refinements]
Refinements.Op.hopp [in refinements]
Refinements.Op.hscale [in refinements]
Refinements.Op.hsub [in refinements]
Refinements.Op.hzero [in refinements]
Refinements.Op.implem_of [in refinements]
Refinements.Op.inv [in refinements]
Refinements.Op.leq [in refinements]
Refinements.Op.lift0mx_class [in refinements]
Refinements.Op.lift0_perm_class [in refinements]
Refinements.Op.lift0_class [in refinements]
Refinements.Op.lsub [in refinements]
Refinements.Op.lt [in refinements]
Refinements.Op.map_mx_class [in refinements]
Refinements.Op.mul [in refinements]
Refinements.Op.odvd [in refinements]
Refinements.Op.one [in refinements]
Refinements.Op.opp [in refinements]
Refinements.Op.row_perm_class [in refinements]
Refinements.Op.row_class [in refinements]
Refinements.Op.row_mx_class [in refinements]
Refinements.Op.row'_class [in refinements]
Refinements.Op.rsub [in refinements]
Refinements.Op.scalar_mx_class [in refinements]
Refinements.Op.scale [in refinements]
Refinements.Op.spec_of [in refinements]
Refinements.Op.sub [in refinements]
Refinements.Op.tperm_class [in refinements]
Refinements.Op.transpose_class [in refinements]
Refinements.Op.ulsub [in refinements]
Refinements.Op.ursub [in refinements]
Refinements.Op.usub [in refinements]
Refinements.Op.xcol_class [in refinements]
Refinements.Op.xrow_class [in refinements]
Refinements.Op.zero [in refinements]


S

StronglyDiscrete.class_of [in stronglydiscrete]
StronglyDiscrete.mixin_of [in stronglydiscrete]
StronglyDiscrete.type [in stronglydiscrete]



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2004 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (152 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (25 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (213 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (15 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (687 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (109 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (101 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (76 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (109 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (27 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (32 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (368 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (90 entries)

This page has been generated by coqdoc