| 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 | (71649 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 | (1792 entries) |
| Binder 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 | (46193 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 | (266 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 | (3623 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 | (91 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 | (14204 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 | (259 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 | (8 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 | (134 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 | (44 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 | (1276 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 | (682 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 | (3041 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 | (36 entries) |
G (definition)
gacent [in mathcomp.fingroup.action]gacent_group [in mathcomp.fingroup.action]
gact_range [in mathcomp.fingroup.action]
gal [in mathcomp.field.galois]
galNorm [in mathcomp.field.galois]
galois [in mathcomp.field.galois]
galoisG [in mathcomp.field.galois]
galoisG_group [in mathcomp.field.galois]
galTrace [in mathcomp.field.galois]
gal_morphism [in mathcomp.field.galois]
gal_repr [in mathcomp.field.galois]
gal_mul [in mathcomp.field.galois]
gal_inv [in mathcomp.field.galois]
gal_one [in mathcomp.field.galois]
gal_sgval [in mathcomp.field.galois]
Gaussian_elimination_unlockable [in mathcomp.algebra.mxalgebra]
Gaussian_elimination_ [in mathcomp.algebra.mxalgebra]
gcard [in mathcomp.character.mxrepresentation]
gcdn [in mathcomp.ssreflect.div]
gcdn_rec [in mathcomp.ssreflect.div]
gcdz [in mathcomp.algebra.intdiv]
gcore [in mathcomp.fingroup.fingroup]
gcore_group [in mathcomp.fingroup.fingroup]
geigenspace [in mathcomp.algebra.mxpoly]
generated_group [in mathcomp.fingroup.fingroup]
generated_unlockable [in mathcomp.fingroup.fingroup]
generator [in mathcomp.solvable.cyclic]
genmx_unlockable [in mathcomp.algebra.mxalgebra]
genmx_witness [in mathcomp.algebra.mxalgebra]
GenTree.decode [in mathcomp.ssreflect.choice]
GenTree.decode_step [in mathcomp.ssreflect.choice]
GenTree.encode [in mathcomp.ssreflect.choice]
GenTree.tree_ind [in mathcomp.ssreflect.choice]
GenTree.tree_rec [in mathcomp.ssreflect.choice]
GenTree.tree_rect [in mathcomp.ssreflect.choice]
gen_rank [in mathcomp.solvable.abelian]
geq [in mathcomp.ssreflect.ssrnat]
gFcomp_mgFun [in mathcomp.solvable.gfunctor]
gFcomp_gFun [in mathcomp.solvable.gfunctor]
gFcomp_igFun [in mathcomp.solvable.gfunctor]
gFgroup [in mathcomp.solvable.gfunctor]
gFmod_pgFun [in mathcomp.solvable.gfunctor]
gFmod_gFun [in mathcomp.solvable.gfunctor]
gFmod_igFun [in mathcomp.solvable.gfunctor]
gFmod_group [in mathcomp.solvable.gfunctor]
GFunctor.clone [in mathcomp.solvable.gfunctor]
GFunctor.clone_mono [in mathcomp.solvable.gfunctor]
GFunctor.clone_pmap [in mathcomp.solvable.gfunctor]
GFunctor.clone_iso [in mathcomp.solvable.gfunctor]
GFunctor.closed [in mathcomp.solvable.gfunctor]
GFunctor.comp [in mathcomp.solvable.gfunctor]
GFunctor.continuous [in mathcomp.solvable.gfunctor]
GFunctor.group_valued [in mathcomp.solvable.gfunctor]
GFunctor.hereditary [in mathcomp.solvable.gfunctor]
GFunctor.iso_continuous [in mathcomp.solvable.gfunctor]
GFunctor.modulo [in mathcomp.solvable.gfunctor]
GFunctor.monotonic [in mathcomp.solvable.gfunctor]
GFunctor.object_map [in mathcomp.solvable.gfunctor]
GFunctor.pack_iso [in mathcomp.solvable.gfunctor]
GFunctor.pcontinuous [in mathcomp.solvable.gfunctor]
gFunc_id [in mathcomp.solvable.gfunctor]
GLgroup [in mathcomp.algebra.matrix]
GLgroup_group [in mathcomp.algebra.matrix]
GLrepr [in mathcomp.character.mxabelem]
GLtype [in mathcomp.algebra.matrix]
GLval [in mathcomp.algebra.matrix]
gnorm [in mathcomp.fingroup.fingroup]
grel [in mathcomp.ssreflect.fingraph]
grepr0 [in mathcomp.character.character]
gring_irr_mode_unlockable [in mathcomp.character.integral_char]
gring_class_sum [in mathcomp.character.integral_char]
gring_classM_coef [in mathcomp.character.integral_char]
gring_classM_coef_set [in mathcomp.character.integral_char]
gring_op_linear [in mathcomp.character.mxrepresentation]
gring_op [in mathcomp.character.mxrepresentation]
gring_mx_linear [in mathcomp.character.mxrepresentation]
gring_mx [in mathcomp.character.mxrepresentation]
gring_proj_linear [in mathcomp.character.mxrepresentation]
gring_proj [in mathcomp.character.mxrepresentation]
gring_row_linear [in mathcomp.character.mxrepresentation]
gring_row [in mathcomp.character.mxrepresentation]
gring_index [in mathcomp.character.mxrepresentation]
GRing.additive [in mathcomp.algebra.ssralg]
GRing.AdditiveExports.Additive.apply [in mathcomp.algebra.ssralg]
GRing.AdditiveExports.Additive.map [in mathcomp.algebra.ssralg]
GRing.addr_closed [in mathcomp.algebra.ssralg]
GRing.add_fun [in mathcomp.algebra.ssralg]
GRing.and_dnf [in mathcomp.algebra.ssralg]
GRing.Builders_644.unitringU [in mathcomp.algebra.ssralg]
GRing.Builders_585.lmodU [in mathcomp.algebra.ssralg]
GRing.Builders_544.ringU [in mathcomp.algebra.ssralg]
GRing.Builders_520.zmodU [in mathcomp.algebra.ssralg]
GRing.Builders_188.mulrDr [in mathcomp.algebra.ssralg]
GRing.Builders_188.mulr1 [in mathcomp.algebra.ssralg]
GRing.char [in mathcomp.algebra.ssralg]
GRing.closed_field_axiom [in mathcomp.algebra.ssralg]
GRing.comm [in mathcomp.algebra.ssralg]
GRing.converse [in mathcomp.algebra.ssralg]
GRing.decidable_field_axiom [in mathcomp.algebra.ssralg]
GRing.divalg_closed [in mathcomp.algebra.ssralg]
GRing.divfK [in mathcomp.algebra.ssralg]
GRing.divring_closed [in mathcomp.algebra.ssralg]
GRing.divrK [in mathcomp.algebra.ssralg]
GRing.divr_closed [in mathcomp.algebra.ssralg]
GRing.divr_2closed [in mathcomp.algebra.ssralg]
GRing.dnf_rterm [in mathcomp.algebra.ssralg]
GRing.dnf_to_form [in mathcomp.algebra.ssralg]
GRing.eq0_rform [in mathcomp.algebra.ssralg]
GRing.eval [in mathcomp.algebra.ssralg]
GRing.exp [in mathcomp.algebra.ssralg]
GRing.field_axiom [in mathcomp.algebra.ssralg]
GRing.Frobenius_aut [in mathcomp.algebra.ssralg]
GRing.fsubst [in mathcomp.algebra.ssralg]
GRing.holds [in mathcomp.algebra.ssralg]
GRing.If [in mathcomp.algebra.ssralg]
GRing.integral_domain_axiom [in mathcomp.algebra.ssralg]
GRing.invr_closed [in mathcomp.algebra.ssralg]
GRing.in_alg_head [in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.apply [in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.map [in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.map_at [in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.map_class [in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.unify_map_at [in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.wrap [in mathcomp.algebra.ssralg]
GRing.linear_for [in mathcomp.algebra.ssralg]
GRing.linear_closed [in mathcomp.algebra.ssralg]
GRing.lreg [in mathcomp.algebra.ssralg]
GRing.LRMorphismExports.LRMorphism.apply [in mathcomp.algebra.ssralg]
GRing.LRMorphismExports.LRMorphism.map [in mathcomp.algebra.ssralg]
GRing.mulfV [in mathcomp.algebra.ssralg]
GRing.mull_fun [in mathcomp.algebra.ssralg]
GRing.mulrV [in mathcomp.algebra.ssralg]
GRing.mulr_fun [in mathcomp.algebra.ssralg]
GRing.mulr_closed [in mathcomp.algebra.ssralg]
GRing.mulr_2closed [in mathcomp.algebra.ssralg]
GRing.multiplicative [in mathcomp.algebra.ssralg]
GRing.mul_fun [in mathcomp.algebra.ssralg]
GRing.natmul [in mathcomp.algebra.ssralg]
GRing.natr_sum [in mathcomp.algebra.ssralg]
GRing.null_fun_head [in mathcomp.algebra.ssralg]
GRing.oppr_closed [in mathcomp.algebra.ssralg]
GRing.opp_fun [in mathcomp.algebra.ssralg]
GRing.Pick [in mathcomp.algebra.ssralg]
GRing.proj_sat [in mathcomp.algebra.ssralg]
GRing.qf_to_dnf [in mathcomp.algebra.ssralg]
GRing.qf_eval [in mathcomp.algebra.ssralg]
GRing.qf_form [in mathcomp.algebra.ssralg]
GRing.quantifier_elim [in mathcomp.algebra.ssralg]
GRing.regular [in mathcomp.algebra.ssralg]
GRing.rformula [in mathcomp.algebra.ssralg]
GRing.RMorphismExports.RMorphism.apply [in mathcomp.algebra.ssralg]
GRing.RMorphismExports.RMorphism.map [in mathcomp.algebra.ssralg]
GRing.rreg [in mathcomp.algebra.ssralg]
GRing.rterm [in mathcomp.algebra.ssralg]
GRing.same_env [in mathcomp.algebra.ssralg]
GRing.scalable_for [in mathcomp.algebra.ssralg]
GRing.scaler_closed [in mathcomp.algebra.ssralg]
GRing.scale_fun [in mathcomp.algebra.ssralg]
GRing.Scale.law [in mathcomp.algebra.ssralg]
GRing.sdivr_closed [in mathcomp.algebra.ssralg]
GRing.semiring_closed [in mathcomp.algebra.ssralg]
GRing.smulr_closed [in mathcomp.algebra.ssralg]
GRing.sol [in mathcomp.algebra.ssralg]
GRing.subalg_closed [in mathcomp.algebra.ssralg]
GRing.submod_closed [in mathcomp.algebra.ssralg]
GRing.subring_closed [in mathcomp.algebra.ssralg]
GRing.subrK [in mathcomp.algebra.ssralg]
GRing.subrr [in mathcomp.algebra.ssralg]
GRing.subr_2closed [in mathcomp.algebra.ssralg]
GRing.sub_fun [in mathcomp.algebra.ssralg]
GRing.Theory.addf_div [in mathcomp.algebra.ssralg]
GRing.Theory.addIr [in mathcomp.algebra.ssralg]
GRing.Theory.additive [in mathcomp.algebra.ssralg]
GRing.Theory.additive_linear [in mathcomp.algebra.ssralg]
GRing.Theory.addKr [in mathcomp.algebra.ssralg]
GRing.Theory.addKr_char2 [in mathcomp.algebra.ssralg]
GRing.Theory.addNKr [in mathcomp.algebra.ssralg]
GRing.Theory.addNr [in mathcomp.algebra.ssralg]
GRing.Theory.addrA [in mathcomp.algebra.ssralg]
GRing.Theory.addrAC [in mathcomp.algebra.ssralg]
GRing.Theory.addrACA [in mathcomp.algebra.ssralg]
GRing.Theory.addrC [in mathcomp.algebra.ssralg]
GRing.Theory.addrCA [in mathcomp.algebra.ssralg]
GRing.Theory.addrI [in mathcomp.algebra.ssralg]
GRing.Theory.addrK [in mathcomp.algebra.ssralg]
GRing.Theory.addrKA [in mathcomp.algebra.ssralg]
GRing.Theory.addrK_char2 [in mathcomp.algebra.ssralg]
GRing.Theory.addrN [in mathcomp.algebra.ssralg]
GRing.Theory.addrNK [in mathcomp.algebra.ssralg]
GRing.Theory.addrr_char2 [in mathcomp.algebra.ssralg]
GRing.Theory.addr_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.addr0 [in mathcomp.algebra.ssralg]
GRing.Theory.addr0_eq [in mathcomp.algebra.ssralg]
GRing.Theory.add0r [in mathcomp.algebra.ssralg]
GRing.Theory.bin_lt_charf_0 [in mathcomp.algebra.ssralg]
GRing.Theory.can2_linear [in mathcomp.algebra.ssralg]
GRing.Theory.can2_scalable [in mathcomp.algebra.ssralg]
GRing.Theory.can2_rmorphism [in mathcomp.algebra.ssralg]
GRing.Theory.can2_additive [in mathcomp.algebra.ssralg]
GRing.Theory.charf_eq [in mathcomp.algebra.ssralg]
GRing.Theory.charf_prime [in mathcomp.algebra.ssralg]
GRing.Theory.charf'_nat [in mathcomp.algebra.ssralg]
GRing.Theory.charf0 [in mathcomp.algebra.ssralg]
GRing.Theory.charf0P [in mathcomp.algebra.ssralg]
GRing.Theory.char_lalg [in mathcomp.algebra.ssralg]
GRing.Theory.char0_natf_div [in mathcomp.algebra.ssralg]
GRing.Theory.commrB [in mathcomp.algebra.ssralg]
GRing.Theory.commrD [in mathcomp.algebra.ssralg]
GRing.Theory.commrM [in mathcomp.algebra.ssralg]
GRing.Theory.commrMn [in mathcomp.algebra.ssralg]
GRing.Theory.commrN [in mathcomp.algebra.ssralg]
GRing.Theory.commrN1 [in mathcomp.algebra.ssralg]
GRing.Theory.commrV [in mathcomp.algebra.ssralg]
GRing.Theory.commrX [in mathcomp.algebra.ssralg]
GRing.Theory.commr_sign [in mathcomp.algebra.ssralg]
GRing.Theory.commr_nat [in mathcomp.algebra.ssralg]
GRing.Theory.commr_prod [in mathcomp.algebra.ssralg]
GRing.Theory.commr_sum [in mathcomp.algebra.ssralg]
GRing.Theory.commr_refl [in mathcomp.algebra.ssralg]
GRing.Theory.commr_sym [in mathcomp.algebra.ssralg]
GRing.Theory.commr0 [in mathcomp.algebra.ssralg]
GRing.Theory.commr1 [in mathcomp.algebra.ssralg]
GRing.Theory.comm_alg [in mathcomp.algebra.ssralg]
GRing.Theory.divff [in mathcomp.algebra.ssralg]
GRing.Theory.divfI [in mathcomp.algebra.ssralg]
GRing.Theory.divfK [in mathcomp.algebra.ssralg]
GRing.Theory.divIf [in mathcomp.algebra.ssralg]
GRing.Theory.divIr [in mathcomp.algebra.ssralg]
GRing.Theory.divKf [in mathcomp.algebra.ssralg]
GRing.Theory.divKr [in mathcomp.algebra.ssralg]
GRing.Theory.divrI [in mathcomp.algebra.ssralg]
GRing.Theory.divringClosedP [in mathcomp.algebra.ssralg]
GRing.Theory.divrK [in mathcomp.algebra.ssralg]
GRing.Theory.divrr [in mathcomp.algebra.ssralg]
GRing.Theory.divr_signM [in mathcomp.algebra.ssralg]
GRing.Theory.divr1 [in mathcomp.algebra.ssralg]
GRing.Theory.divr1_eq [in mathcomp.algebra.ssralg]
GRing.Theory.div1r [in mathcomp.algebra.ssralg]
GRing.Theory.dvdn_charf [in mathcomp.algebra.ssralg]
GRing.Theory.eqf_sqr [in mathcomp.algebra.ssralg]
GRing.Theory.eqr_sum_div [in mathcomp.algebra.ssralg]
GRing.Theory.eqr_div [in mathcomp.algebra.ssralg]
GRing.Theory.eqr_oppLR [in mathcomp.algebra.ssralg]
GRing.Theory.eqr_opp [in mathcomp.algebra.ssralg]
GRing.Theory.eq_sol [in mathcomp.algebra.ssralg]
GRing.Theory.eq_sat [in mathcomp.algebra.ssralg]
GRing.Theory.eq_holds [in mathcomp.algebra.ssralg]
GRing.Theory.eq_eval [in mathcomp.algebra.ssralg]
GRing.Theory.eval_tsubst [in mathcomp.algebra.ssralg]
GRing.Theory.expfB [in mathcomp.algebra.ssralg]
GRing.Theory.expfB_cond [in mathcomp.algebra.ssralg]
GRing.Theory.expfS_eq1 [in mathcomp.algebra.ssralg]
GRing.Theory.expf_neq0 [in mathcomp.algebra.ssralg]
GRing.Theory.expf_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.exprAC [in mathcomp.algebra.ssralg]
GRing.Theory.exprB [in mathcomp.algebra.ssralg]
GRing.Theory.exprBn [in mathcomp.algebra.ssralg]
GRing.Theory.exprBn_comm [in mathcomp.algebra.ssralg]
GRing.Theory.exprD [in mathcomp.algebra.ssralg]
GRing.Theory.exprDn [in mathcomp.algebra.ssralg]
GRing.Theory.exprDn_char [in mathcomp.algebra.ssralg]
GRing.Theory.exprDn_comm [in mathcomp.algebra.ssralg]
GRing.Theory.exprD1n [in mathcomp.algebra.ssralg]
GRing.Theory.exprM [in mathcomp.algebra.ssralg]
GRing.Theory.exprMn [in mathcomp.algebra.ssralg]
GRing.Theory.exprMn_n [in mathcomp.algebra.ssralg]
GRing.Theory.exprMn_comm [in mathcomp.algebra.ssralg]
GRing.Theory.exprNn [in mathcomp.algebra.ssralg]
GRing.Theory.exprNn_char [in mathcomp.algebra.ssralg]
GRing.Theory.exprS [in mathcomp.algebra.ssralg]
GRing.Theory.exprSr [in mathcomp.algebra.ssralg]
GRing.Theory.exprVn [in mathcomp.algebra.ssralg]
GRing.Theory.exprZn [in mathcomp.algebra.ssralg]
GRing.Theory.expr_div_n [in mathcomp.algebra.ssralg]
GRing.Theory.expr_dvd [in mathcomp.algebra.ssralg]
GRing.Theory.expr_mod [in mathcomp.algebra.ssralg]
GRing.Theory.expr_sum [in mathcomp.algebra.ssralg]
GRing.Theory.expr0 [in mathcomp.algebra.ssralg]
GRing.Theory.expr0n [in mathcomp.algebra.ssralg]
GRing.Theory.expr1 [in mathcomp.algebra.ssralg]
GRing.Theory.expr1n [in mathcomp.algebra.ssralg]
GRing.Theory.expr2 [in mathcomp.algebra.ssralg]
GRing.Theory.fieldP [in mathcomp.algebra.ssralg]
GRing.Theory.fmorphV [in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_div [in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_unit [in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_char [in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_eq1 [in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_eq [in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_inj [in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.fpredMl [in mathcomp.algebra.ssralg]
GRing.Theory.fpredMr [in mathcomp.algebra.ssralg]
GRing.Theory.fpred_divl [in mathcomp.algebra.ssralg]
GRing.Theory.fpred_divr [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autB_comm [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autN [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autX [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autM_comm [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_aut_nat [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autMn [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autD_comm [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_aut1 [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_aut0 [in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autE [in mathcomp.algebra.ssralg]
GRing.Theory.holds_fsubst [in mathcomp.algebra.ssralg]
GRing.Theory.imaginary_exists [in mathcomp.algebra.ssralg]
GRing.Theory.invfM [in mathcomp.algebra.ssralg]
GRing.Theory.invf_div [in mathcomp.algebra.ssralg]
GRing.Theory.invrK [in mathcomp.algebra.ssralg]
GRing.Theory.invrM [in mathcomp.algebra.ssralg]
GRing.Theory.invrN [in mathcomp.algebra.ssralg]
GRing.Theory.invrN1 [in mathcomp.algebra.ssralg]
GRing.Theory.invrZ [in mathcomp.algebra.ssralg]
GRing.Theory.invr_signM [in mathcomp.algebra.ssralg]
GRing.Theory.invr_neq0 [in mathcomp.algebra.ssralg]
GRing.Theory.invr_eq1 [in mathcomp.algebra.ssralg]
GRing.Theory.invr_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.invr_sign [in mathcomp.algebra.ssralg]
GRing.Theory.invr_inj [in mathcomp.algebra.ssralg]
GRing.Theory.invr_out [in mathcomp.algebra.ssralg]
GRing.Theory.invr0 [in mathcomp.algebra.ssralg]
GRing.Theory.invr1 [in mathcomp.algebra.ssralg]
GRing.Theory.in_algE [in mathcomp.algebra.ssralg]
GRing.Theory.iter_mulr_1 [in mathcomp.algebra.ssralg]
GRing.Theory.iter_mulr [in mathcomp.algebra.ssralg]
GRing.Theory.iter_addr_0 [in mathcomp.algebra.ssralg]
GRing.Theory.iter_addr [in mathcomp.algebra.ssralg]
GRing.Theory.linearB [in mathcomp.algebra.ssralg]
GRing.Theory.linearD [in mathcomp.algebra.ssralg]
GRing.Theory.linearE [in mathcomp.algebra.ssralg]
GRing.Theory.linearMn [in mathcomp.algebra.ssralg]
GRing.Theory.linearMNn [in mathcomp.algebra.ssralg]
GRing.Theory.linearN [in mathcomp.algebra.ssralg]
GRing.Theory.linearP [in mathcomp.algebra.ssralg]
GRing.Theory.linearPZ [in mathcomp.algebra.ssralg]
GRing.Theory.linearZ [in mathcomp.algebra.ssralg]
GRing.Theory.linearZZ [in mathcomp.algebra.ssralg]
GRing.Theory.linearZ_LR [in mathcomp.algebra.ssralg]
GRing.Theory.linear_sum [in mathcomp.algebra.ssralg]
GRing.Theory.linear_for [in mathcomp.algebra.ssralg]
GRing.Theory.linear0 [in mathcomp.algebra.ssralg]
GRing.Theory.lregM [in mathcomp.algebra.ssralg]
GRing.Theory.lregN [in mathcomp.algebra.ssralg]
GRing.Theory.lregP [in mathcomp.algebra.ssralg]
GRing.Theory.lregX [in mathcomp.algebra.ssralg]
GRing.Theory.lreg_sign [in mathcomp.algebra.ssralg]
GRing.Theory.lreg_neq0 [in mathcomp.algebra.ssralg]
GRing.Theory.lreg1 [in mathcomp.algebra.ssralg]
GRing.Theory.mulfI [in mathcomp.algebra.ssralg]
GRing.Theory.mulfK [in mathcomp.algebra.ssralg]
GRing.Theory.mulfV [in mathcomp.algebra.ssralg]
GRing.Theory.mulfVK [in mathcomp.algebra.ssralg]
GRing.Theory.mulf_div [in mathcomp.algebra.ssralg]
GRing.Theory.mulf_neq0 [in mathcomp.algebra.ssralg]
GRing.Theory.mulf_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.mulIf [in mathcomp.algebra.ssralg]
GRing.Theory.mulIr [in mathcomp.algebra.ssralg]
GRing.Theory.mulIr_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.mulIr0_rreg [in mathcomp.algebra.ssralg]
GRing.Theory.mulKf [in mathcomp.algebra.ssralg]
GRing.Theory.mulKr [in mathcomp.algebra.ssralg]
GRing.Theory.mulNr [in mathcomp.algebra.ssralg]
GRing.Theory.mulNrn [in mathcomp.algebra.ssralg]
GRing.Theory.mulN1r [in mathcomp.algebra.ssralg]
GRing.Theory.mulrA [in mathcomp.algebra.ssralg]
GRing.Theory.mulrAC [in mathcomp.algebra.ssralg]
GRing.Theory.mulrACA [in mathcomp.algebra.ssralg]
GRing.Theory.mulrb [in mathcomp.algebra.ssralg]
GRing.Theory.mulrBl [in mathcomp.algebra.ssralg]
GRing.Theory.mulrBr [in mathcomp.algebra.ssralg]
GRing.Theory.mulrC [in mathcomp.algebra.ssralg]
GRing.Theory.mulrCA [in mathcomp.algebra.ssralg]
GRing.Theory.mulrDl [in mathcomp.algebra.ssralg]
GRing.Theory.mulrDr [in mathcomp.algebra.ssralg]
GRing.Theory.mulrI [in mathcomp.algebra.ssralg]
GRing.Theory.mulrI_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.mulrI0_lreg [in mathcomp.algebra.ssralg]
GRing.Theory.mulrK [in mathcomp.algebra.ssralg]
GRing.Theory.mulrN [in mathcomp.algebra.ssralg]
GRing.Theory.mulrnA [in mathcomp.algebra.ssralg]
GRing.Theory.mulrnAC [in mathcomp.algebra.ssralg]
GRing.Theory.mulrnAl [in mathcomp.algebra.ssralg]
GRing.Theory.mulrnAr [in mathcomp.algebra.ssralg]
GRing.Theory.mulrnBl [in mathcomp.algebra.ssralg]
GRing.Theory.mulrnBr [in mathcomp.algebra.ssralg]
GRing.Theory.mulrnDl [in mathcomp.algebra.ssralg]
GRing.Theory.mulrnDr [in mathcomp.algebra.ssralg]
GRing.Theory.mulrNN [in mathcomp.algebra.ssralg]
GRing.Theory.mulrn_char [in mathcomp.algebra.ssralg]
GRing.Theory.mulrN1 [in mathcomp.algebra.ssralg]
GRing.Theory.mulrS [in mathcomp.algebra.ssralg]
GRing.Theory.mulrSr [in mathcomp.algebra.ssralg]
GRing.Theory.mulrV [in mathcomp.algebra.ssralg]
GRing.Theory.mulrVK [in mathcomp.algebra.ssralg]
GRing.Theory.mulr_algr [in mathcomp.algebra.ssralg]
GRing.Theory.mulr_algl [in mathcomp.algebra.ssralg]
GRing.Theory.mulr_signM [in mathcomp.algebra.ssralg]
GRing.Theory.mulr_sign [in mathcomp.algebra.ssralg]
GRing.Theory.mulr_natr [in mathcomp.algebra.ssralg]
GRing.Theory.mulr_natl [in mathcomp.algebra.ssralg]
GRing.Theory.mulr_sumr [in mathcomp.algebra.ssralg]
GRing.Theory.mulr_suml [in mathcomp.algebra.ssralg]
GRing.Theory.mulr0 [in mathcomp.algebra.ssralg]
GRing.Theory.mulr0n [in mathcomp.algebra.ssralg]
GRing.Theory.mulr1 [in mathcomp.algebra.ssralg]
GRing.Theory.mulr1n [in mathcomp.algebra.ssralg]
GRing.Theory.mulr1_eq [in mathcomp.algebra.ssralg]
GRing.Theory.mulr2n [in mathcomp.algebra.ssralg]
GRing.Theory.multiplicative [in mathcomp.algebra.ssralg]
GRing.Theory.mulVf [in mathcomp.algebra.ssralg]
GRing.Theory.mulVKf [in mathcomp.algebra.ssralg]
GRing.Theory.mulVKr [in mathcomp.algebra.ssralg]
GRing.Theory.mulVr [in mathcomp.algebra.ssralg]
GRing.Theory.mul0r [in mathcomp.algebra.ssralg]
GRing.Theory.mul0rn [in mathcomp.algebra.ssralg]
GRing.Theory.mul1r [in mathcomp.algebra.ssralg]
GRing.Theory.natf_neq0 [in mathcomp.algebra.ssralg]
GRing.Theory.natf0_char [in mathcomp.algebra.ssralg]
GRing.Theory.natrB [in mathcomp.algebra.ssralg]
GRing.Theory.natrD [in mathcomp.algebra.ssralg]
GRing.Theory.natrM [in mathcomp.algebra.ssralg]
GRing.Theory.natrX [in mathcomp.algebra.ssralg]
GRing.Theory.natr_div [in mathcomp.algebra.ssralg]
GRing.Theory.natr_prod [in mathcomp.algebra.ssralg]
GRing.Theory.natr_sum [in mathcomp.algebra.ssralg]
GRing.Theory.natr1 [in mathcomp.algebra.ssralg]
GRing.Theory.nat1r [in mathcomp.algebra.ssralg]
GRing.Theory.oner_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.oner_neq0 [in mathcomp.algebra.ssralg]
GRing.Theory.opprB [in mathcomp.algebra.ssralg]
GRing.Theory.opprD [in mathcomp.algebra.ssralg]
GRing.Theory.opprK [in mathcomp.algebra.ssralg]
GRing.Theory.oppr_char2 [in mathcomp.algebra.ssralg]
GRing.Theory.oppr_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.oppr_inj [in mathcomp.algebra.ssralg]
GRing.Theory.oppr0 [in mathcomp.algebra.ssralg]
GRing.Theory.prodfV [in mathcomp.algebra.ssralg]
GRing.Theory.prodf_div [in mathcomp.algebra.ssralg]
GRing.Theory.prodf_seq_neq0 [in mathcomp.algebra.ssralg]
GRing.Theory.prodf_neq0 [in mathcomp.algebra.ssralg]
GRing.Theory.prodf_seq_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.prodf_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.prodrMn [in mathcomp.algebra.ssralg]
GRing.Theory.prodrMn_const [in mathcomp.algebra.ssralg]
GRing.Theory.prodrN [in mathcomp.algebra.ssralg]
GRing.Theory.prodrXl [in mathcomp.algebra.ssralg]
GRing.Theory.prodrXr [in mathcomp.algebra.ssralg]
GRing.Theory.prodr_undup_exp_count [in mathcomp.algebra.ssralg]
GRing.Theory.prodr_const_nat [in mathcomp.algebra.ssralg]
GRing.Theory.prodr_const [in mathcomp.algebra.ssralg]
GRing.Theory.raddf [in mathcomp.algebra.ssralg]
GRing.Theory.raddfB [in mathcomp.algebra.ssralg]
GRing.Theory.raddfD [in mathcomp.algebra.ssralg]
GRing.Theory.raddfMn [in mathcomp.algebra.ssralg]
GRing.Theory.raddfMnat [in mathcomp.algebra.ssralg]
GRing.Theory.raddfMNn [in mathcomp.algebra.ssralg]
GRing.Theory.raddfMsign [in mathcomp.algebra.ssralg]
GRing.Theory.raddfN [in mathcomp.algebra.ssralg]
GRing.Theory.raddfZnat [in mathcomp.algebra.ssralg]
GRing.Theory.raddfZsign [in mathcomp.algebra.ssralg]
GRing.Theory.raddf_sum [in mathcomp.algebra.ssralg]
GRing.Theory.raddf_inj [in mathcomp.algebra.ssralg]
GRing.Theory.raddf_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.raddf0 [in mathcomp.algebra.ssralg]
GRing.Theory.revrX [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphB [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphD [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphE [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphismMP [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphM [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphMn [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphMNn [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphMsign [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphN [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphN1 [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphV [in mathcomp.algebra.ssralg]
GRing.Theory.rmorphX [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_alg [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_div [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_unit [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_comm [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_char [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_sign [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_prod [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_eq_nat [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_nat [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_eq1 [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_sum [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph0 [in mathcomp.algebra.ssralg]
GRing.Theory.rmorph1 [in mathcomp.algebra.ssralg]
GRing.Theory.rpredB [in mathcomp.algebra.ssralg]
GRing.Theory.rpredBC [in mathcomp.algebra.ssralg]
GRing.Theory.rpredBl [in mathcomp.algebra.ssralg]
GRing.Theory.rpredBr [in mathcomp.algebra.ssralg]
GRing.Theory.rpredD [in mathcomp.algebra.ssralg]
GRing.Theory.rpredDl [in mathcomp.algebra.ssralg]
GRing.Theory.rpredDr [in mathcomp.algebra.ssralg]
GRing.Theory.rpredM [in mathcomp.algebra.ssralg]
GRing.Theory.rpredMl [in mathcomp.algebra.ssralg]
GRing.Theory.rpredMn [in mathcomp.algebra.ssralg]
GRing.Theory.rpredMNn [in mathcomp.algebra.ssralg]
GRing.Theory.rpredMr [in mathcomp.algebra.ssralg]
GRing.Theory.rpredMsign [in mathcomp.algebra.ssralg]
GRing.Theory.rpredN [in mathcomp.algebra.ssralg]
GRing.Theory.rpredNr [in mathcomp.algebra.ssralg]
GRing.Theory.rpredN1 [in mathcomp.algebra.ssralg]
GRing.Theory.rpredV [in mathcomp.algebra.ssralg]
GRing.Theory.rpredVr [in mathcomp.algebra.ssralg]
GRing.Theory.rpredX [in mathcomp.algebra.ssralg]
GRing.Theory.rpredXN [in mathcomp.algebra.ssralg]
GRing.Theory.rpredZ [in mathcomp.algebra.ssralg]
GRing.Theory.rpredZeq [in mathcomp.algebra.ssralg]
GRing.Theory.rpredZnat [in mathcomp.algebra.ssralg]
GRing.Theory.rpredZsign [in mathcomp.algebra.ssralg]
GRing.Theory.rpred_divl [in mathcomp.algebra.ssralg]
GRing.Theory.rpred_divr [in mathcomp.algebra.ssralg]
GRing.Theory.rpred_div [in mathcomp.algebra.ssralg]
GRing.Theory.rpred_sign [in mathcomp.algebra.ssralg]
GRing.Theory.rpred_nat [in mathcomp.algebra.ssralg]
GRing.Theory.rpred_prod [in mathcomp.algebra.ssralg]
GRing.Theory.rpred_sum [in mathcomp.algebra.ssralg]
GRing.Theory.rpred0 [in mathcomp.algebra.ssralg]
GRing.Theory.rpred0D [in mathcomp.algebra.ssralg]
GRing.Theory.rpred1 [in mathcomp.algebra.ssralg]
GRing.Theory.rpred1M [in mathcomp.algebra.ssralg]
GRing.Theory.rregM [in mathcomp.algebra.ssralg]
GRing.Theory.rregN [in mathcomp.algebra.ssralg]
GRing.Theory.rregP [in mathcomp.algebra.ssralg]
GRing.Theory.rregX [in mathcomp.algebra.ssralg]
GRing.Theory.rreg_neq0 [in mathcomp.algebra.ssralg]
GRing.Theory.rreg1 [in mathcomp.algebra.ssralg]
GRing.Theory.satP [in mathcomp.algebra.ssralg]
GRing.Theory.scalable_linear [in mathcomp.algebra.ssralg]
GRing.Theory.scalable_for [in mathcomp.algebra.ssralg]
GRing.Theory.scalarP [in mathcomp.algebra.ssralg]
GRing.Theory.scalarZ [in mathcomp.algebra.ssralg]
GRing.Theory.scaleNr [in mathcomp.algebra.ssralg]
GRing.Theory.scaleN1r [in mathcomp.algebra.ssralg]
GRing.Theory.scalerA [in mathcomp.algebra.ssralg]
GRing.Theory.scalerAl [in mathcomp.algebra.ssralg]
GRing.Theory.scalerAr [in mathcomp.algebra.ssralg]
GRing.Theory.scalerBl [in mathcomp.algebra.ssralg]
GRing.Theory.scalerBr [in mathcomp.algebra.ssralg]
GRing.Theory.scalerCA [in mathcomp.algebra.ssralg]
GRing.Theory.scalerDl [in mathcomp.algebra.ssralg]
GRing.Theory.scalerDr [in mathcomp.algebra.ssralg]
GRing.Theory.scalerI [in mathcomp.algebra.ssralg]
GRing.Theory.scalerK [in mathcomp.algebra.ssralg]
GRing.Theory.scalerKV [in mathcomp.algebra.ssralg]
GRing.Theory.scalerMnl [in mathcomp.algebra.ssralg]
GRing.Theory.scalerMnr [in mathcomp.algebra.ssralg]
GRing.Theory.scalerN [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_unit [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_injl [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_prod [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_prodr [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_prodl [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_sign [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_sumr [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_suml [in mathcomp.algebra.ssralg]
GRing.Theory.scaler_nat [in mathcomp.algebra.ssralg]
GRing.Theory.scaler0 [in mathcomp.algebra.ssralg]
GRing.Theory.scale0r [in mathcomp.algebra.ssralg]
GRing.Theory.scale1r [in mathcomp.algebra.ssralg]
GRing.Theory.signrE [in mathcomp.algebra.ssralg]
GRing.Theory.signrMK [in mathcomp.algebra.ssralg]
GRing.Theory.signrN [in mathcomp.algebra.ssralg]
GRing.Theory.signrZK [in mathcomp.algebra.ssralg]
GRing.Theory.signr_addb [in mathcomp.algebra.ssralg]
GRing.Theory.signr_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.signr_odd [in mathcomp.algebra.ssralg]
GRing.Theory.size_sol [in mathcomp.algebra.ssralg]
GRing.Theory.solP [in mathcomp.algebra.ssralg]
GRing.Theory.solve_monicpoly [in mathcomp.algebra.ssralg]
GRing.Theory.sqrf_eq1 [in mathcomp.algebra.ssralg]
GRing.Theory.sqrf_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.sqrrB [in mathcomp.algebra.ssralg]
GRing.Theory.sqrrB1 [in mathcomp.algebra.ssralg]
GRing.Theory.sqrrD [in mathcomp.algebra.ssralg]
GRing.Theory.sqrrD1 [in mathcomp.algebra.ssralg]
GRing.Theory.sqrrN [in mathcomp.algebra.ssralg]
GRing.Theory.sqrr_sign [in mathcomp.algebra.ssralg]
GRing.Theory.subalgClosedP [in mathcomp.algebra.ssralg]
GRing.Theory.subIr [in mathcomp.algebra.ssralg]
GRing.Theory.subKr [in mathcomp.algebra.ssralg]
GRing.Theory.submodClosedP [in mathcomp.algebra.ssralg]
GRing.Theory.subrI [in mathcomp.algebra.ssralg]
GRing.Theory.subringClosedP [in mathcomp.algebra.ssralg]
GRing.Theory.subrK [in mathcomp.algebra.ssralg]
GRing.Theory.subrKA [in mathcomp.algebra.ssralg]
GRing.Theory.subrr [in mathcomp.algebra.ssralg]
GRing.Theory.subrXX [in mathcomp.algebra.ssralg]
GRing.Theory.subrXX_comm [in mathcomp.algebra.ssralg]
GRing.Theory.subrX1 [in mathcomp.algebra.ssralg]
GRing.Theory.subr_sqrDB [in mathcomp.algebra.ssralg]
GRing.Theory.subr_sqr [in mathcomp.algebra.ssralg]
GRing.Theory.subr_sqr_1 [in mathcomp.algebra.ssralg]
GRing.Theory.subr_eq0 [in mathcomp.algebra.ssralg]
GRing.Theory.subr_eq [in mathcomp.algebra.ssralg]
GRing.Theory.subr0 [in mathcomp.algebra.ssralg]
GRing.Theory.subr0_eq [in mathcomp.algebra.ssralg]
GRing.Theory.sub0r [in mathcomp.algebra.ssralg]
GRing.Theory.sumrB [in mathcomp.algebra.ssralg]
GRing.Theory.sumrMnl [in mathcomp.algebra.ssralg]
GRing.Theory.sumrMnr [in mathcomp.algebra.ssralg]
GRing.Theory.sumrN [in mathcomp.algebra.ssralg]
GRing.Theory.sumr_const_nat [in mathcomp.algebra.ssralg]
GRing.Theory.sumr_const [in mathcomp.algebra.ssralg]
GRing.Theory.telescope_prodf [in mathcomp.algebra.ssralg]
GRing.Theory.telescope_prodr [in mathcomp.algebra.ssralg]
GRing.Theory.telescope_sumr [in mathcomp.algebra.ssralg]
GRing.Theory.unitfE [in mathcomp.algebra.ssralg]
GRing.Theory.unitrE [in mathcomp.algebra.ssralg]
GRing.Theory.unitrM [in mathcomp.algebra.ssralg]
GRing.Theory.unitrMl [in mathcomp.algebra.ssralg]
GRing.Theory.unitrMr [in mathcomp.algebra.ssralg]
GRing.Theory.unitrM_comm [in mathcomp.algebra.ssralg]
GRing.Theory.unitrN [in mathcomp.algebra.ssralg]
GRing.Theory.unitrN1 [in mathcomp.algebra.ssralg]
GRing.Theory.unitrP [in mathcomp.algebra.ssralg]
GRing.Theory.unitrPr [in mathcomp.algebra.ssralg]
GRing.Theory.unitrV [in mathcomp.algebra.ssralg]
GRing.Theory.unitrX [in mathcomp.algebra.ssralg]
GRing.Theory.unitrX_pos [in mathcomp.algebra.ssralg]
GRing.Theory.unitr0 [in mathcomp.algebra.ssralg]
GRing.Theory.unitr1 [in mathcomp.algebra.ssralg]
GRing.Theory.zmodClosedP [in mathcomp.algebra.ssralg]
GRing.to_rform [in mathcomp.algebra.ssralg]
GRing.to_rterm [in mathcomp.algebra.ssralg]
GRing.tsubst [in mathcomp.algebra.ssralg]
GRing.ub_var [in mathcomp.algebra.ssralg]
GRing.unit [in mathcomp.algebra.ssralg]
GRing.unit_pred [in mathcomp.algebra.ssralg]
GRing.valid_QE_proj [in mathcomp.algebra.ssralg]
GRing.wf_QE_proj [in mathcomp.algebra.ssralg]
GRing.zmod_closed [in mathcomp.algebra.ssralg]
group [in mathcomp.fingroup.fingroup]
GroupSetBaseGroupSig.sort [in mathcomp.fingroup.fingroup]
GroupSet.sort [in mathcomp.fingroup.fingroup]
group_of [in mathcomp.fingroup.fingroup]
group_set [in mathcomp.fingroup.fingroup]
group_closure_field [in mathcomp.character.mxrepresentation]
group_splitting_field [in mathcomp.character.mxrepresentation]
group_ring [in mathcomp.character.mxrepresentation]
group_rel_of [in mathcomp.solvable.gseries]
gset_mx [in mathcomp.character.mxrepresentation]
gsimp [in mathcomp.fingroup.fingroup]
gtn [in mathcomp.ssreflect.ssrnat]
| 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 | (71649 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 | (1792 entries) |
| Binder 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 | (46193 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 | (266 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 | (3623 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 | (91 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 | (14204 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 | (259 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 | (8 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 | (134 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 | (44 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 | (1276 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 | (682 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 | (3041 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 | (36 entries) |