| 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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 entries) | +
| Axiom 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +
G (lemma)
+gacentC [in mathcomp.fingroup.action]+gacentD1 [in mathcomp.fingroup.action]
+gacentE [in mathcomp.fingroup.action]
+gacentEsd [in mathcomp.fingroup.gproduct]
+gacentIdom [in mathcomp.fingroup.action]
+gacentIim [in mathcomp.fingroup.action]
+gacentJ [in mathcomp.fingroup.action]
+gacentM [in mathcomp.fingroup.action]
+gacentQ [in mathcomp.fingroup.action]
+gacentS [in mathcomp.fingroup.action]
+gacentU [in mathcomp.fingroup.action]
+gacentY [in mathcomp.fingroup.action]
+gacent_comp [in mathcomp.fingroup.action]
+gacent_mod [in mathcomp.fingroup.action]
+gacent_actby [in mathcomp.fingroup.action]
+gacent_ract [in mathcomp.fingroup.action]
+gacent_cycle [in mathcomp.fingroup.action]
+gacent_gen [in mathcomp.fingroup.action]
+gacent_repr [in mathcomp.character.mxabelem]
+gacent1 [in mathcomp.fingroup.action]
+gacent1E [in mathcomp.fingroup.action]
+gactJ [in mathcomp.fingroup.action]
+gactM [in mathcomp.fingroup.action]
+gactR [in mathcomp.fingroup.action]
+gactsI [in mathcomp.solvable.jordanholder]
+gactsM [in mathcomp.solvable.jordanholder]
+gactsP [in mathcomp.solvable.jordanholder]
+gacts_char [in mathcomp.fingroup.action]
+gacts_range [in mathcomp.fingroup.action]
+gactV [in mathcomp.fingroup.action]
+gactX [in mathcomp.fingroup.action]
+gact_stable [in mathcomp.fingroup.action]
+gact_out [in mathcomp.fingroup.action]
+gact1 [in mathcomp.fingroup.action]
+galK [in mathcomp.field.galois]
+galLgen [in mathcomp.field.finfield]
+galM [in mathcomp.field.galois]
+galNormM [in mathcomp.field.galois]
+galNormV [in mathcomp.field.galois]
+galNormX [in mathcomp.field.galois]
+galNorm_gal [in mathcomp.field.galois]
+galNorm_fixedField [in mathcomp.field.galois]
+galNorm_eq0 [in mathcomp.field.galois]
+galNorm_prod [in mathcomp.field.galois]
+galNorm0 [in mathcomp.field.galois]
+galNorm1 [in mathcomp.field.galois]
+galoisS [in mathcomp.field.galois]
+galois_fixedField [in mathcomp.field.galois]
+galois_factors [in mathcomp.field.galois]
+galois_dim [in mathcomp.field.galois]
+galois_connection [in mathcomp.field.galois]
+galois_connection_subset [in mathcomp.field.galois]
+galois_connection_subv [in mathcomp.field.galois]
+galS [in mathcomp.field.galois]
+galTrace_gal [in mathcomp.field.galois]
+galTrace_fixedField [in mathcomp.field.galois]
+galTrace_is_additive [in mathcomp.field.galois]
+galV [in mathcomp.field.galois]
+gal_generated [in mathcomp.field.galois]
+gal_fixedField [in mathcomp.field.galois]
+gal_matrix [in mathcomp.field.galois]
+gal_independent [in mathcomp.field.galois]
+gal_independent_contra [in mathcomp.field.galois]
+gal_conjg [in mathcomp.field.galois]
+gal_adjoin_eq [in mathcomp.field.galois]
+gal_kHom [in mathcomp.field.galois]
+gal_kAut [in mathcomp.field.galois]
+gal_cap [in mathcomp.field.galois]
+gal_id [in mathcomp.field.galois]
+gal_eqP [in mathcomp.field.galois]
+gal_AEnd [in mathcomp.field.galois]
+gal_repr_inj [in mathcomp.field.galois]
+gal_reprK [in mathcomp.field.galois]
+gal_is_morphism [in mathcomp.field.galois]
+gal_mulP [in mathcomp.field.galois]
+gal_invP [in mathcomp.field.galois]
+gal_oneP [in mathcomp.field.galois]
+gal_sgvalK [in mathcomp.field.galois]
+Gaschutz_transitive [in mathcomp.solvable.finmodule]
+Gaschutz_split [in mathcomp.solvable.finmodule]
+gastabsP [in mathcomp.solvable.jordanholder]
+Gaussian_elimination_map [in mathcomp.algebra.mxalgebra]
+Gaussian_elimination_key [in mathcomp.algebra.mxalgebra]
+Gauss_gcdl [in mathcomp.ssreflect.div]
+Gauss_gcdr [in mathcomp.ssreflect.div]
+Gauss_dvdl [in mathcomp.ssreflect.div]
+Gauss_dvdr [in mathcomp.ssreflect.div]
+Gauss_dvd [in mathcomp.ssreflect.div]
+Gauss_gcdzl [in mathcomp.algebra.intdiv]
+Gauss_gcdzr [in mathcomp.algebra.intdiv]
+Gauss_dvdzl [in mathcomp.algebra.intdiv]
+Gauss_dvdzr [in mathcomp.algebra.intdiv]
+Gauss_dvdz [in mathcomp.algebra.intdiv]
+gcdnA [in mathcomp.ssreflect.div]
+gcdnAC [in mathcomp.ssreflect.div]
+gcdnACA [in mathcomp.ssreflect.div]
+gcdnC [in mathcomp.ssreflect.div]
+gcdnCA [in mathcomp.ssreflect.div]
+gcdnDl [in mathcomp.ssreflect.div]
+gcdnDr [in mathcomp.ssreflect.div]
+gcdnE [in mathcomp.ssreflect.div]
+gcdnMDl [in mathcomp.ssreflect.div]
+gcdnMl [in mathcomp.ssreflect.div]
+gcdnMr [in mathcomp.ssreflect.div]
+gcdnn [in mathcomp.ssreflect.div]
+gcdNz [in mathcomp.algebra.intdiv]
+gcdn_def [in mathcomp.ssreflect.div]
+gcdn_modl [in mathcomp.ssreflect.div]
+gcdn_modr [in mathcomp.ssreflect.div]
+gcdn_idPr [in mathcomp.ssreflect.div]
+gcdn_idPl [in mathcomp.ssreflect.div]
+gcdn_gt0 [in mathcomp.ssreflect.div]
+gcdn0 [in mathcomp.ssreflect.div]
+gcdn1 [in mathcomp.ssreflect.div]
+gcdp_polyOver [in mathcomp.field.fieldext]
+gcdzA [in mathcomp.algebra.intdiv]
+gcdzAC [in mathcomp.algebra.intdiv]
+gcdzACA [in mathcomp.algebra.intdiv]
+gcdzC [in mathcomp.algebra.intdiv]
+gcdzCA [in mathcomp.algebra.intdiv]
+gcdzDl [in mathcomp.algebra.intdiv]
+gcdzDr [in mathcomp.algebra.intdiv]
+gcdzMDl [in mathcomp.algebra.intdiv]
+gcdzMl [in mathcomp.algebra.intdiv]
+gcdzMr [in mathcomp.algebra.intdiv]
+gcdzN [in mathcomp.algebra.intdiv]
+gcdzz [in mathcomp.algebra.intdiv]
+gcdz_idPr [in mathcomp.algebra.intdiv]
+gcdz_idPl [in mathcomp.algebra.intdiv]
+gcdz_modl [in mathcomp.algebra.intdiv]
+gcdz_modr [in mathcomp.algebra.intdiv]
+gcdz_eq0 [in mathcomp.algebra.intdiv]
+gcdz0 [in mathcomp.algebra.intdiv]
+gcdz1 [in mathcomp.algebra.intdiv]
+gcd0n [in mathcomp.ssreflect.div]
+gcd0z [in mathcomp.algebra.intdiv]
+gcd1n [in mathcomp.ssreflect.div]
+gcd1z [in mathcomp.algebra.intdiv]
+gcore_max [in mathcomp.fingroup.fingroup]
+gcore_normal [in mathcomp.fingroup.fingroup]
+gcore_norm [in mathcomp.fingroup.fingroup]
+gcore_sub [in mathcomp.fingroup.fingroup]
+genD [in mathcomp.fingroup.fingroup]
+genDU [in mathcomp.fingroup.fingroup]
+genD1 [in mathcomp.fingroup.fingroup]
+genD1id [in mathcomp.fingroup.fingroup]
+generalized_orthogonality_relation [in mathcomp.character.character]
+generatedP [in mathcomp.fingroup.fingroup]
+generators_quaternion [in mathcomp.solvable.extremal]
+generators_semidihedral [in mathcomp.solvable.extremal]
+generators_2dihedral [in mathcomp.solvable.extremal]
+generators_modular_group [in mathcomp.solvable.extremal]
+generator_coprime [in mathcomp.solvable.cyclic]
+generator_order [in mathcomp.solvable.cyclic]
+generator_cycle [in mathcomp.solvable.cyclic]
+genGid [in mathcomp.fingroup.fingroup]
+genGidG [in mathcomp.fingroup.fingroup]
+genJ [in mathcomp.fingroup.fingroup]
+genmxE [in mathcomp.algebra.mxalgebra]
+genmxP [in mathcomp.algebra.mxalgebra]
+genmx_Socle [in mathcomp.character.mxrepresentation]
+genmx_component [in mathcomp.character.mxrepresentation]
+genmx_muls [in mathcomp.algebra.mxalgebra]
+genmx_diff [in mathcomp.algebra.mxalgebra]
+genmx_bigcap [in mathcomp.algebra.mxalgebra]
+genmx_cap [in mathcomp.algebra.mxalgebra]
+genmx_sums [in mathcomp.algebra.mxalgebra]
+genmx_adds [in mathcomp.algebra.mxalgebra]
+genmx_id [in mathcomp.algebra.mxalgebra]
+genmx_key [in mathcomp.algebra.mxalgebra]
+genmx0 [in mathcomp.algebra.mxalgebra]
+genmx1 [in mathcomp.algebra.mxalgebra]
+genM_join [in mathcomp.fingroup.fingroup]
+genS [in mathcomp.fingroup.fingroup]
+GenTree.codeK [in mathcomp.ssreflect.choice]
+genV [in mathcomp.fingroup.fingroup]
+gen_prodgP [in mathcomp.fingroup.fingroup]
+gen_expgs [in mathcomp.fingroup.fingroup]
+gen_set_id [in mathcomp.fingroup.fingroup]
+gen_subG [in mathcomp.fingroup.fingroup]
+gen_diso3 [in mathcomp.solvable.burnside_app]
+gen0 [in mathcomp.fingroup.fingroup]
+geq_divBl [in mathcomp.ssreflect.div]
+geq_leqif [in mathcomp.ssreflect.ssrnat]
+geq_minr [in mathcomp.ssreflect.ssrnat]
+geq_minl [in mathcomp.ssreflect.ssrnat]
+geq_min [in mathcomp.ssreflect.ssrnat]
+geq_max [in mathcomp.ssreflect.ssrnat]
+getCratK [in mathcomp.field.algC]
+gez0_abs [in mathcomp.algebra.ssrint]
+ge_rat0_norm [in mathcomp.algebra.rat]
+ge_rat0 [in mathcomp.algebra.rat]
+gFchar [in mathcomp.solvable.gfunctor]
+gFchar_trans [in mathcomp.solvable.gfunctor]
+gFcompS [in mathcomp.solvable.gfunctor]
+gFcomp_cont [in mathcomp.solvable.gfunctor]
+gFcomp_closed [in mathcomp.solvable.gfunctor]
+gFcont [in mathcomp.solvable.gfunctor]
+gFgroupset [in mathcomp.solvable.gfunctor]
+gFhereditary [in mathcomp.solvable.gfunctor]
+gFid [in mathcomp.solvable.gfunctor]
+gFisog [in mathcomp.solvable.gfunctor]
+gFisom [in mathcomp.solvable.gfunctor]
+gFiso_cont [in mathcomp.solvable.gfunctor]
+gFmod_hereditary [in mathcomp.solvable.gfunctor]
+gFmod_cont [in mathcomp.solvable.gfunctor]
+gFmod_closed [in mathcomp.solvable.gfunctor]
+gFnorm [in mathcomp.solvable.gfunctor]
+gFnormal [in mathcomp.solvable.gfunctor]
+gFnormal_trans [in mathcomp.solvable.gfunctor]
+gFnorms [in mathcomp.solvable.gfunctor]
+gFnorm_trans [in mathcomp.solvable.gfunctor]
+gFsub [in mathcomp.solvable.gfunctor]
+gFsub_trans [in mathcomp.solvable.gfunctor]
+gFunctorI [in mathcomp.solvable.gfunctor]
+gFunctorS [in mathcomp.solvable.gfunctor]
+GFunctor.continuous_is_iso_continuous [in mathcomp.solvable.gfunctor]
+GFunctor.pcontinuous_is_hereditary [in mathcomp.solvable.gfunctor]
+GFunctor.pcontinuous_is_continuous [in mathcomp.solvable.gfunctor]
+gF1 [in mathcomp.solvable.gfunctor]
+GLmx_faithful [in mathcomp.character.mxabelem]
+GL_det [in mathcomp.algebra.matrix]
+GL_unitmx [in mathcomp.algebra.matrix]
+GL_unit [in mathcomp.algebra.matrix]
+GL_MxE [in mathcomp.algebra.matrix]
+GL_ME [in mathcomp.algebra.matrix]
+GL_VxE [in mathcomp.algebra.matrix]
+GL_VE [in mathcomp.algebra.matrix]
+GL_1E [in mathcomp.algebra.matrix]
+GL_mx_repr [in mathcomp.character.mxabelem]
+grank_abelian [in mathcomp.solvable.abelian]
+grank_witness [in mathcomp.solvable.abelian]
+grank_min [in mathcomp.solvable.abelian]
+gring_classM_coef_sum_eq [in mathcomp.character.integral_char]
+gring_mode_class_sum_eq [in mathcomp.character.integral_char]
+gring_irr_modeM [in mathcomp.character.integral_char]
+gring_irr_mode_key [in mathcomp.character.integral_char]
+gring_classM_expansion [in mathcomp.character.integral_char]
+gring_class_sum_central [in mathcomp.character.integral_char]
+gring_opM [in mathcomp.character.mxrepresentation]
+gring_mxP [in mathcomp.character.mxrepresentation]
+gring_rowK [in mathcomp.character.mxrepresentation]
+gring_op_id [in mathcomp.character.mxrepresentation]
+gring_free [in mathcomp.character.mxrepresentation]
+gring_mxA [in mathcomp.character.mxrepresentation]
+gring_op_mx [in mathcomp.character.mxrepresentation]
+gring_opJ [in mathcomp.character.mxrepresentation]
+gring_op1 [in mathcomp.character.mxrepresentation]
+gring_opG [in mathcomp.character.mxrepresentation]
+gring_opE [in mathcomp.character.mxrepresentation]
+gring_mxK [in mathcomp.character.mxrepresentation]
+gring_mxJ [in mathcomp.character.mxrepresentation]
+gring_projE [in mathcomp.character.mxrepresentation]
+gring_row_mul [in mathcomp.character.mxrepresentation]
+gring_indexK [in mathcomp.character.mxrepresentation]
+gring_valK [in mathcomp.character.mxrepresentation]
+GRing.addf_div [in mathcomp.algebra.ssralg]
+GRing.addIr [in mathcomp.algebra.ssralg]
+GRing.addKr [in mathcomp.algebra.ssralg]
+GRing.addKr_char2 [in mathcomp.algebra.ssralg]
+GRing.addNKr [in mathcomp.algebra.ssralg]
+GRing.addNr [in mathcomp.algebra.ssralg]
+GRing.addrA [in mathcomp.algebra.ssralg]
+GRing.addrAC [in mathcomp.algebra.ssralg]
+GRing.addrACA [in mathcomp.algebra.ssralg]
+GRing.addrC [in mathcomp.algebra.ssralg]
+GRing.addrCA [in mathcomp.algebra.ssralg]
+GRing.addrI [in mathcomp.algebra.ssralg]
+GRing.addrK [in mathcomp.algebra.ssralg]
+GRing.addrKA [in mathcomp.algebra.ssralg]
+GRing.addrK_char2 [in mathcomp.algebra.ssralg]
+GRing.addrN [in mathcomp.algebra.ssralg]
+GRing.addrNK [in mathcomp.algebra.ssralg]
+GRing.addrr_char2 [in mathcomp.algebra.ssralg]
+GRing.addr_eq0 [in mathcomp.algebra.ssralg]
+GRing.addr0 [in mathcomp.algebra.ssralg]
+GRing.addr0_eq [in mathcomp.algebra.ssralg]
+GRing.add_fun_is_scalable [in mathcomp.algebra.ssralg]
+GRing.add_fun_is_additive [in mathcomp.algebra.ssralg]
+GRing.add0r [in mathcomp.algebra.ssralg]
+GRing.Algebra.comm_axiom [in mathcomp.algebra.ssralg]
+GRing.and_dnfP [in mathcomp.algebra.ssralg]
+GRing.bij_lrmorphism [in mathcomp.algebra.ssralg]
+GRing.bij_linear [in mathcomp.algebra.ssralg]
+GRing.bij_rmorphism [in mathcomp.algebra.ssralg]
+GRing.bij_additive [in mathcomp.algebra.ssralg]
+GRing.bin_lt_charf_0 [in mathcomp.algebra.ssralg]
+GRing.can2_lrmorphism [in mathcomp.algebra.ssralg]
+GRing.can2_linear [in mathcomp.algebra.ssralg]
+GRing.can2_rmorphism [in mathcomp.algebra.ssralg]
+GRing.can2_additive [in mathcomp.algebra.ssralg]
+GRing.cat_dnfP [in mathcomp.algebra.ssralg]
+GRing.charf_eq [in mathcomp.algebra.ssralg]
+GRing.charf_prime [in mathcomp.algebra.ssralg]
+GRing.charf'_nat [in mathcomp.algebra.ssralg]
+GRing.charf0 [in mathcomp.algebra.ssralg]
+GRing.charf0P [in mathcomp.algebra.ssralg]
+GRing.char_lalg [in mathcomp.algebra.ssralg]
+GRing.char0_natf_div [in mathcomp.algebra.ssralg]
+GRing.commrD [in mathcomp.algebra.ssralg]
+GRing.commrM [in mathcomp.algebra.ssralg]
+GRing.commrMn [in mathcomp.algebra.ssralg]
+GRing.commrN [in mathcomp.algebra.ssralg]
+GRing.commrN1 [in mathcomp.algebra.ssralg]
+GRing.commrV [in mathcomp.algebra.ssralg]
+GRing.commrX [in mathcomp.algebra.ssralg]
+GRing.commr_sign [in mathcomp.algebra.ssralg]
+GRing.commr_nat [in mathcomp.algebra.ssralg]
+GRing.commr_refl [in mathcomp.algebra.ssralg]
+GRing.commr_sym [in mathcomp.algebra.ssralg]
+GRing.commr0 [in mathcomp.algebra.ssralg]
+GRing.commr1 [in mathcomp.algebra.ssralg]
+GRing.comp_is_scalable [in mathcomp.algebra.ssralg]
+GRing.comp_is_multiplicative [in mathcomp.algebra.ssralg]
+GRing.comp_is_additive [in mathcomp.algebra.ssralg]
+GRing.ComUnitRing.mulC_unitP [in mathcomp.algebra.ssralg]
+GRing.ComUnitRing.mulC_mulrV [in mathcomp.algebra.ssralg]
+GRing.divalg_closedZ [in mathcomp.algebra.ssralg]
+GRing.divalg_closedBdiv [in mathcomp.algebra.ssralg]
+GRing.divff [in mathcomp.algebra.ssralg]
+GRing.divfI [in mathcomp.algebra.ssralg]
+GRing.divIf [in mathcomp.algebra.ssralg]
+GRing.divIr [in mathcomp.algebra.ssralg]
+GRing.divKf [in mathcomp.algebra.ssralg]
+GRing.divKr [in mathcomp.algebra.ssralg]
+GRing.divrI [in mathcomp.algebra.ssralg]
+GRing.divring_closed_div [in mathcomp.algebra.ssralg]
+GRing.divring_closedBM [in mathcomp.algebra.ssralg]
+GRing.divrr [in mathcomp.algebra.ssralg]
+GRing.divr_signM [in mathcomp.algebra.ssralg]
+GRing.divr_closedM [in mathcomp.algebra.ssralg]
+GRing.divr_closedV [in mathcomp.algebra.ssralg]
+GRing.divr1 [in mathcomp.algebra.ssralg]
+GRing.divr1_eq [in mathcomp.algebra.ssralg]
+GRing.div1r [in mathcomp.algebra.ssralg]
+GRing.dnf_to_rform [in mathcomp.algebra.ssralg]
+GRing.dnf_to_form_qf [in mathcomp.algebra.ssralg]
+GRing.dvdn_charf [in mathcomp.algebra.ssralg]
+GRing.eqf_sqr [in mathcomp.algebra.ssralg]
+GRing.eqr_oppLR [in mathcomp.algebra.ssralg]
+GRing.eqr_opp [in mathcomp.algebra.ssralg]
+GRing.eq_sol [in mathcomp.algebra.ssralg]
+GRing.eq_sat [in mathcomp.algebra.ssralg]
+GRing.eq_holds [in mathcomp.algebra.ssralg]
+GRing.eq_eval [in mathcomp.algebra.ssralg]
+GRing.eval_Pick [in mathcomp.algebra.ssralg]
+GRing.eval_If [in mathcomp.algebra.ssralg]
+GRing.eval_tsubst [in mathcomp.algebra.ssralg]
+GRing.expfB [in mathcomp.algebra.ssralg]
+GRing.expfB_cond [in mathcomp.algebra.ssralg]
+GRing.expfS_eq1 [in mathcomp.algebra.ssralg]
+GRing.expf_neq0 [in mathcomp.algebra.ssralg]
+GRing.expf_eq0 [in mathcomp.algebra.ssralg]
+GRing.exprAC [in mathcomp.algebra.ssralg]
+GRing.exprB [in mathcomp.algebra.ssralg]
+GRing.exprBn [in mathcomp.algebra.ssralg]
+GRing.exprBn_comm [in mathcomp.algebra.ssralg]
+GRing.exprD [in mathcomp.algebra.ssralg]
+GRing.exprDn [in mathcomp.algebra.ssralg]
+GRing.exprDn_char [in mathcomp.algebra.ssralg]
+GRing.exprDn_comm [in mathcomp.algebra.ssralg]
+GRing.exprD1n [in mathcomp.algebra.ssralg]
+GRing.exprM [in mathcomp.algebra.ssralg]
+GRing.exprMn [in mathcomp.algebra.ssralg]
+GRing.exprMn_n [in mathcomp.algebra.ssralg]
+GRing.exprMn_comm [in mathcomp.algebra.ssralg]
+GRing.exprNn [in mathcomp.algebra.ssralg]
+GRing.exprNn_char [in mathcomp.algebra.ssralg]
+GRing.exprS [in mathcomp.algebra.ssralg]
+GRing.exprSr [in mathcomp.algebra.ssralg]
+GRing.exprVn [in mathcomp.algebra.ssralg]
+GRing.exprZn [in mathcomp.algebra.ssralg]
+GRing.expr_div_n [in mathcomp.algebra.ssralg]
+GRing.expr_dvd [in mathcomp.algebra.ssralg]
+GRing.expr_mod [in mathcomp.algebra.ssralg]
+GRing.expr0 [in mathcomp.algebra.ssralg]
+GRing.expr0n [in mathcomp.algebra.ssralg]
+GRing.expr1 [in mathcomp.algebra.ssralg]
+GRing.expr1n [in mathcomp.algebra.ssralg]
+GRing.expr2 [in mathcomp.algebra.ssralg]
+GRing.fieldP [in mathcomp.algebra.ssralg]
+GRing.Field.IdomainMixin [in mathcomp.algebra.ssralg]
+GRing.Field.intro_unit [in mathcomp.algebra.ssralg]
+GRing.Field.inv_out [in mathcomp.algebra.ssralg]
+GRing.Field.Mixin [in mathcomp.algebra.ssralg]
+GRing.fmorphV [in mathcomp.algebra.ssralg]
+GRing.fmorph_div [in mathcomp.algebra.ssralg]
+GRing.fmorph_unit [in mathcomp.algebra.ssralg]
+GRing.fmorph_char [in mathcomp.algebra.ssralg]
+GRing.fmorph_eq1 [in mathcomp.algebra.ssralg]
+GRing.fmorph_inj [in mathcomp.algebra.ssralg]
+GRing.fmorph_eq0 [in mathcomp.algebra.ssralg]
+GRing.foldExistsP [in mathcomp.algebra.ssralg]
+GRing.foldForallP [in mathcomp.algebra.ssralg]
+GRing.fpredMl [in mathcomp.algebra.ssralg]
+GRing.fpredMr [in mathcomp.algebra.ssralg]
+GRing.fpred_divr [in mathcomp.algebra.ssralg]
+GRing.fpred_divl [in mathcomp.algebra.ssralg]
+GRing.Frobenius_aut_is_rmorphism [in mathcomp.algebra.ssralg]
+GRing.Frobenius_autB_comm [in mathcomp.algebra.ssralg]
+GRing.Frobenius_autN [in mathcomp.algebra.ssralg]
+GRing.Frobenius_autX [in mathcomp.algebra.ssralg]
+GRing.Frobenius_autM_comm [in mathcomp.algebra.ssralg]
+GRing.Frobenius_aut_nat [in mathcomp.algebra.ssralg]
+GRing.Frobenius_autMn [in mathcomp.algebra.ssralg]
+GRing.Frobenius_autD_comm [in mathcomp.algebra.ssralg]
+GRing.Frobenius_aut1 [in mathcomp.algebra.ssralg]
+GRing.Frobenius_aut0 [in mathcomp.algebra.ssralg]
+GRing.Frobenius_autE [in mathcomp.algebra.ssralg]
+GRing.holds_fsubst [in mathcomp.algebra.ssralg]
+GRing.idfun_is_scalable [in mathcomp.algebra.ssralg]
+GRing.idfun_is_multiplicative [in mathcomp.algebra.ssralg]
+GRing.idfun_is_additive [in mathcomp.algebra.ssralg]
+GRing.If_form_rf [in mathcomp.algebra.ssralg]
+GRing.If_form_qf [in mathcomp.algebra.ssralg]
+GRing.imaginary_exists [in mathcomp.algebra.ssralg]
+GRing.invfM [in mathcomp.algebra.ssralg]
+GRing.invf_div [in mathcomp.algebra.ssralg]
+GRing.invrK [in mathcomp.algebra.ssralg]
+GRing.invrM [in mathcomp.algebra.ssralg]
+GRing.invrN [in mathcomp.algebra.ssralg]
+GRing.invrN1 [in mathcomp.algebra.ssralg]
+GRing.invrZ [in mathcomp.algebra.ssralg]
+GRing.invr_signM [in mathcomp.algebra.ssralg]
+GRing.invr_eq1 [in mathcomp.algebra.ssralg]
+GRing.invr_eq0 [in mathcomp.algebra.ssralg]
+GRing.invr_neq0 [in mathcomp.algebra.ssralg]
+GRing.invr_sign [in mathcomp.algebra.ssralg]
+GRing.invr_inj [in mathcomp.algebra.ssralg]
+GRing.invr_out [in mathcomp.algebra.ssralg]
+GRing.invr0 [in mathcomp.algebra.ssralg]
+GRing.invr1 [in mathcomp.algebra.ssralg]
+GRing.in_algE [in mathcomp.algebra.ssralg]
+GRing.in_alg_is_rmorphism [in mathcomp.algebra.ssralg]
+GRing.linearB [in mathcomp.algebra.ssralg]
+GRing.linearD [in mathcomp.algebra.ssralg]
+GRing.linearMn [in mathcomp.algebra.ssralg]
+GRing.linearMNn [in mathcomp.algebra.ssralg]
+GRing.linearN [in mathcomp.algebra.ssralg]
+GRing.linearP [in mathcomp.algebra.ssralg]
+GRing.linearPZ [in mathcomp.algebra.ssralg]
+GRing.linearZ [in mathcomp.algebra.ssralg]
+GRing.linearZZ [in mathcomp.algebra.ssralg]
+GRing.linearZ_LR [in mathcomp.algebra.ssralg]
+GRing.linear_sum [in mathcomp.algebra.ssralg]
+GRing.linear_closedB [in mathcomp.algebra.ssralg]
+GRing.Linear.class_of_axiom [in mathcomp.algebra.ssralg]
+GRing.linear0 [in mathcomp.algebra.ssralg]
+GRing.locked_is_scalable [in mathcomp.algebra.ssralg]
+GRing.locked_is_multiplicative [in mathcomp.algebra.ssralg]
+GRing.locked_is_additive [in mathcomp.algebra.ssralg]
+GRing.lregM [in mathcomp.algebra.ssralg]
+GRing.lregN [in mathcomp.algebra.ssralg]
+GRing.lregP [in mathcomp.algebra.ssralg]
+GRing.lregX [in mathcomp.algebra.ssralg]
+GRing.lreg_sign [in mathcomp.algebra.ssralg]
+GRing.lreg_neq0 [in mathcomp.algebra.ssralg]
+GRing.lreg1 [in mathcomp.algebra.ssralg]
+GRing.lrmorphismP [in mathcomp.algebra.ssralg]
+GRing.mulfI [in mathcomp.algebra.ssralg]
+GRing.mulfK [in mathcomp.algebra.ssralg]
+GRing.mulfVK [in mathcomp.algebra.ssralg]
+GRing.mulf_div [in mathcomp.algebra.ssralg]
+GRing.mulf_neq0 [in mathcomp.algebra.ssralg]
+GRing.mulf_eq0 [in mathcomp.algebra.ssralg]
+GRing.mulIf [in mathcomp.algebra.ssralg]
+GRing.mulIr [in mathcomp.algebra.ssralg]
+GRing.mulIr_eq0 [in mathcomp.algebra.ssralg]
+GRing.mulIr0_rreg [in mathcomp.algebra.ssralg]
+GRing.mulKf [in mathcomp.algebra.ssralg]
+GRing.mulKr [in mathcomp.algebra.ssralg]
+GRing.mull_fun_is_scalable [in mathcomp.algebra.ssralg]
+GRing.mull_fun_is_additive [in mathcomp.algebra.ssralg]
+GRing.mulNr [in mathcomp.algebra.ssralg]
+GRing.mulNrn [in mathcomp.algebra.ssralg]
+GRing.mulN1r [in mathcomp.algebra.ssralg]
+GRing.mulrA [in mathcomp.algebra.ssralg]
+GRing.mulrAC [in mathcomp.algebra.ssralg]
+GRing.mulrACA [in mathcomp.algebra.ssralg]
+GRing.mulrb [in mathcomp.algebra.ssralg]
+GRing.mulrBl [in mathcomp.algebra.ssralg]
+GRing.mulrBr [in mathcomp.algebra.ssralg]
+GRing.mulrC [in mathcomp.algebra.ssralg]
+GRing.mulrCA [in mathcomp.algebra.ssralg]
+GRing.mulrDl [in mathcomp.algebra.ssralg]
+GRing.mulrDr [in mathcomp.algebra.ssralg]
+GRing.mulrI [in mathcomp.algebra.ssralg]
+GRing.mulrI_eq0 [in mathcomp.algebra.ssralg]
+GRing.mulrI0_lreg [in mathcomp.algebra.ssralg]
+GRing.mulrK [in mathcomp.algebra.ssralg]
+GRing.mulrN [in mathcomp.algebra.ssralg]
+GRing.mulrnA [in mathcomp.algebra.ssralg]
+GRing.mulrnAC [in mathcomp.algebra.ssralg]
+GRing.mulrnAl [in mathcomp.algebra.ssralg]
+GRing.mulrnAr [in mathcomp.algebra.ssralg]
+GRing.mulrnBl [in mathcomp.algebra.ssralg]
+GRing.mulrnBr [in mathcomp.algebra.ssralg]
+GRing.mulrnDl [in mathcomp.algebra.ssralg]
+GRing.mulrnDr [in mathcomp.algebra.ssralg]
+GRing.mulrNN [in mathcomp.algebra.ssralg]
+GRing.mulrn_char [in mathcomp.algebra.ssralg]
+GRing.mulrN1 [in mathcomp.algebra.ssralg]
+GRing.mulrS [in mathcomp.algebra.ssralg]
+GRing.mulrSr [in mathcomp.algebra.ssralg]
+GRing.mulrVK [in mathcomp.algebra.ssralg]
+GRing.mulr_algr [in mathcomp.algebra.ssralg]
+GRing.mulr_fun_is_scalable [in mathcomp.algebra.ssralg]
+GRing.mulr_fun_is_additive [in mathcomp.algebra.ssralg]
+GRing.mulr_algl [in mathcomp.algebra.ssralg]
+GRing.mulr_signM [in mathcomp.algebra.ssralg]
+GRing.mulr_sign [in mathcomp.algebra.ssralg]
+GRing.mulr_natr [in mathcomp.algebra.ssralg]
+GRing.mulr_natl [in mathcomp.algebra.ssralg]
+GRing.mulr_sumr [in mathcomp.algebra.ssralg]
+GRing.mulr_suml [in mathcomp.algebra.ssralg]
+GRing.mulr0 [in mathcomp.algebra.ssralg]
+GRing.mulr0n [in mathcomp.algebra.ssralg]
+GRing.mulr1 [in mathcomp.algebra.ssralg]
+GRing.mulr1n [in mathcomp.algebra.ssralg]
+GRing.mulr1_eq [in mathcomp.algebra.ssralg]
+GRing.mulr2n [in mathcomp.algebra.ssralg]
+GRing.mulVf [in mathcomp.algebra.ssralg]
+GRing.mulVKf [in mathcomp.algebra.ssralg]
+GRing.mulVKr [in mathcomp.algebra.ssralg]
+GRing.mulVr [in mathcomp.algebra.ssralg]
+GRing.mul0r [in mathcomp.algebra.ssralg]
+GRing.mul0rn [in mathcomp.algebra.ssralg]
+GRing.mul1r [in mathcomp.algebra.ssralg]
+GRing.natf_neq0 [in mathcomp.algebra.ssralg]
+GRing.natf0_char [in mathcomp.algebra.ssralg]
+GRing.natrB [in mathcomp.algebra.ssralg]
+GRing.natrD [in mathcomp.algebra.ssralg]
+GRing.natrM [in mathcomp.algebra.ssralg]
+GRing.natrX [in mathcomp.algebra.ssralg]
+GRing.natr_div [in mathcomp.algebra.ssralg]
+GRing.natr_mod_char [in mathcomp.algebra.ssralg]
+GRing.natr_prod [in mathcomp.algebra.ssralg]
+GRing.null_fun_is_scalable [in mathcomp.algebra.ssralg]
+GRing.null_fun_is_additive [in mathcomp.algebra.ssralg]
+GRing.oner_eq0 [in mathcomp.algebra.ssralg]
+GRing.oner_neq0 [in mathcomp.algebra.ssralg]
+GRing.opprB [in mathcomp.algebra.ssralg]
+GRing.opprD [in mathcomp.algebra.ssralg]
+GRing.opprK [in mathcomp.algebra.ssralg]
+GRing.oppr_char2 [in mathcomp.algebra.ssralg]
+GRing.oppr_eq0 [in mathcomp.algebra.ssralg]
+GRing.oppr_inj [in mathcomp.algebra.ssralg]
+GRing.oppr0 [in mathcomp.algebra.ssralg]
+GRing.opp_is_scalable [in mathcomp.algebra.ssralg]
+GRing.opp_is_additive [in mathcomp.algebra.ssralg]
+GRing.Pick_form_qf [in mathcomp.algebra.ssralg]
+GRing.Pred.add_ext [in mathcomp.algebra.ssralg]
+GRing.Pred.divalg_scaler [in mathcomp.algebra.ssralg]
+GRing.Pred.divring_invr [in mathcomp.algebra.ssralg]
+GRing.Pred.inv_ext [in mathcomp.algebra.ssralg]
+GRing.Pred.mul_ext [in mathcomp.algebra.ssralg]
+GRing.Pred.opp_ext [in mathcomp.algebra.ssralg]
+GRing.Pred.scale_ext [in mathcomp.algebra.ssralg]
+GRing.Pred.sdiv_invr [in mathcomp.algebra.ssralg]
+GRing.Pred.semiring_mulr [in mathcomp.algebra.ssralg]
+GRing.Pred.smul_mulr [in mathcomp.algebra.ssralg]
+GRing.Pred.subalg_scaler [in mathcomp.algebra.ssralg]
+GRing.Pred.submod_scaler [in mathcomp.algebra.ssralg]
+GRing.Pred.subring_mulr [in mathcomp.algebra.ssralg]
+GRing.Pred.zmod_oppr [in mathcomp.algebra.ssralg]
+GRing.prodfV [in mathcomp.algebra.ssralg]
+GRing.prodf_div [in mathcomp.algebra.ssralg]
+GRing.prodf_seq_neq0 [in mathcomp.algebra.ssralg]
+GRing.prodf_neq0 [in mathcomp.algebra.ssralg]
+GRing.prodf_seq_eq0 [in mathcomp.algebra.ssralg]
+GRing.prodf_eq0 [in mathcomp.algebra.ssralg]
+GRing.prodrMn [in mathcomp.algebra.ssralg]
+GRing.prodrN [in mathcomp.algebra.ssralg]
+GRing.prodrXl [in mathcomp.algebra.ssralg]
+GRing.prodrXr [in mathcomp.algebra.ssralg]
+GRing.prodr_undup_exp_count [in mathcomp.algebra.ssralg]
+GRing.prodr_const [in mathcomp.algebra.ssralg]
+GRing.proj_satP [in mathcomp.algebra.ssralg]
+GRing.qf_to_dnf_rterm [in mathcomp.algebra.ssralg]
+GRing.qf_to_dnfP [in mathcomp.algebra.ssralg]
+GRing.qf_evalP [in mathcomp.algebra.ssralg]
+GRing.quantifier_elim_rformP [in mathcomp.algebra.ssralg]
+GRing.quantifier_elim_wf [in mathcomp.algebra.ssralg]
+GRing.raddfB [in mathcomp.algebra.ssralg]
+GRing.raddfD [in mathcomp.algebra.ssralg]
+GRing.raddfMn [in mathcomp.algebra.ssralg]
+GRing.raddfMnat [in mathcomp.algebra.ssralg]
+GRing.raddfMNn [in mathcomp.algebra.ssralg]
+GRing.raddfMsign [in mathcomp.algebra.ssralg]
+GRing.raddfN [in mathcomp.algebra.ssralg]
+GRing.raddfZnat [in mathcomp.algebra.ssralg]
+GRing.raddfZsign [in mathcomp.algebra.ssralg]
+GRing.raddf_sum [in mathcomp.algebra.ssralg]
+GRing.raddf_eq0 [in mathcomp.algebra.ssralg]
+GRing.raddf0 [in mathcomp.algebra.ssralg]
+GRing.revrX [in mathcomp.algebra.ssralg]
+GRing.rev_unitrP [in mathcomp.algebra.ssralg]
+GRing.rmorphB [in mathcomp.algebra.ssralg]
+GRing.rmorphD [in mathcomp.algebra.ssralg]
+GRing.rmorphismMP [in mathcomp.algebra.ssralg]
+GRing.rmorphismP [in mathcomp.algebra.ssralg]
+GRing.rmorphM [in mathcomp.algebra.ssralg]
+GRing.rmorphMn [in mathcomp.algebra.ssralg]
+GRing.rmorphMNn [in mathcomp.algebra.ssralg]
+GRing.rmorphMsign [in mathcomp.algebra.ssralg]
+GRing.rmorphN [in mathcomp.algebra.ssralg]
+GRing.rmorphN1 [in mathcomp.algebra.ssralg]
+GRing.rmorphV [in mathcomp.algebra.ssralg]
+GRing.rmorphX [in mathcomp.algebra.ssralg]
+GRing.rmorph_div [in mathcomp.algebra.ssralg]
+GRing.rmorph_unit [in mathcomp.algebra.ssralg]
+GRing.rmorph_comm [in mathcomp.algebra.ssralg]
+GRing.rmorph_alg [in mathcomp.algebra.ssralg]
+GRing.rmorph_eq1 [in mathcomp.algebra.ssralg]
+GRing.rmorph_eq_nat [in mathcomp.algebra.ssralg]
+GRing.rmorph_char [in mathcomp.algebra.ssralg]
+GRing.rmorph_sign [in mathcomp.algebra.ssralg]
+GRing.rmorph_nat [in mathcomp.algebra.ssralg]
+GRing.rmorph_prod [in mathcomp.algebra.ssralg]
+GRing.rmorph_sum [in mathcomp.algebra.ssralg]
+GRing.rmorph0 [in mathcomp.algebra.ssralg]
+GRing.rmorph1 [in mathcomp.algebra.ssralg]
+GRing.rpredB [in mathcomp.algebra.ssralg]
+GRing.rpredBl [in mathcomp.algebra.ssralg]
+GRing.rpredBr [in mathcomp.algebra.ssralg]
+GRing.rpredD [in mathcomp.algebra.ssralg]
+GRing.rpredDl [in mathcomp.algebra.ssralg]
+GRing.rpredDr [in mathcomp.algebra.ssralg]
+GRing.rpredM [in mathcomp.algebra.ssralg]
+GRing.rpredMl [in mathcomp.algebra.ssralg]
+GRing.rpredMn [in mathcomp.algebra.ssralg]
+GRing.rpredMNn [in mathcomp.algebra.ssralg]
+GRing.rpredMr [in mathcomp.algebra.ssralg]
+GRing.rpredMsign [in mathcomp.algebra.ssralg]
+GRing.rpredN [in mathcomp.algebra.ssralg]
+GRing.rpredNr [in mathcomp.algebra.ssralg]
+GRing.rpredN1 [in mathcomp.algebra.ssralg]
+GRing.rpredV [in mathcomp.algebra.ssralg]
+GRing.rpredVr [in mathcomp.algebra.ssralg]
+GRing.rpredX [in mathcomp.algebra.ssralg]
+GRing.rpredXN [in mathcomp.algebra.ssralg]
+GRing.rpredZ [in mathcomp.algebra.ssralg]
+GRing.rpredZeq [in mathcomp.algebra.ssralg]
+GRing.rpredZnat [in mathcomp.algebra.ssralg]
+GRing.rpredZsign [in mathcomp.algebra.ssralg]
+GRing.rpred_divl [in mathcomp.algebra.ssralg]
+GRing.rpred_divr [in mathcomp.algebra.ssralg]
+GRing.rpred_div [in mathcomp.algebra.ssralg]
+GRing.rpred_sign [in mathcomp.algebra.ssralg]
+GRing.rpred_nat [in mathcomp.algebra.ssralg]
+GRing.rpred_prod [in mathcomp.algebra.ssralg]
+GRing.rpred_sum [in mathcomp.algebra.ssralg]
+GRing.rpred0 [in mathcomp.algebra.ssralg]
+GRing.rpred0D [in mathcomp.algebra.ssralg]
+GRing.rpred1 [in mathcomp.algebra.ssralg]
+GRing.rpred1M [in mathcomp.algebra.ssralg]
+GRing.rregM [in mathcomp.algebra.ssralg]
+GRing.rregN [in mathcomp.algebra.ssralg]
+GRing.rregP [in mathcomp.algebra.ssralg]
+GRing.rregX [in mathcomp.algebra.ssralg]
+GRing.rreg_neq0 [in mathcomp.algebra.ssralg]
+GRing.rreg1 [in mathcomp.algebra.ssralg]
+GRing.same_env_sym [in mathcomp.algebra.ssralg]
+GRing.satP [in mathcomp.algebra.ssralg]
+GRing.scalarP [in mathcomp.algebra.ssralg]
+GRing.scalarZ [in mathcomp.algebra.ssralg]
+GRing.scaleNr [in mathcomp.algebra.ssralg]
+GRing.scaleN1r [in mathcomp.algebra.ssralg]
+GRing.scalerA [in mathcomp.algebra.ssralg]
+GRing.scalerAl [in mathcomp.algebra.ssralg]
+GRing.scalerAr [in mathcomp.algebra.ssralg]
+GRing.scalerBl [in mathcomp.algebra.ssralg]
+GRing.scalerBr [in mathcomp.algebra.ssralg]
+GRing.scalerCA [in mathcomp.algebra.ssralg]
+GRing.scalerDl [in mathcomp.algebra.ssralg]
+GRing.scalerDr [in mathcomp.algebra.ssralg]
+GRing.scalerI [in mathcomp.algebra.ssralg]
+GRing.scalerK [in mathcomp.algebra.ssralg]
+GRing.scalerKV [in mathcomp.algebra.ssralg]
+GRing.scalerMnl [in mathcomp.algebra.ssralg]
+GRing.scalerMnr [in mathcomp.algebra.ssralg]
+GRing.scalerN [in mathcomp.algebra.ssralg]
+GRing.scaler_eq0 [in mathcomp.algebra.ssralg]
+GRing.scaler_unit [in mathcomp.algebra.ssralg]
+GRing.scaler_injl [in mathcomp.algebra.ssralg]
+GRing.scaler_prodr [in mathcomp.algebra.ssralg]
+GRing.scaler_prodl [in mathcomp.algebra.ssralg]
+GRing.scaler_prod [in mathcomp.algebra.ssralg]
+GRing.scaler_sumr [in mathcomp.algebra.ssralg]
+GRing.scaler_suml [in mathcomp.algebra.ssralg]
+GRing.scaler_sign [in mathcomp.algebra.ssralg]
+GRing.scaler_nat [in mathcomp.algebra.ssralg]
+GRing.scaler0 [in mathcomp.algebra.ssralg]
+GRing.scale_fun_is_scalable [in mathcomp.algebra.ssralg]
+GRing.scale_is_scalable [in mathcomp.algebra.ssralg]
+GRing.Scale.compN1op [in mathcomp.algebra.ssralg]
+GRing.Scale.comp_opE [in mathcomp.algebra.ssralg]
+GRing.Scale.N1op [in mathcomp.algebra.ssralg]
+GRing.Scale.opB [in mathcomp.algebra.ssralg]
+GRing.Scale.opE [in mathcomp.algebra.ssralg]
+GRing.scale0r [in mathcomp.algebra.ssralg]
+GRing.scale1r [in mathcomp.algebra.ssralg]
+GRing.sdivr_closedM [in mathcomp.algebra.ssralg]
+GRing.sdivr_closed_div [in mathcomp.algebra.ssralg]
+GRing.semiring_closedM [in mathcomp.algebra.ssralg]
+GRing.semiring_closedD [in mathcomp.algebra.ssralg]
+GRing.signrE [in mathcomp.algebra.ssralg]
+GRing.signrMK [in mathcomp.algebra.ssralg]
+GRing.signrN [in mathcomp.algebra.ssralg]
+GRing.signrZK [in mathcomp.algebra.ssralg]
+GRing.signr_addb [in mathcomp.algebra.ssralg]
+GRing.signr_eq0 [in mathcomp.algebra.ssralg]
+GRing.signr_odd [in mathcomp.algebra.ssralg]
+GRing.size_sol [in mathcomp.algebra.ssralg]
+GRing.smulr_closedN [in mathcomp.algebra.ssralg]
+GRing.smulr_closedM [in mathcomp.algebra.ssralg]
+GRing.solP [in mathcomp.algebra.ssralg]
+GRing.solve_monicpoly [in mathcomp.algebra.ssralg]
+GRing.sol_subproof [in mathcomp.algebra.ssralg]
+GRing.sqrf_eq1 [in mathcomp.algebra.ssralg]
+GRing.sqrf_eq0 [in mathcomp.algebra.ssralg]
+GRing.sqrrB [in mathcomp.algebra.ssralg]
+GRing.sqrrB1 [in mathcomp.algebra.ssralg]
+GRing.sqrrD [in mathcomp.algebra.ssralg]
+GRing.sqrrD1 [in mathcomp.algebra.ssralg]
+GRing.sqrrN [in mathcomp.algebra.ssralg]
+GRing.sqrr_sign [in mathcomp.algebra.ssralg]
+GRing.subalg_closedBM [in mathcomp.algebra.ssralg]
+GRing.subalg_closedZ [in mathcomp.algebra.ssralg]
+GRing.subIr [in mathcomp.algebra.ssralg]
+GRing.subKr [in mathcomp.algebra.ssralg]
+GRing.submod_closedZ [in mathcomp.algebra.ssralg]
+GRing.submod_closedB [in mathcomp.algebra.ssralg]
+GRing.subrI [in mathcomp.algebra.ssralg]
+GRing.subring_closed_semi [in mathcomp.algebra.ssralg]
+GRing.subring_closedM [in mathcomp.algebra.ssralg]
+GRing.subring_closedB [in mathcomp.algebra.ssralg]
+GRing.subrKA [in mathcomp.algebra.ssralg]
+GRing.subrXX [in mathcomp.algebra.ssralg]
+GRing.subrXX_comm [in mathcomp.algebra.ssralg]
+GRing.subrX1 [in mathcomp.algebra.ssralg]
+GRing.subr_sqrDB [in mathcomp.algebra.ssralg]
+GRing.subr_sqr [in mathcomp.algebra.ssralg]
+GRing.subr_char2 [in mathcomp.algebra.ssralg]
+GRing.subr_sqr_1 [in mathcomp.algebra.ssralg]
+GRing.subr_eq0 [in mathcomp.algebra.ssralg]
+GRing.subr_eq [in mathcomp.algebra.ssralg]
+GRing.subr0 [in mathcomp.algebra.ssralg]
+GRing.subr0_eq [in mathcomp.algebra.ssralg]
+GRing.SubType.addA [in mathcomp.algebra.ssralg]
+GRing.SubType.addC [in mathcomp.algebra.ssralg]
+GRing.SubType.addN [in mathcomp.algebra.ssralg]
+GRing.SubType.add0 [in mathcomp.algebra.ssralg]
+GRing.SubType.algMixin [in mathcomp.algebra.ssralg]
+GRing.SubType.comRingMixin [in mathcomp.algebra.ssralg]
+GRing.SubType.fieldMixin [in mathcomp.algebra.ssralg]
+GRing.SubType.idomainMixin [in mathcomp.algebra.ssralg]
+GRing.SubType.lalgMixin [in mathcomp.algebra.ssralg]
+GRing.SubType.mulA [in mathcomp.algebra.ssralg]
+GRing.SubType.mulDl [in mathcomp.algebra.ssralg]
+GRing.SubType.mulDr [in mathcomp.algebra.ssralg]
+GRing.SubType.mulrV [in mathcomp.algebra.ssralg]
+GRing.SubType.mulVr [in mathcomp.algebra.ssralg]
+GRing.SubType.mul1l [in mathcomp.algebra.ssralg]
+GRing.SubType.mul1r [in mathcomp.algebra.ssralg]
+GRing.SubType.nz1 [in mathcomp.algebra.ssralg]
+GRing.SubType.scaleA [in mathcomp.algebra.ssralg]
+GRing.SubType.scaleDl [in mathcomp.algebra.ssralg]
+GRing.SubType.scaleDr [in mathcomp.algebra.ssralg]
+GRing.SubType.scale1 [in mathcomp.algebra.ssralg]
+GRing.SubType.unitP [in mathcomp.algebra.ssralg]
+GRing.SubType.unit_id [in mathcomp.algebra.ssralg]
+GRing.sub_fun_is_scalable [in mathcomp.algebra.ssralg]
+GRing.sub_fun_is_additive [in mathcomp.algebra.ssralg]
+GRing.sub0r [in mathcomp.algebra.ssralg]
+GRing.sumrB [in mathcomp.algebra.ssralg]
+GRing.sumrMnl [in mathcomp.algebra.ssralg]
+GRing.sumrMnr [in mathcomp.algebra.ssralg]
+GRing.sumrN [in mathcomp.algebra.ssralg]
+GRing.sumr_const [in mathcomp.algebra.ssralg]
+GRing.telescope_prodf [in mathcomp.algebra.ssralg]
+GRing.telescope_prodr [in mathcomp.algebra.ssralg]
+GRing.telescope_sumr [in mathcomp.algebra.ssralg]
+GRing.to_rformP [in mathcomp.algebra.ssralg]
+GRing.to_rform_rformula [in mathcomp.algebra.ssralg]
+GRing.to_rterm_id [in mathcomp.algebra.ssralg]
+GRing.unitfE [in mathcomp.algebra.ssralg]
+GRing.unitrE [in mathcomp.algebra.ssralg]
+GRing.unitrM [in mathcomp.algebra.ssralg]
+GRing.unitrMl [in mathcomp.algebra.ssralg]
+GRing.unitrMr [in mathcomp.algebra.ssralg]
+GRing.unitrM_comm [in mathcomp.algebra.ssralg]
+GRing.unitrN [in mathcomp.algebra.ssralg]
+GRing.unitrN1 [in mathcomp.algebra.ssralg]
+GRing.unitrP [in mathcomp.algebra.ssralg]
+GRing.unitrPr [in mathcomp.algebra.ssralg]
+GRing.unitrV [in mathcomp.algebra.ssralg]
+GRing.unitrX [in mathcomp.algebra.ssralg]
+GRing.unitrX_pos [in mathcomp.algebra.ssralg]
+GRing.unitr_sdivr_closed [in mathcomp.algebra.ssralg]
+GRing.unitr0 [in mathcomp.algebra.ssralg]
+GRing.unitr1 [in mathcomp.algebra.ssralg]
+GRing.unit_key [in mathcomp.algebra.ssralg]
+GRing.zmod_closedD [in mathcomp.algebra.ssralg]
+GRing.zmod_closedN [in mathcomp.algebra.ssralg]
+groupC [in mathcomp.character.character]
+groupD1_inj [in mathcomp.fingroup.fingroup]
+groupJ [in mathcomp.fingroup.fingroup]
+groupJr [in mathcomp.fingroup.fingroup]
+groupM [in mathcomp.fingroup.fingroup]
+groupMl [in mathcomp.fingroup.fingroup]
+groupMr [in mathcomp.fingroup.fingroup]
+groupP [in mathcomp.fingroup.fingroup]
+groupR [in mathcomp.fingroup.fingroup]
+groupV [in mathcomp.fingroup.fingroup]
+groupVl [in mathcomp.fingroup.fingroup]
+groupVr [in mathcomp.fingroup.fingroup]
+groupX [in mathcomp.fingroup.fingroup]
+group_num_field_exists [in mathcomp.character.integral_char]
+group_closure_closed_field [in mathcomp.character.mxrepresentation]
+group_closure_field_exists [in mathcomp.character.mxrepresentation]
+group_splitting_field_exists [in mathcomp.character.mxrepresentation]
+group_setX [in mathcomp.fingroup.gproduct]
+group_not0 [in mathcomp.fingroup.gproduct]
+group_set_inertia [in mathcomp.character.inertia]
+group_Ldiv [in mathcomp.solvable.abelian]
+group_set_gacent [in mathcomp.fingroup.action]
+group_set_astabs [in mathcomp.fingroup.action]
+group_set_astab [in mathcomp.fingroup.action]
+group_set_normaliser [in mathcomp.fingroup.fingroup]
+group_set_bigcap [in mathcomp.fingroup.fingroup]
+group_setI [in mathcomp.fingroup.fingroup]
+group_modr [in mathcomp.fingroup.fingroup]
+group_modl [in mathcomp.fingroup.fingroup]
+group_set_conjG [in mathcomp.fingroup.fingroup]
+group_setJ [in mathcomp.fingroup.fingroup]
+group_prod [in mathcomp.fingroup.fingroup]
+group_setT [in mathcomp.fingroup.fingroup]
+group_set_one [in mathcomp.fingroup.fingroup]
+group_inj [in mathcomp.fingroup.fingroup]
+group_setP [in mathcomp.fingroup.fingroup]
+group_set_diso3 [in mathcomp.solvable.burnside_app]
+group_set_iso3 [in mathcomp.solvable.burnside_app]
+group_set_rotations [in mathcomp.solvable.burnside_app]
+group_set_iso [in mathcomp.solvable.burnside_app]
+group_set_iso2 [in mathcomp.solvable.burnside_app]
+group_set_rot [in mathcomp.solvable.burnside_app]
+group0 [in mathcomp.fingroup.gproduct]
+group1 [in mathcomp.fingroup.fingroup]
+group1_contra [in mathcomp.fingroup.fingroup]
+group1_finType [in mathcomp.fingroup.fingroup]
+group1_eqType [in mathcomp.fingroup.fingroup]
+group1_class12 [in mathcomp.fingroup.fingroup]
+group1_class2 [in mathcomp.fingroup.fingroup]
+group1_class1 [in mathcomp.fingroup.fingroup]
+Grp_pX1p2 [in mathcomp.solvable.extraspecial]
+Grp_quaternion [in mathcomp.solvable.extremal]
+Grp_semidihedral [in mathcomp.solvable.extremal]
+Grp_2dihedral [in mathcomp.solvable.extremal]
+Grp_dihedral [in mathcomp.solvable.extremal]
+Grp_ext_dihedral [in mathcomp.solvable.extremal]
+Grp_modular_group [in mathcomp.solvable.extremal]
+Grp'_dihedral [in mathcomp.solvable.extremal]
+gtnNdvd [in mathcomp.ssreflect.div]
+gtn_min [in mathcomp.ssreflect.ssrnat]
+gtn_max [in mathcomp.ssreflect.ssrnat]
+gtn_eqF [in mathcomp.ssreflect.ssrnat]
+gtr0_sgz [in mathcomp.algebra.ssrint]
+gtz0_abs [in mathcomp.algebra.ssrint]
+gtz0_ge1 [in mathcomp.algebra.ssrint]
+gt_rat0 [in mathcomp.algebra.rat]
+gt0CG [in mathcomp.character.classfun]
+gt0CiG [in mathcomp.character.classfun]
+
| 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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 entries) | +
| Axiom 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +