From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/index_global_C.html | 898 ++++++++++++++++++++++----------------- 1 file changed, 506 insertions(+), 392 deletions(-) (limited to 'docs/htmldoc/index_global_C.html') diff --git a/docs/htmldoc/index_global_C.html b/docs/htmldoc/index_global_C.html index 715d2ba..911c265 100644 --- a/docs/htmldoc/index_global_C.html +++ b/docs/htmldoc/index_global_C.html @@ -4,7 +4,7 @@ -mathcomp.ssreflect.tuple +mathcomp.test_suite.hierarchy_test @@ -47,7 +47,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -79,14 +79,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -111,7 +111,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -143,7 +143,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -175,7 +175,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -207,7 +207,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -239,7 +239,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -271,7 +271,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -303,14 +303,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -335,7 +335,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -367,7 +367,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -399,7 +399,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -431,14 +431,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -463,7 +463,7 @@ Z _ other -(185 entries) +(189 entries)

C

@@ -567,7 +567,6 @@ CardGL [section, in mathcomp.algebra.mxalgebra]
CardGL.F [variable, in mathcomp.algebra.mxalgebra]
cardG_gt1 [lemma, in mathcomp.fingroup.fingroup]
-cardG_gt0_reduced [definition, in mathcomp.fingroup.fingroup]
cardG_gt0 [lemma, in mathcomp.fingroup.fingroup]
cardID [lemma, in mathcomp.ssreflect.fintype]
cardIg_divn [lemma, in mathcomp.fingroup.fingroup]
@@ -703,8 +702,9 @@ card_ffun [lemma, in mathcomp.ssreflect.finfun]
card_ffun_on [lemma, in mathcomp.ssreflect.finfun]
card_pffun_on [lemma, in mathcomp.ssreflect.finfun]
-card_family [lemma, in mathcomp.ssreflect.finfun]
card_pfamily [lemma, in mathcomp.ssreflect.finfun]
+card_dep_ffun [lemma, in mathcomp.ssreflect.finfun]
+card_family [lemma, in mathcomp.ssreflect.finfun]
card_rVabelem [lemma, in mathcomp.character.mxabelem]
card_abelem_rV [lemma, in mathcomp.character.mxabelem]
card_rowg [lemma, in mathcomp.character.mxabelem]
@@ -1170,6 +1170,7 @@ cfIirr [definition, in mathcomp.character.character]
cfIirrE [lemma, in mathcomp.character.character]
cfIirrPE [lemma, in mathcomp.character.character]
+cfIirr_key [lemma, in mathcomp.character.character]
cfInd [definition, in mathcomp.character.classfun]
cfIndE [lemma, in mathcomp.character.classfun]
cfIndEout [lemma, in mathcomp.character.classfun]
@@ -1490,7 +1491,7 @@ ChangeOfField.OneRepresentation.n [variable, in mathcomp.character.mxrepresentation]
ChangeOfField.OneRepresentation.rG [variable, in mathcomp.character.mxrepresentation]
ChangeOfField.rF [variable, in mathcomp.character.mxrepresentation]
-_ ^f (ring_scope) [notation, in mathcomp.character.mxrepresentation]
+_ ^f (ring_scope) [notation, in mathcomp.character.mxrepresentation]
ChangeOfRing [section, in mathcomp.character.mxrepresentation]
ChangeOfRing.aR [variable, in mathcomp.character.mxrepresentation]
ChangeOfRing.f [variable, in mathcomp.character.mxrepresentation]
@@ -1500,14 +1501,14 @@ ChangeOfRing.OneRepresentation.n [variable, in mathcomp.character.mxrepresentation]
ChangeOfRing.OneRepresentation.rG [variable, in mathcomp.character.mxrepresentation]
ChangeOfRing.rR [variable, in mathcomp.character.mxrepresentation]
-_ ^f (ring_scope) [notation, in mathcomp.character.mxrepresentation]
+_ ^f (ring_scope) [notation, in mathcomp.character.mxrepresentation]
Char [section, in mathcomp.character.character]
character [definition, in mathcomp.character.character]
character [library]
characteristic [definition, in mathcomp.fingroup.automorphism]
Characteristicity [section, in mathcomp.fingroup.automorphism]
Characteristicity.gT [variable, in mathcomp.fingroup.automorphism]
-_ \char _ [notation, in mathcomp.fingroup.automorphism]
+_ \char _ [notation, in mathcomp.fingroup.automorphism]
character_table_unit [lemma, in mathcomp.character.character]
character_table [definition, in mathcomp.character.character]
character_key [lemma, in mathcomp.character.character]
@@ -1597,6 +1598,7 @@ Chinese.m2 [variable, in mathcomp.algebra.intdiv]
Choice [module, in mathcomp.ssreflect.choice]
choice [library]
+choiceMixin [lemma, in mathcomp.ssreflect.finfun]
ChoiceTheory [section, in mathcomp.ssreflect.choice]
ChoiceTheory.OneType [section, in mathcomp.ssreflect.choice]
ChoiceTheory.OneType.CanChoice [section, in mathcomp.ssreflect.choice]
@@ -1623,8 +1625,8 @@ Choice.Exports.choiceMixin [abbreviation, in mathcomp.ssreflect.choice]
Choice.Exports.ChoiceType [abbreviation, in mathcomp.ssreflect.choice]
Choice.Exports.choiceType [abbreviation, in mathcomp.ssreflect.choice]
-[ choiceType of _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
-[ choiceType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
+[ choiceType of _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
+[ choiceType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
Choice.find [projection, in mathcomp.ssreflect.choice]
Choice.InternalTheory [module, in mathcomp.ssreflect.choice]
Choice.InternalTheory.complete [lemma, in mathcomp.ssreflect.choice]
@@ -1686,7 +1688,7 @@ classfun_key [lemma, in mathcomp.character.classfun]
ClassFun.G [variable, in mathcomp.character.classfun]
ClassFun.gT [variable, in mathcomp.character.classfun]
-'1_ _ [notation, in mathcomp.character.classfun]
+'1_ _ [notation, in mathcomp.character.classfun]
classGidl [lemma, in mathcomp.fingroup.fingroup]
classGidr [lemma, in mathcomp.fingroup.fingroup]
classg_base_center [lemma, in mathcomp.character.mxrepresentation]
@@ -1751,15 +1753,113 @@ clone_aspace [definition, in mathcomp.field.falgebra]
closed [abbreviation, in mathcomp.ssreflect.fingraph]
ClosedField [section, in mathcomp.algebra.poly]
-ClosedFieldQE [section, in mathcomp.field.closed_field]
-ClosedFieldQE.axiom [variable, in mathcomp.field.closed_field]
-ClosedFieldQE.F [variable, in mathcomp.field.closed_field]
+ClosedFieldQE [module, in mathcomp.field.closed_field]
+ClosedFieldQE.abstrX [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.abstrXP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.abstrX_bigmul [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.abstrX_mulM [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.abstrX1 [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.amulXnT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.bigmap_id [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.bind [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.ClosedFieldQE [section, in mathcomp.field.closed_field]
+ClosedFieldQE.ClosedFieldQE.F [variable, in mathcomp.field.closed_field]
+ClosedFieldQE.ClosedFieldQE.F_closed [variable, in mathcomp.field.closed_field]
+_ ->_ _ _ [notation, in mathcomp.field.closed_field]
+'if _ then _ else _ [notation, in mathcomp.field.closed_field]
+'let _ <- _ ; _ [notation, in mathcomp.field.closed_field]
+ClosedFieldQE.cps [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.cpsif [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.eval [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_bigmul [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_poly1 [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_poly_mulM [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_natmulpT [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_opppT [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_mulpT [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_sumpT [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_amulXnT [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_lift [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.eval_poly [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.ex_elim_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.ex_elim [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.ex_elim_seq_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.ex_elim_seqP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.ex_elim_seq [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.fF [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.holds_ex_elim [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.holds_conjn [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.holds_conj [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.isnull [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.isnullP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.isnull_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.lead_coefT_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.lead_coefTP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.lead_coefT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.lift [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.lt_sizeT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.Mixin [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.mulpT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.natmulpT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.opppT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.polyF [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.qf [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.qf_cps_if [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.qf_cps_bind [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.qf_cps_ret [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.qf_cps [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.qf_red_cps [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.qf_eval [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.qf_simpl [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rabstrX [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.ramulXnT [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rdivpT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rdvdpT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.redivpT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.redivpTP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.redivpT_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.redivp_rec_loopP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.redivp_rec_loopT_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.redivp_rec_loopTP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.redivp_rec_loop [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.redivp_rec_loopT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.ret [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpTP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpTs [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpTsP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpTs_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdpT_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdp_loopT_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdp_loopP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdp_loopT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rgcdp_loop [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcopT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcopTP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcopT_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcop_recT_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcop_recTP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rgdcop_recT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rmodpT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rmulpT [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rpoly [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rpoly_map_mul [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rscalpT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.rseq_poly_map [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rsumpT [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.rterm [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.sizeT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.sizeTP [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.sizeT_qf [lemma, in mathcomp.field.closed_field]
+ClosedFieldQE.sumpT [definition, in mathcomp.field.closed_field]
+ClosedFieldQE.tF [abbreviation, in mathcomp.field.closed_field]
+ClosedFieldQE.wf_ex_elim [lemma, in mathcomp.field.closed_field]
ClosedField.closedF [variable, in mathcomp.algebra.poly]
ClosedField.F [variable, in mathcomp.algebra.poly]
closed_field_poly_normal [lemma, in mathcomp.algebra.poly]
closed_nonrootP [lemma, in mathcomp.algebra.poly]
closed_rootP [lemma, in mathcomp.algebra.poly]
-closed_fields_QEMixin [definition, in mathcomp.field.closed_field]
+closed_field_QEMixin [abbreviation, in mathcomp.field.closed_field]
closed_connect [lemma, in mathcomp.ssreflect.fingraph]
closed_mem [definition, in mathcomp.ssreflect.fingraph]
closed_field [library]
@@ -1773,8 +1873,8 @@ Closure.K [variable, in mathcomp.field.falgebra]
Closure.sym_e [variable, in mathcomp.ssreflect.fingraph]
Closure.T [variable, in mathcomp.ssreflect.fingraph]
-<< _ ; _ >> (vspace_scope) [notation, in mathcomp.field.falgebra]
-<< _ & _ >> (vspace_scope) [notation, in mathcomp.field.falgebra]
+<< _ ; _ >> (vspace_scope) [notation, in mathcomp.field.falgebra]
+<< _ & _ >> (vspace_scope) [notation, in mathcomp.field.falgebra]
CnatEint [lemma, in mathcomp.field.algC]
CnatP [lemma, in mathcomp.field.algC]
Cnat_aut [lemma, in mathcomp.field.algC]
@@ -1805,13 +1905,14 @@ CodeSeq.decode_rec [definition, in mathcomp.ssreflect.choice]
CodeSeq.gtn_decode [lemma, in mathcomp.ssreflect.choice]
CodeSeq.ltn_code [lemma, in mathcomp.ssreflect.choice]
-[ rec _ , _ , _ ] [notation, in mathcomp.ssreflect.choice]
+[ rec _ , _ , _ ] [notation, in mathcomp.ssreflect.choice]
codom [definition, in mathcomp.ssreflect.fintype]
codomE [lemma, in mathcomp.ssreflect.fintype]
codomP [lemma, in mathcomp.ssreflect.fintype]
codom_val [lemma, in mathcomp.ssreflect.fintype]
codom_f [lemma, in mathcomp.ssreflect.fintype]
codom_ffun [lemma, in mathcomp.ssreflect.finfun]
+codom_tffun [lemma, in mathcomp.ssreflect.finfun]
coefB [lemma, in mathcomp.algebra.poly]
coefC [lemma, in mathcomp.algebra.poly]
coefCM [lemma, in mathcomp.algebra.poly]
@@ -1837,6 +1938,7 @@ coef_rVpoly_ord [lemma, in mathcomp.algebra.mxpoly]
coef_rVpoly [lemma, in mathcomp.algebra.mxpoly]
coef_swapXY [lemma, in mathcomp.algebra.polyXY]
+coef_comp_poly [lemma, in mathcomp.algebra.poly]
coef_map [lemma, in mathcomp.algebra.poly]
coef_map_id0 [lemma, in mathcomp.algebra.poly]
coef_nderivn [lemma, in mathcomp.algebra.poly]
@@ -2009,10 +2111,13 @@ CompAct.gT [variable, in mathcomp.fingroup.action]
CompAct.rT [variable, in mathcomp.fingroup.action]
CompAct.to [variable, in mathcomp.fingroup.action]
+companionmx [definition, in mathcomp.algebra.mxpoly]
+companionmxK [lemma, in mathcomp.algebra.mxpoly]
+companion_map_poly [lemma, in mathcomp.algebra.mxpoly]
comparable [definition, in mathcomp.ssreflect.eqtype]
-comparableClass [definition, in mathcomp.ssreflect.eqtype]
+comparableMixin [definition, in mathcomp.ssreflect.eqtype]
ComparableType [section, in mathcomp.ssreflect.eqtype]
-ComparableType.Hcompare [variable, in mathcomp.ssreflect.eqtype]
+ComparableType.compare_T [variable, in mathcomp.ssreflect.eqtype]
ComparableType.T [variable, in mathcomp.ssreflect.eqtype]
compareb [definition, in mathcomp.ssreflect.eqtype]
CompareNatEq [constructor, in mathcomp.ssreflect.ssrnat]
@@ -2073,6 +2178,7 @@ comp_is_action [lemma, in mathcomp.fingroup.action]
comp_act [definition, in mathcomp.fingroup.action]
comp_poly2_eq0 [lemma, in mathcomp.algebra.poly]
+comp_poly_eq0 [lemma, in mathcomp.algebra.poly]
comp_polyA [lemma, in mathcomp.algebra.poly]
comp_polyM [lemma, in mathcomp.algebra.poly]
comp_poly_multiplicative [lemma, in mathcomp.algebra.poly]
@@ -2251,7 +2357,7 @@ ConsttInertiaBijection.H [variable, in mathcomp.character.inertia]
ConsttInertiaBijection.nsHG [variable, in mathcomp.character.inertia]
ConsttInertiaBijection.t [variable, in mathcomp.character.inertia]
-` T (group_scope) [notation, in mathcomp.character.inertia]
+` T (group_scope) [notation, in mathcomp.character.inertia]
consttJ [lemma, in mathcomp.solvable.pgroup]
consttM [lemma, in mathcomp.solvable.pgroup]
consttNK [lemma, in mathcomp.solvable.pgroup]
@@ -2274,7 +2380,8 @@ const_mx_is_additive [lemma, in mathcomp.algebra.matrix]
const_mx [definition, in mathcomp.algebra.matrix]
const_mx_key [lemma, in mathcomp.algebra.matrix]
-cons_pfactor [definition, in mathcomp.ssreflect.prime]
+cons_perms [abbreviation, in mathcomp.ssreflect.seq]
+cons_perms_ [definition, in mathcomp.ssreflect.seq]
cons_uniq [lemma, in mathcomp.ssreflect.seq]
cons_poly_def [lemma, in mathcomp.algebra.poly]
cons_poly [definition, in mathcomp.algebra.poly]
@@ -2288,8 +2395,13 @@ contraTeq [lemma, in mathcomp.ssreflect.eqtype]
contraTneq [lemma, in mathcomp.ssreflect.eqtype]
contra_orbit [lemma, in mathcomp.fingroup.action]
+contra_eq_neq [lemma, in mathcomp.ssreflect.eqtype]
+contra_neq_eq [lemma, in mathcomp.ssreflect.eqtype]
contra_neq [lemma, in mathcomp.ssreflect.eqtype]
contra_eq [lemma, in mathcomp.ssreflect.eqtype]
+contra_neqT [lemma, in mathcomp.ssreflect.eqtype]
+contra_neqF [lemma, in mathcomp.ssreflect.eqtype]
+contra_neqN [lemma, in mathcomp.ssreflect.eqtype]
contra_eqT [lemma, in mathcomp.ssreflect.eqtype]
contra_eqF [lemma, in mathcomp.ssreflect.eqtype]
contra_eqN [lemma, in mathcomp.ssreflect.eqtype]
@@ -2395,7 +2507,7 @@ CosetOfGroupTheory.InverseImage.G [variable, in mathcomp.fingroup.quotient]
CosetOfGroupTheory.InverseImage.Kbar [variable, in mathcomp.fingroup.quotient]
CosetOfGroupTheory.InverseImage.nHG [variable, in mathcomp.fingroup.quotient]
-_ / _ (Group_scope) [notation, in mathcomp.fingroup.quotient]
+_ / _ (Group_scope) [notation, in mathcomp.fingroup.quotient]
cosetP [lemma, in mathcomp.fingroup.quotient]
cosetpreK [lemma, in mathcomp.fingroup.quotient]
cosetpreM [lemma, in mathcomp.fingroup.quotient]
@@ -2449,8 +2561,8 @@ Coset.G [variable, in mathcomp.character.classfun]
Coset.gT [variable, in mathcomp.character.character]
Coset.gT [variable, in mathcomp.character.classfun]
-_ %% B (cfun_scope) [notation, in mathcomp.character.classfun]
-_ / B (cfun_scope) [notation, in mathcomp.character.classfun]
+_ %% B (cfun_scope) [notation, in mathcomp.character.classfun]
+_ / B (cfun_scope) [notation, in mathcomp.character.classfun]
coset1 [lemma, in mathcomp.fingroup.quotient]
coset1_injm [lemma, in mathcomp.fingroup.quotient]
count [definition, in mathcomp.ssreflect.seq]
@@ -2458,8 +2570,8 @@ CountableDataTypes [section, in mathcomp.ssreflect.choice]
CountableTheory [section, in mathcomp.ssreflect.choice]
CountableTheory.T [variable, in mathcomp.ssreflect.choice]
-countable_algebraic_closure [lemma, in mathcomp.field.countalg]
-countable_field_extension [lemma, in mathcomp.field.countalg]
+countable_algebraic_closure [lemma, in mathcomp.field.closed_field]
+countable_field_extension [lemma, in mathcomp.field.closed_field]
Countable.base [projection, in mathcomp.ssreflect.choice]
Countable.ChoiceMixin [definition, in mathcomp.ssreflect.choice]
Countable.choiceType [definition, in mathcomp.ssreflect.choice]
@@ -2478,8 +2590,8 @@ Countable.Exports.CountMixin [abbreviation, in mathcomp.ssreflect.choice]
Countable.Exports.CountType [abbreviation, in mathcomp.ssreflect.choice]
Countable.Exports.countType [abbreviation, in mathcomp.ssreflect.choice]
-[ countType of _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
-[ countType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
+[ countType of _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
+[ countType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
Countable.mixin [projection, in mathcomp.ssreflect.choice]
Countable.Mixin [constructor, in mathcomp.ssreflect.choice]
Countable.mixin_of [record, in mathcomp.ssreflect.choice]
@@ -2491,7 +2603,7 @@ Countable.type [record, in mathcomp.ssreflect.choice]
Countable.unpickle [projection, in mathcomp.ssreflect.choice]
Countable.xclass [abbreviation, in mathcomp.ssreflect.choice]
-countalg [library]
+countalg [library]
CountEncodingModuloRel [section, in mathcomp.ssreflect.generic_quotient]
CountEncodingModuloRel.C [variable, in mathcomp.ssreflect.generic_quotient]
CountEncodingModuloRel.CD [variable, in mathcomp.ssreflect.generic_quotient]
@@ -2499,348 +2611,350 @@ CountEncodingModuloRel.DC [variable, in mathcomp.ssreflect.generic_quotient]
CountEncodingModuloRel.eD [variable, in mathcomp.ssreflect.generic_quotient]
CountEncodingModuloRel.encD [variable, in mathcomp.ssreflect.generic_quotient]
-CountRing [module, in mathcomp.field.countalg]
-CountRing.ClosedField [module, in mathcomp.field.countalg]
-CountRing.ClosedField.base [projection, in mathcomp.field.countalg]
-CountRing.ClosedField.base2 [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.choiceType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.class [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.Class [constructor, in mathcomp.field.countalg]
-CountRing.ClosedField.ClassDef [section, in mathcomp.field.countalg]
-CountRing.ClosedField.ClassDef.cT [variable, in mathcomp.field.countalg]
-CountRing.ClosedField.ClassDef.xT [variable, in mathcomp.field.countalg]
-CountRing.ClosedField.class_of [record, in mathcomp.field.countalg]
-CountRing.ClosedField.closedFieldType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.comRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.comUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.countComRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.countComUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.countDecFieldType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.countFieldType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.countIdomainType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.countRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.countType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.countZmodType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.decFieldType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.eqType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.Exports [module, in mathcomp.field.countalg]
-CountRing.ClosedField.Exports.countClosedFieldType [abbreviation, in mathcomp.field.countalg]
-[ countClosedFieldType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
-CountRing.ClosedField.fieldType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.idomainType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.join_countDecFieldType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.join_countFieldType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.join_countIdomainType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.join_countComUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.join_countComRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.join_countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.join_countRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.join_countZmodType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.join_countType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.mixin [projection, in mathcomp.field.countalg]
-CountRing.ClosedField.pack [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.Pack [constructor, in mathcomp.field.countalg]
-CountRing.ClosedField.ringType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.sort [projection, in mathcomp.field.countalg]
-CountRing.ClosedField.type [record, in mathcomp.field.countalg]
-CountRing.ClosedField.unitRingType [definition, in mathcomp.field.countalg]
-CountRing.ClosedField.xclass [abbreviation, in mathcomp.field.countalg]
-CountRing.ClosedField.zmodType [definition, in mathcomp.field.countalg]
-CountRing.cnt_ [abbreviation, in mathcomp.field.countalg]
-CountRing.ComRing [module, in mathcomp.field.countalg]
-CountRing.ComRing.base [projection, in mathcomp.field.countalg]
-CountRing.ComRing.base2 [definition, in mathcomp.field.countalg]
-CountRing.ComRing.choiceType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.class [definition, in mathcomp.field.countalg]
-CountRing.ComRing.Class [constructor, in mathcomp.field.countalg]
-CountRing.ComRing.ClassDef [section, in mathcomp.field.countalg]
-CountRing.ComRing.ClassDef.cT [variable, in mathcomp.field.countalg]
-CountRing.ComRing.ClassDef.xT [variable, in mathcomp.field.countalg]
-CountRing.ComRing.class_of [record, in mathcomp.field.countalg]
-CountRing.ComRing.comRingType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.countRingType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.countType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.countZmodType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.eqType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.Exports [module, in mathcomp.field.countalg]
-CountRing.ComRing.Exports.countComRingType [abbreviation, in mathcomp.field.countalg]
-[ countComRingType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
-CountRing.ComRing.join_countRingType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.join_countZmodType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.join_countType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.mixin [projection, in mathcomp.field.countalg]
-CountRing.ComRing.pack [definition, in mathcomp.field.countalg]
-CountRing.ComRing.Pack [constructor, in mathcomp.field.countalg]
-CountRing.ComRing.ringType [definition, in mathcomp.field.countalg]
-CountRing.ComRing.sort [projection, in mathcomp.field.countalg]
-CountRing.ComRing.type [record, in mathcomp.field.countalg]
-CountRing.ComRing.xclass [abbreviation, in mathcomp.field.countalg]
-CountRing.ComRing.zmodType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing [module, in mathcomp.field.countalg]
-CountRing.ComUnitRing.base [projection, in mathcomp.field.countalg]
-CountRing.ComUnitRing.base2 [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.base3 [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.ccjoin_countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.choiceType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.cjoin_countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.class [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.Class [constructor, in mathcomp.field.countalg]
-CountRing.ComUnitRing.ClassDef [section, in mathcomp.field.countalg]
-CountRing.ComUnitRing.ClassDef.cT [variable, in mathcomp.field.countalg]
-CountRing.ComUnitRing.ClassDef.xT [variable, in mathcomp.field.countalg]
-CountRing.ComUnitRing.class_of [record, in mathcomp.field.countalg]
-CountRing.ComUnitRing.comRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.comUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.countComRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.countRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.countType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.countZmodType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.eqType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.Exports [module, in mathcomp.field.countalg]
-CountRing.ComUnitRing.Exports.countComUnitRingType [abbreviation, in mathcomp.field.countalg]
-[ countComUnitRingType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
-CountRing.ComUnitRing.join_countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.join_countComRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.join_countRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.join_countZmodType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.join_countType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.mixin [projection, in mathcomp.field.countalg]
-CountRing.ComUnitRing.pack [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.Pack [constructor, in mathcomp.field.countalg]
-CountRing.ComUnitRing.ringType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.sort [projection, in mathcomp.field.countalg]
-CountRing.ComUnitRing.type [record, in mathcomp.field.countalg]
-CountRing.ComUnitRing.ujoin_countComRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.unitRingType [definition, in mathcomp.field.countalg]
-CountRing.ComUnitRing.xclass [abbreviation, in mathcomp.field.countalg]
-CountRing.ComUnitRing.zmodType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField [module, in mathcomp.field.countalg]
-CountRing.DecidableField.base [projection, in mathcomp.field.countalg]
-CountRing.DecidableField.base2 [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.choiceType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.class [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.Class [constructor, in mathcomp.field.countalg]
-CountRing.DecidableField.ClassDef [section, in mathcomp.field.countalg]
-CountRing.DecidableField.ClassDef.cT [variable, in mathcomp.field.countalg]
-CountRing.DecidableField.ClassDef.xT [variable, in mathcomp.field.countalg]
-CountRing.DecidableField.class_of [record, in mathcomp.field.countalg]
-CountRing.DecidableField.comRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.comUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.countComRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.countComUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.countFieldType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.countIdomainType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.countRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.countType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.countZmodType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.decFieldType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.eqType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.Exports [module, in mathcomp.field.countalg]
-CountRing.DecidableField.Exports.countDecFieldType [abbreviation, in mathcomp.field.countalg]
-[ countDecFieldType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
-CountRing.DecidableField.fieldType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.idomainType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.join_countFieldType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.join_countIdomainType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.join_countComUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.join_countComRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.join_countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.join_countRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.join_countZmodType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.join_countType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.mixin [projection, in mathcomp.field.countalg]
-CountRing.DecidableField.pack [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.Pack [constructor, in mathcomp.field.countalg]
-CountRing.DecidableField.ringType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.sort [projection, in mathcomp.field.countalg]
-CountRing.DecidableField.type [record, in mathcomp.field.countalg]
-CountRing.DecidableField.unitRingType [definition, in mathcomp.field.countalg]
-CountRing.DecidableField.xclass [abbreviation, in mathcomp.field.countalg]
-CountRing.DecidableField.zmodType [definition, in mathcomp.field.countalg]
-CountRing.do_pack [abbreviation, in mathcomp.field.countalg]
-CountRing.Field [module, in mathcomp.field.countalg]
-CountRing.Field.base [projection, in mathcomp.field.countalg]
-CountRing.Field.base2 [definition, in mathcomp.field.countalg]
-CountRing.Field.choiceType [definition, in mathcomp.field.countalg]
-CountRing.Field.class [definition, in mathcomp.field.countalg]
-CountRing.Field.Class [constructor, in mathcomp.field.countalg]
-CountRing.Field.ClassDef [section, in mathcomp.field.countalg]
-CountRing.Field.ClassDef.cT [variable, in mathcomp.field.countalg]
-CountRing.Field.ClassDef.xT [variable, in mathcomp.field.countalg]
-CountRing.Field.class_of [record, in mathcomp.field.countalg]
-CountRing.Field.comRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.comUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.countComRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.countComUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.countIdomainType [definition, in mathcomp.field.countalg]
-CountRing.Field.countRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.countType [definition, in mathcomp.field.countalg]
-CountRing.Field.countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.countZmodType [definition, in mathcomp.field.countalg]
-CountRing.Field.eqType [definition, in mathcomp.field.countalg]
-CountRing.Field.Exports [module, in mathcomp.field.countalg]
-CountRing.Field.Exports.countFieldType [abbreviation, in mathcomp.field.countalg]
-[ countFieldType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
-CountRing.Field.fieldType [definition, in mathcomp.field.countalg]
-CountRing.Field.idomainType [definition, in mathcomp.field.countalg]
-CountRing.Field.join_countIdomainType [definition, in mathcomp.field.countalg]
-CountRing.Field.join_countComUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.join_countComRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.join_countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.join_countRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.join_countZmodType [definition, in mathcomp.field.countalg]
-CountRing.Field.join_countType [definition, in mathcomp.field.countalg]
-CountRing.Field.mixin [projection, in mathcomp.field.countalg]
-CountRing.Field.pack [definition, in mathcomp.field.countalg]
-CountRing.Field.Pack [constructor, in mathcomp.field.countalg]
-CountRing.Field.ringType [definition, in mathcomp.field.countalg]
-CountRing.Field.sort [projection, in mathcomp.field.countalg]
-CountRing.Field.type [record, in mathcomp.field.countalg]
-CountRing.Field.unitRingType [definition, in mathcomp.field.countalg]
-CountRing.Field.xclass [abbreviation, in mathcomp.field.countalg]
-CountRing.Field.zmodType [definition, in mathcomp.field.countalg]
-CountRing.Generic [section, in mathcomp.field.countalg]
-CountRing.Generic.base_class [variable, in mathcomp.field.countalg]
-CountRing.Generic.base_sort [variable, in mathcomp.field.countalg]
-CountRing.Generic.base_of [variable, in mathcomp.field.countalg]
-CountRing.Generic.base_type [variable, in mathcomp.field.countalg]
-CountRing.Generic.Class [variable, in mathcomp.field.countalg]
-CountRing.Generic.class_of [variable, in mathcomp.field.countalg]
-CountRing.Generic.Pack [variable, in mathcomp.field.countalg]
-CountRing.Generic.type [variable, in mathcomp.field.countalg]
-CountRing.gen_pack [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain [module, in mathcomp.field.countalg]
-CountRing.IntegralDomain.base [projection, in mathcomp.field.countalg]
-CountRing.IntegralDomain.base2 [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.choiceType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.class [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.Class [constructor, in mathcomp.field.countalg]
-CountRing.IntegralDomain.ClassDef [section, in mathcomp.field.countalg]
-CountRing.IntegralDomain.ClassDef.cT [variable, in mathcomp.field.countalg]
-CountRing.IntegralDomain.ClassDef.xT [variable, in mathcomp.field.countalg]
-CountRing.IntegralDomain.class_of [record, in mathcomp.field.countalg]
-CountRing.IntegralDomain.comRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.comUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.countComRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.countComUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.countRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.countType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.countZmodType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.eqType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.Exports [module, in mathcomp.field.countalg]
-CountRing.IntegralDomain.Exports.countIdomainType [abbreviation, in mathcomp.field.countalg]
-[ countIdomainType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
-CountRing.IntegralDomain.idomainType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.join_countComUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.join_countComRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.join_countUnitRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.join_countRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.join_countZmodType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.join_countType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.mixin [projection, in mathcomp.field.countalg]
-CountRing.IntegralDomain.pack [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.Pack [constructor, in mathcomp.field.countalg]
-CountRing.IntegralDomain.ringType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.sort [projection, in mathcomp.field.countalg]
-CountRing.IntegralDomain.type [record, in mathcomp.field.countalg]
-CountRing.IntegralDomain.unitRingType [definition, in mathcomp.field.countalg]
-CountRing.IntegralDomain.xclass [abbreviation, in mathcomp.field.countalg]
-CountRing.IntegralDomain.zmodType [definition, in mathcomp.field.countalg]
-CountRing.mixin_of [abbreviation, in mathcomp.field.countalg]
-CountRing.Ring [module, in mathcomp.field.countalg]
-CountRing.Ring.base [projection, in mathcomp.field.countalg]
-CountRing.Ring.base2 [definition, in mathcomp.field.countalg]
-CountRing.Ring.choiceType [definition, in mathcomp.field.countalg]
-CountRing.Ring.class [definition, in mathcomp.field.countalg]
-CountRing.Ring.Class [constructor, in mathcomp.field.countalg]
-CountRing.Ring.ClassDef [section, in mathcomp.field.countalg]
-CountRing.Ring.ClassDef.cT [variable, in mathcomp.field.countalg]
-CountRing.Ring.ClassDef.xT [variable, in mathcomp.field.countalg]
-CountRing.Ring.class_of [record, in mathcomp.field.countalg]
-CountRing.Ring.countType [definition, in mathcomp.field.countalg]
-CountRing.Ring.countZmodType [definition, in mathcomp.field.countalg]
-CountRing.Ring.eqType [definition, in mathcomp.field.countalg]
-CountRing.Ring.Exports [module, in mathcomp.field.countalg]
-CountRing.Ring.Exports.countRingType [abbreviation, in mathcomp.field.countalg]
-[ countRingType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
-CountRing.Ring.join_countZmodType [definition, in mathcomp.field.countalg]
-CountRing.Ring.join_countType [definition, in mathcomp.field.countalg]
-CountRing.Ring.mixin [projection, in mathcomp.field.countalg]
-CountRing.Ring.pack [definition, in mathcomp.field.countalg]
-CountRing.Ring.Pack [constructor, in mathcomp.field.countalg]
-CountRing.Ring.ringType [definition, in mathcomp.field.countalg]
-CountRing.Ring.sort [projection, in mathcomp.field.countalg]
-CountRing.Ring.type [record, in mathcomp.field.countalg]
-CountRing.Ring.xclass [abbreviation, in mathcomp.field.countalg]
-CountRing.Ring.zmodType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing [module, in mathcomp.field.countalg]
-CountRing.UnitRing.base [projection, in mathcomp.field.countalg]
-CountRing.UnitRing.base2 [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.choiceType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.class [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.Class [constructor, in mathcomp.field.countalg]
-CountRing.UnitRing.ClassDef [section, in mathcomp.field.countalg]
-CountRing.UnitRing.ClassDef.cT [variable, in mathcomp.field.countalg]
-CountRing.UnitRing.ClassDef.xT [variable, in mathcomp.field.countalg]
-CountRing.UnitRing.class_of [record, in mathcomp.field.countalg]
-CountRing.UnitRing.countRingType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.countType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.countZmodType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.eqType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.Exports [module, in mathcomp.field.countalg]
-CountRing.UnitRing.Exports.countUnitRingType [abbreviation, in mathcomp.field.countalg]
-[ countUnitRingType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
-CountRing.UnitRing.join_countRingType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.join_countZmodType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.join_countType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.mixin [projection, in mathcomp.field.countalg]
-CountRing.UnitRing.pack [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.Pack [constructor, in mathcomp.field.countalg]
-CountRing.UnitRing.ringType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.sort [projection, in mathcomp.field.countalg]
-CountRing.UnitRing.type [record, in mathcomp.field.countalg]
-CountRing.UnitRing.unitRingType [definition, in mathcomp.field.countalg]
-CountRing.UnitRing.xclass [abbreviation, in mathcomp.field.countalg]
-CountRing.UnitRing.zmodType [definition, in mathcomp.field.countalg]
-CountRing.Zmodule [module, in mathcomp.field.countalg]
-CountRing.Zmodule.base [projection, in mathcomp.field.countalg]
-CountRing.Zmodule.choiceType [definition, in mathcomp.field.countalg]
-CountRing.Zmodule.class [definition, in mathcomp.field.countalg]
-CountRing.Zmodule.Class [constructor, in mathcomp.field.countalg]
-CountRing.Zmodule.ClassDef [section, in mathcomp.field.countalg]
-CountRing.Zmodule.ClassDef.cT [variable, in mathcomp.field.countalg]
-CountRing.Zmodule.ClassDef.xT [variable, in mathcomp.field.countalg]
-CountRing.Zmodule.class_of [record, in mathcomp.field.countalg]
-CountRing.Zmodule.countType [definition, in mathcomp.field.countalg]
-CountRing.Zmodule.eqType [definition, in mathcomp.field.countalg]
-CountRing.Zmodule.Exports [module, in mathcomp.field.countalg]
-CountRing.Zmodule.Exports.countZmodType [abbreviation, in mathcomp.field.countalg]
-[ countZmodType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
-CountRing.Zmodule.join_countType [definition, in mathcomp.field.countalg]
-CountRing.Zmodule.mixin [projection, in mathcomp.field.countalg]
-CountRing.Zmodule.pack [definition, in mathcomp.field.countalg]
-CountRing.Zmodule.Pack [constructor, in mathcomp.field.countalg]
-CountRing.Zmodule.sort [projection, in mathcomp.field.countalg]
-CountRing.Zmodule.type [record, in mathcomp.field.countalg]
-CountRing.Zmodule.xclass [abbreviation, in mathcomp.field.countalg]
-CountRing.Zmodule.zmodType [definition, in mathcomp.field.countalg]
+countMixin [lemma, in mathcomp.ssreflect.finfun]
+CountRing [module, in mathcomp.algebra.countalg]
+CountRing.ClosedField [module, in mathcomp.algebra.countalg]
+CountRing.ClosedField.base [projection, in mathcomp.algebra.countalg]
+CountRing.ClosedField.base2 [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.choiceType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.class [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.Class [constructor, in mathcomp.algebra.countalg]
+CountRing.ClosedField.ClassDef [section, in mathcomp.algebra.countalg]
+CountRing.ClosedField.ClassDef.cT [variable, in mathcomp.algebra.countalg]
+CountRing.ClosedField.ClassDef.xT [variable, in mathcomp.algebra.countalg]
+CountRing.ClosedField.class_of [record, in mathcomp.algebra.countalg]
+CountRing.ClosedField.closedFieldType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.comRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.comUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.countComUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.countDecFieldType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.countFieldType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.countIdomainType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.countType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.decFieldType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.eqType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.Exports [module, in mathcomp.algebra.countalg]
+CountRing.ClosedField.Exports.countClosedFieldType [abbreviation, in mathcomp.algebra.countalg]
+[ countClosedFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
+CountRing.ClosedField.fieldType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.idomainType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.join_countDecFieldType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.join_countFieldType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.join_countIdomainType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.join_countComUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.join_countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.join_countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.join_countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.join_countType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.mixin [projection, in mathcomp.algebra.countalg]
+CountRing.ClosedField.pack [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.Pack [constructor, in mathcomp.algebra.countalg]
+CountRing.ClosedField.ringType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.sort [projection, in mathcomp.algebra.countalg]
+CountRing.ClosedField.type [record, in mathcomp.algebra.countalg]
+CountRing.ClosedField.unitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ClosedField.xclass [abbreviation, in mathcomp.algebra.countalg]
+CountRing.ClosedField.zmodType [definition, in mathcomp.algebra.countalg]
+CountRing.cnt_ [abbreviation, in mathcomp.algebra.countalg]
+CountRing.ComRing [module, in mathcomp.algebra.countalg]
+CountRing.ComRing.base [projection, in mathcomp.algebra.countalg]
+CountRing.ComRing.base2 [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.choiceType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.class [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.Class [constructor, in mathcomp.algebra.countalg]
+CountRing.ComRing.ClassDef [section, in mathcomp.algebra.countalg]
+CountRing.ComRing.ClassDef.cT [variable, in mathcomp.algebra.countalg]
+CountRing.ComRing.ClassDef.xT [variable, in mathcomp.algebra.countalg]
+CountRing.ComRing.class_of [record, in mathcomp.algebra.countalg]
+CountRing.ComRing.comRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.countType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.eqType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.Exports [module, in mathcomp.algebra.countalg]
+CountRing.ComRing.Exports.countComRingType [abbreviation, in mathcomp.algebra.countalg]
+[ countComRingType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
+CountRing.ComRing.join_countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.join_countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.join_countType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.mixin [projection, in mathcomp.algebra.countalg]
+CountRing.ComRing.pack [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.Pack [constructor, in mathcomp.algebra.countalg]
+CountRing.ComRing.ringType [definition, in mathcomp.algebra.countalg]
+CountRing.ComRing.sort [projection, in mathcomp.algebra.countalg]
+CountRing.ComRing.type [record, in mathcomp.algebra.countalg]
+CountRing.ComRing.xclass [abbreviation, in mathcomp.algebra.countalg]
+CountRing.ComRing.zmodType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing [module, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.base [projection, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.base2 [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.base3 [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.ccjoin_countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.choiceType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.cjoin_countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.class [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.Class [constructor, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.ClassDef [section, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.ClassDef.cT [variable, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.ClassDef.xT [variable, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.class_of [record, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.comRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.comUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.countType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.eqType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.Exports [module, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.Exports.countComUnitRingType [abbreviation, in mathcomp.algebra.countalg]
+[ countComUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.join_countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.join_countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.join_countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.join_countType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.mixin [projection, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.pack [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.Pack [constructor, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.ringType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.sort [projection, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.type [record, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.ujoin_countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.unitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.xclass [abbreviation, in mathcomp.algebra.countalg]
+CountRing.ComUnitRing.zmodType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField [module, in mathcomp.algebra.countalg]
+CountRing.DecidableField.base [projection, in mathcomp.algebra.countalg]
+CountRing.DecidableField.base2 [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.choiceType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.class [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.Class [constructor, in mathcomp.algebra.countalg]
+CountRing.DecidableField.ClassDef [section, in mathcomp.algebra.countalg]
+CountRing.DecidableField.ClassDef.cT [variable, in mathcomp.algebra.countalg]
+CountRing.DecidableField.ClassDef.xT [variable, in mathcomp.algebra.countalg]
+CountRing.DecidableField.class_of [record, in mathcomp.algebra.countalg]
+CountRing.DecidableField.comRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.comUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.countComUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.countFieldType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.countIdomainType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.countType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.decFieldType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.eqType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.Exports [module, in mathcomp.algebra.countalg]
+CountRing.DecidableField.Exports.countDecFieldType [abbreviation, in mathcomp.algebra.countalg]
+[ countDecFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
+CountRing.DecidableField.fieldType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.idomainType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.join_countFieldType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.join_countIdomainType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.join_countComUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.join_countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.join_countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.join_countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.join_countType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.mixin [projection, in mathcomp.algebra.countalg]
+CountRing.DecidableField.pack [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.Pack [constructor, in mathcomp.algebra.countalg]
+CountRing.DecidableField.ringType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.sort [projection, in mathcomp.algebra.countalg]
+CountRing.DecidableField.type [record, in mathcomp.algebra.countalg]
+CountRing.DecidableField.unitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.DecidableField.xclass [abbreviation, in mathcomp.algebra.countalg]
+CountRing.DecidableField.zmodType [definition, in mathcomp.algebra.countalg]
+CountRing.do_pack [abbreviation, in mathcomp.algebra.countalg]
+CountRing.Field [module, in mathcomp.algebra.countalg]
+CountRing.Field.base [projection, in mathcomp.algebra.countalg]
+CountRing.Field.base2 [definition, in mathcomp.algebra.countalg]
+CountRing.Field.choiceType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.class [definition, in mathcomp.algebra.countalg]
+CountRing.Field.Class [constructor, in mathcomp.algebra.countalg]
+CountRing.Field.ClassDef [section, in mathcomp.algebra.countalg]
+CountRing.Field.ClassDef.cT [variable, in mathcomp.algebra.countalg]
+CountRing.Field.ClassDef.xT [variable, in mathcomp.algebra.countalg]
+CountRing.Field.class_of [record, in mathcomp.algebra.countalg]
+CountRing.Field.comRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.comUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.countComUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.countIdomainType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.countType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.eqType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.Exports [module, in mathcomp.algebra.countalg]
+CountRing.Field.Exports.countFieldType [abbreviation, in mathcomp.algebra.countalg]
+[ countFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
+CountRing.Field.fieldType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.idomainType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.join_countIdomainType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.join_countComUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.join_countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.join_countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.join_countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.join_countType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.mixin [projection, in mathcomp.algebra.countalg]
+CountRing.Field.pack [definition, in mathcomp.algebra.countalg]
+CountRing.Field.Pack [constructor, in mathcomp.algebra.countalg]
+CountRing.Field.ringType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.sort [projection, in mathcomp.algebra.countalg]
+CountRing.Field.type [record, in mathcomp.algebra.countalg]
+CountRing.Field.unitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.Field.xclass [abbreviation, in mathcomp.algebra.countalg]
+CountRing.Field.zmodType [definition, in mathcomp.algebra.countalg]
+CountRing.Generic [section, in mathcomp.algebra.countalg]
+CountRing.Generic.base_class [variable, in mathcomp.algebra.countalg]
+CountRing.Generic.base_sort [variable, in mathcomp.algebra.countalg]
+CountRing.Generic.base_of [variable, in mathcomp.algebra.countalg]
+CountRing.Generic.base_type [variable, in mathcomp.algebra.countalg]
+CountRing.Generic.Class [variable, in mathcomp.algebra.countalg]
+CountRing.Generic.class_of [variable, in mathcomp.algebra.countalg]
+CountRing.Generic.Pack [variable, in mathcomp.algebra.countalg]
+CountRing.Generic.type [variable, in mathcomp.algebra.countalg]
+CountRing.gen_pack [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain [module, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.base [projection, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.base2 [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.choiceType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.class [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.Class [constructor, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.ClassDef [section, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.ClassDef.cT [variable, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.ClassDef.xT [variable, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.class_of [record, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.comRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.comUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.countComUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.countType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.eqType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.Exports [module, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.Exports.countIdomainType [abbreviation, in mathcomp.algebra.countalg]
+[ countIdomainType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.idomainType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.join_countComUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.join_countComRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.join_countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.join_countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.join_countType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.mixin [projection, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.pack [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.Pack [constructor, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.ringType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.sort [projection, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.type [record, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.unitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.xclass [abbreviation, in mathcomp.algebra.countalg]
+CountRing.IntegralDomain.zmodType [definition, in mathcomp.algebra.countalg]
+CountRing.mixin_of [abbreviation, in mathcomp.algebra.countalg]
+CountRing.Ring [module, in mathcomp.algebra.countalg]
+CountRing.Ring.base [projection, in mathcomp.algebra.countalg]
+CountRing.Ring.base2 [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.choiceType [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.class [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.Class [constructor, in mathcomp.algebra.countalg]
+CountRing.Ring.ClassDef [section, in mathcomp.algebra.countalg]
+CountRing.Ring.ClassDef.cT [variable, in mathcomp.algebra.countalg]
+CountRing.Ring.ClassDef.xT [variable, in mathcomp.algebra.countalg]
+CountRing.Ring.class_of [record, in mathcomp.algebra.countalg]
+CountRing.Ring.countType [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.eqType [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.Exports [module, in mathcomp.algebra.countalg]
+CountRing.Ring.Exports.countRingType [abbreviation, in mathcomp.algebra.countalg]
+[ countRingType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
+CountRing.Ring.join_countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.join_countType [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.mixin [projection, in mathcomp.algebra.countalg]
+CountRing.Ring.pack [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.Pack [constructor, in mathcomp.algebra.countalg]
+CountRing.Ring.ringType [definition, in mathcomp.algebra.countalg]
+CountRing.Ring.sort [projection, in mathcomp.algebra.countalg]
+CountRing.Ring.type [record, in mathcomp.algebra.countalg]
+CountRing.Ring.xclass [abbreviation, in mathcomp.algebra.countalg]
+CountRing.Ring.zmodType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing [module, in mathcomp.algebra.countalg]
+CountRing.UnitRing.base [projection, in mathcomp.algebra.countalg]
+CountRing.UnitRing.base2 [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.choiceType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.class [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.Class [constructor, in mathcomp.algebra.countalg]
+CountRing.UnitRing.ClassDef [section, in mathcomp.algebra.countalg]
+CountRing.UnitRing.ClassDef.cT [variable, in mathcomp.algebra.countalg]
+CountRing.UnitRing.ClassDef.xT [variable, in mathcomp.algebra.countalg]
+CountRing.UnitRing.class_of [record, in mathcomp.algebra.countalg]
+CountRing.UnitRing.countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.countType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.eqType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.Exports [module, in mathcomp.algebra.countalg]
+CountRing.UnitRing.Exports.countUnitRingType [abbreviation, in mathcomp.algebra.countalg]
+[ countUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
+CountRing.UnitRing.join_countRingType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.join_countZmodType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.join_countType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.mixin [projection, in mathcomp.algebra.countalg]
+CountRing.UnitRing.pack [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.Pack [constructor, in mathcomp.algebra.countalg]
+CountRing.UnitRing.ringType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.sort [projection, in mathcomp.algebra.countalg]
+CountRing.UnitRing.type [record, in mathcomp.algebra.countalg]
+CountRing.UnitRing.unitRingType [definition, in mathcomp.algebra.countalg]
+CountRing.UnitRing.xclass [abbreviation, in mathcomp.algebra.countalg]
+CountRing.UnitRing.zmodType [definition, in mathcomp.algebra.countalg]
+CountRing.Zmodule [module, in mathcomp.algebra.countalg]
+CountRing.Zmodule.base [projection, in mathcomp.algebra.countalg]
+CountRing.Zmodule.choiceType [definition, in mathcomp.algebra.countalg]
+CountRing.Zmodule.class [definition, in mathcomp.algebra.countalg]
+CountRing.Zmodule.Class [constructor, in mathcomp.algebra.countalg]
+CountRing.Zmodule.ClassDef [section, in mathcomp.algebra.countalg]
+CountRing.Zmodule.ClassDef.cT [variable, in mathcomp.algebra.countalg]
+CountRing.Zmodule.ClassDef.xT [variable, in mathcomp.algebra.countalg]
+CountRing.Zmodule.class_of [record, in mathcomp.algebra.countalg]
+CountRing.Zmodule.countType [definition, in mathcomp.algebra.countalg]
+CountRing.Zmodule.eqType [definition, in mathcomp.algebra.countalg]
+CountRing.Zmodule.Exports [module, in mathcomp.algebra.countalg]
+CountRing.Zmodule.Exports.countZmodType [abbreviation, in mathcomp.algebra.countalg]
+[ countZmodType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
+CountRing.Zmodule.join_countType [definition, in mathcomp.algebra.countalg]
+CountRing.Zmodule.mixin [projection, in mathcomp.algebra.countalg]
+CountRing.Zmodule.pack [definition, in mathcomp.algebra.countalg]
+CountRing.Zmodule.Pack [constructor, in mathcomp.algebra.countalg]
+CountRing.Zmodule.sort [projection, in mathcomp.algebra.countalg]
+CountRing.Zmodule.type [record, in mathcomp.algebra.countalg]
+CountRing.Zmodule.xclass [abbreviation, in mathcomp.algebra.countalg]
+CountRing.Zmodule.zmodType [definition, in mathcomp.algebra.countalg]
count_flatten [lemma, in mathcomp.ssreflect.seq]
count_map [lemma, in mathcomp.ssreflect.seq]
count_mem_uniq [lemma, in mathcomp.ssreflect.seq]
count_uniq_mem [lemma, in mathcomp.ssreflect.seq]
count_memPn [lemma, in mathcomp.ssreflect.seq]
-count_rev [lemma, in mathcomp.ssreflect.seq]
count_mem [abbreviation, in mathcomp.ssreflect.seq]
+count_rev [lemma, in mathcomp.ssreflect.seq]
count_filter [lemma, in mathcomp.ssreflect.seq]
count_predC [lemma, in mathcomp.ssreflect.seq]
count_predUI [lemma, in mathcomp.ssreflect.seq]
count_predT [lemma, in mathcomp.ssreflect.seq]
count_pred0 [lemma, in mathcomp.ssreflect.seq]
count_cat [lemma, in mathcomp.ssreflect.seq]
+count_nseq [lemma, in mathcomp.ssreflect.seq]
count_size [lemma, in mathcomp.ssreflect.seq]
count_logn_dprod_cycle [lemma, in mathcomp.solvable.abelian]
cover [definition, in mathcomp.ssreflect.finset]
@@ -3087,7 +3201,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -3119,14 +3233,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -3151,7 +3265,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -3183,7 +3297,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -3215,7 +3329,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -3247,7 +3361,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -3279,7 +3393,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -3311,7 +3425,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -3343,14 +3457,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -3375,7 +3489,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -3407,7 +3521,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -3439,7 +3553,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -3471,14 +3585,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -3503,7 +3617,7 @@ Z _ other -(185 entries) +(189 entries) -- cgit v1.2.3