| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 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.lastr_eq0 [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]
-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]
-gt_size_poly_neq0 [in mathcomp.algebra.poly]
-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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -