| 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 | (76754 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 | (1892 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 | (49588 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 | (305 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 | (4034 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 | (94 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 | (14802 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 | (222 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 | (9 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 | (131 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 | (43 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 | (1392 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 | (1140 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 | (3066 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) |
S
S [abbreviation, in mathcomp.character.mxrepresentation]sAG:394 [binder, in mathcomp.fingroup.morphism]
sAG:397 [binder, in mathcomp.fingroup.morphism]
same_pblock [lemma, in mathcomp.ssreflect.finset]
same_fconnect1_r [lemma, in mathcomp.ssreflect.fingraph]
same_fconnect1 [lemma, in mathcomp.ssreflect.fingraph]
same_fconnect_finv [lemma, in mathcomp.ssreflect.fingraph]
same_connect_rev [lemma, in mathcomp.ssreflect.fingraph]
same_connect1r [lemma, in mathcomp.ssreflect.fingraph]
same_connect1 [lemma, in mathcomp.ssreflect.fingraph]
same_connect_r [lemma, in mathcomp.ssreflect.fingraph]
same_connect [lemma, in mathcomp.ssreflect.fingraph]
satP:1931 [binder, in mathcomp.algebra.ssralg]
sat:1930 [binder, in mathcomp.algebra.ssralg]
scalar_mx_sum_delta [lemma, in mathcomp.algebra.matrix]
scalar_mxC [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_multiplicative [lemma, in mathcomp.algebra.matrix]
scalar_mxM [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_additive [lemma, in mathcomp.algebra.matrix]
scalar_mx_block [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_trig [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_diag [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_scalar [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_semi_additive [lemma, in mathcomp.algebra.matrix]
scalar_mx [definition, in mathcomp.algebra.matrix]
scalar_mx_key [lemma, in mathcomp.algebra.matrix]
scalar_mx_hom [lemma, in mathcomp.character.mxrepresentation]
scalar_mx_cent [lemma, in mathcomp.algebra.mxalgebra]
ScaleCompLfun [section, in mathcomp.algebra.vector]
ScaleCompLfun.aT [variable, in mathcomp.algebra.vector]
ScaleCompLfun.R [variable, in mathcomp.algebra.vector]
ScaleCompLfun.rT [variable, in mathcomp.algebra.vector]
ScaleCompLfun.vT [variable, in mathcomp.algebra.vector]
scalemx [definition, in mathcomp.algebra.matrix]
scalemxA [lemma, in mathcomp.algebra.matrix]
scalemxAl [lemma, in mathcomp.algebra.matrix]
scalemxAr [lemma, in mathcomp.algebra.matrix]
scalemxDl [lemma, in mathcomp.algebra.matrix]
scalemxDr [lemma, in mathcomp.algebra.matrix]
scalemx_inj [lemma, in mathcomp.algebra.matrix]
scalemx_eq0 [lemma, in mathcomp.algebra.matrix]
scalemx_const [lemma, in mathcomp.algebra.matrix]
scalemx_key [lemma, in mathcomp.algebra.matrix]
scalemx_sub [lemma, in mathcomp.algebra.mxalgebra]
scalemx1 [lemma, in mathcomp.algebra.matrix]
scalerAl:749 [binder, in mathcomp.algebra.ssralg]
scalerAr:1319 [binder, in mathcomp.algebra.ssralg]
scalerA:676 [binder, in mathcomp.algebra.ssralg]
scalerDl:684 [binder, in mathcomp.algebra.ssralg]
scalerDr:678 [binder, in mathcomp.algebra.ssralg]
scalerMzl [lemma, in mathcomp.algebra.ssrint]
scalerMzr [lemma, in mathcomp.algebra.ssrint]
scaler_int [lemma, in mathcomp.algebra.ssrint]
scalezrE [lemma, in mathcomp.algebra.ssrint]
scale_zchar [lemma, in mathcomp.character.vcharacter]
scale_scalar_mx [lemma, in mathcomp.algebra.matrix]
scale_block_mx [lemma, in mathcomp.algebra.matrix]
scale_col_mx [lemma, in mathcomp.algebra.matrix]
scale_row_mx [lemma, in mathcomp.algebra.matrix]
scale_groupAction [definition, in mathcomp.character.mxabelem]
scale_is_groupAction [lemma, in mathcomp.character.mxabelem]
scale_action [definition, in mathcomp.character.mxabelem]
scale_is_action [lemma, in mathcomp.character.mxabelem]
scale_actE [lemma, in mathcomp.character.mxabelem]
scale_act [definition, in mathcomp.character.mxabelem]
scale_pair [definition, in mathcomp.algebra.ssralg]
scale_lfunE [lemma, in mathcomp.algebra.vector]
scale_lfun [definition, in mathcomp.algebra.vector]
scale_poly_eq0 [lemma, in mathcomp.algebra.poly]
scale_polyC [lemma, in mathcomp.algebra.poly]
scale_polyAl [lemma, in mathcomp.algebra.poly]
scale_polyDl [lemma, in mathcomp.algebra.poly]
scale_polyDr [lemma, in mathcomp.algebra.poly]
scale_1poly [lemma, in mathcomp.algebra.poly]
scale_polyA [lemma, in mathcomp.algebra.poly]
scale_polyE [lemma, in mathcomp.algebra.poly]
scale_poly_unlockable [definition, in mathcomp.algebra.poly]
scale_poly [definition, in mathcomp.algebra.poly]
scale_poly_key [lemma, in mathcomp.algebra.poly]
scale_poly_def [definition, in mathcomp.algebra.poly]
scale1mx [lemma, in mathcomp.algebra.matrix]
scale1r:677 [binder, in mathcomp.algebra.ssralg]
scale:672 [binder, in mathcomp.algebra.ssralg]
scalq [definition, in mathcomp.algebra.rat]
scalqE [lemma, in mathcomp.algebra.rat]
scalq_eq0 [lemma, in mathcomp.algebra.rat]
scalq_def [lemma, in mathcomp.algebra.rat]
Scan [section, in mathcomp.ssreflect.seq]
scanl [definition, in mathcomp.ssreflect.seq]
scanlK [lemma, in mathcomp.ssreflect.seq]
scanl_bseq [definition, in mathcomp.ssreflect.tuple]
scanl_bseqP [lemma, in mathcomp.ssreflect.tuple]
scanl_tuple [definition, in mathcomp.ssreflect.tuple]
scanl_tupleP [lemma, in mathcomp.ssreflect.tuple]
scanl_rcons [lemma, in mathcomp.ssreflect.seq]
scanl_cat [lemma, in mathcomp.ssreflect.seq]
Scan.f [variable, in mathcomp.ssreflect.seq]
Scan.g [variable, in mathcomp.ssreflect.seq]
Scan.T1 [variable, in mathcomp.ssreflect.seq]
Scan.T2 [variable, in mathcomp.ssreflect.seq]
Scan.x1 [variable, in mathcomp.ssreflect.seq]
Scan.x2 [variable, in mathcomp.ssreflect.seq]
SchurZassenhaus_trans_actsol [lemma, in mathcomp.solvable.hall]
SchurZassenhaus_trans_sol [lemma, in mathcomp.solvable.hall]
SchurZassenhaus_split [lemma, in mathcomp.solvable.hall]
Schur:2593 [binder, in mathcomp.algebra.matrix]
SCN [section, in mathcomp.solvable.maximal]
SCN [definition, in mathcomp.solvable.maximal]
SCN_max [lemma, in mathcomp.solvable.maximal]
SCN_abelian [lemma, in mathcomp.solvable.maximal]
SCN_P [lemma, in mathcomp.solvable.maximal]
SCN_at [definition, in mathcomp.solvable.maximal]
SCN.G [variable, in mathcomp.solvable.maximal]
SCN.gT [variable, in mathcomp.solvable.maximal]
SCN.p [variable, in mathcomp.solvable.maximal]
SCN.SCNseries [section, in mathcomp.solvable.maximal]
SCN.SCNseries.A [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.cAA [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.nZA [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.SCN_A [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.sZA [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.Z [variable, in mathcomp.solvable.maximal]
sc:100 [binder, in mathcomp.solvable.burnside_app]
sc:101 [binder, in mathcomp.solvable.burnside_app]
sc:102 [binder, in mathcomp.solvable.burnside_app]
sc:104 [binder, in mathcomp.solvable.burnside_app]
sc:11 [binder, in mathcomp.solvable.burnside_app]
sc:12 [binder, in mathcomp.solvable.burnside_app]
sc:13 [binder, in mathcomp.solvable.burnside_app]
sc:139 [binder, in mathcomp.solvable.burnside_app]
sc:146 [binder, in mathcomp.solvable.burnside_app]
sc:147 [binder, in mathcomp.solvable.burnside_app]
sc:148 [binder, in mathcomp.solvable.burnside_app]
sc:149 [binder, in mathcomp.solvable.burnside_app]
sc:150 [binder, in mathcomp.solvable.burnside_app]
sc:151 [binder, in mathcomp.solvable.burnside_app]
sc:20 [binder, in mathcomp.solvable.burnside_app]
sc:21 [binder, in mathcomp.solvable.burnside_app]
sc:22 [binder, in mathcomp.solvable.burnside_app]
sc:23 [binder, in mathcomp.solvable.burnside_app]
sc:26 [binder, in mathcomp.solvable.burnside_app]
sc:33 [binder, in mathcomp.solvable.burnside_app]
sc:40 [binder, in mathcomp.solvable.burnside_app]
sc:41 [binder, in mathcomp.solvable.burnside_app]
sc:42 [binder, in mathcomp.solvable.burnside_app]
sc:43 [binder, in mathcomp.solvable.burnside_app]
sc:80 [binder, in mathcomp.solvable.burnside_app]
sc:81 [binder, in mathcomp.solvable.burnside_app]
sc:82 [binder, in mathcomp.solvable.burnside_app]
sc:83 [binder, in mathcomp.solvable.burnside_app]
sc:84 [binder, in mathcomp.solvable.burnside_app]
sc:85 [binder, in mathcomp.solvable.burnside_app]
sc:86 [binder, in mathcomp.solvable.burnside_app]
sc:87 [binder, in mathcomp.solvable.burnside_app]
sc:88 [binder, in mathcomp.solvable.burnside_app]
sc:89 [binder, in mathcomp.solvable.burnside_app]
sc:90 [binder, in mathcomp.solvable.burnside_app]
sc:91 [binder, in mathcomp.solvable.burnside_app]
sc:92 [binder, in mathcomp.solvable.burnside_app]
sc:93 [binder, in mathcomp.solvable.burnside_app]
sc:94 [binder, in mathcomp.solvable.burnside_app]
sc:95 [binder, in mathcomp.solvable.burnside_app]
sc:96 [binder, in mathcomp.solvable.burnside_app]
sc:97 [binder, in mathcomp.solvable.burnside_app]
sc:98 [binder, in mathcomp.solvable.burnside_app]
sc:99 [binder, in mathcomp.solvable.burnside_app]
sdivr_closed_subproof:2178 [binder, in mathcomp.algebra.ssralg]
SdPair [constructor, in mathcomp.fingroup.gproduct]
sdpairE [lemma, in mathcomp.fingroup.gproduct]
sdpair_setact [lemma, in mathcomp.fingroup.gproduct]
sdpair_act [lemma, in mathcomp.fingroup.gproduct]
sdpair1 [definition, in mathcomp.fingroup.gproduct]
sdpair1_morphism [definition, in mathcomp.fingroup.gproduct]
sdpair1_morphM [lemma, in mathcomp.fingroup.gproduct]
sdpair2 [definition, in mathcomp.fingroup.gproduct]
sdpair2_morphism [definition, in mathcomp.fingroup.gproduct]
sdpair2_morphM [lemma, in mathcomp.fingroup.gproduct]
sdprod [abbreviation, in mathcomp.fingroup.gproduct]
sdprod [abbreviation, in mathcomp.fingroup.gproduct]
Sdprod [section, in mathcomp.character.character]
sdprodE [lemma, in mathcomp.fingroup.gproduct]
sdprodEY [lemma, in mathcomp.fingroup.gproduct]
sdprodg1 [lemma, in mathcomp.fingroup.gproduct]
sdprodJ [lemma, in mathcomp.fingroup.gproduct]
sdprodm [definition, in mathcomp.fingroup.gproduct]
sdprodmE [lemma, in mathcomp.fingroup.gproduct]
sdprodmEl [lemma, in mathcomp.fingroup.gproduct]
sdprodmEr [lemma, in mathcomp.fingroup.gproduct]
sdprodm_morphism [definition, in mathcomp.fingroup.gproduct]
sdprodm_eqf [lemma, in mathcomp.fingroup.gproduct]
sdprodm_sub [lemma, in mathcomp.fingroup.gproduct]
sdprodm_norm [lemma, in mathcomp.fingroup.gproduct]
sdprodP [lemma, in mathcomp.fingroup.gproduct]
SDproduct [section, in mathcomp.character.classfun]
SDproduct.defG [variable, in mathcomp.character.classfun]
SDproduct.G [variable, in mathcomp.character.classfun]
SDproduct.gT [variable, in mathcomp.character.classfun]
SDproduct.H [variable, in mathcomp.character.classfun]
SDproduct.K [variable, in mathcomp.character.classfun]
SDproduct.nsKG [variable, in mathcomp.character.classfun]
SDproduct.sHG [variable, in mathcomp.character.classfun]
SDproduct.sKG [variable, in mathcomp.character.classfun]
sdprodW [lemma, in mathcomp.fingroup.gproduct]
sdprodWC [lemma, in mathcomp.fingroup.gproduct]
sdprodWpp [lemma, in mathcomp.fingroup.gproduct]
sdprodWY [lemma, in mathcomp.fingroup.gproduct]
sdprod_cfker [lemma, in mathcomp.character.classfun]
sdprod_p'core_HallP [lemma, in mathcomp.solvable.pgroup]
sdprod_Hall_p'coreP [lemma, in mathcomp.solvable.pgroup]
sdprod_pcore_HallP [lemma, in mathcomp.solvable.pgroup]
sdprod_Hall_pcoreP [lemma, in mathcomp.solvable.pgroup]
sdprod_normal_pHallP [lemma, in mathcomp.solvable.pgroup]
sdprod_normal_p'HallP [lemma, in mathcomp.solvable.pgroup]
sdprod_Hall [lemma, in mathcomp.solvable.pgroup]
sdprod_sdpair [lemma, in mathcomp.fingroup.gproduct]
sdprod_groupType [definition, in mathcomp.fingroup.gproduct]
sdprod_mulgA [lemma, in mathcomp.fingroup.gproduct]
sdprod_mulVg [lemma, in mathcomp.fingroup.gproduct]
sdprod_mul1g [lemma, in mathcomp.fingroup.gproduct]
sdprod_mul [definition, in mathcomp.fingroup.gproduct]
sdprod_mul_proof [lemma, in mathcomp.fingroup.gproduct]
sdprod_inv [definition, in mathcomp.fingroup.gproduct]
sdprod_inv_proof [lemma, in mathcomp.fingroup.gproduct]
sdprod_one [definition, in mathcomp.fingroup.gproduct]
sdprod_by [inductive, in mathcomp.fingroup.gproduct]
sdprod_recr [lemma, in mathcomp.fingroup.gproduct]
sdprod_recl [lemma, in mathcomp.fingroup.gproduct]
sdprod_modr [lemma, in mathcomp.fingroup.gproduct]
sdprod_modl [lemma, in mathcomp.fingroup.gproduct]
sdprod_subr [lemma, in mathcomp.fingroup.gproduct]
sdprod_isog [lemma, in mathcomp.fingroup.gproduct]
sdprod_isom [lemma, in mathcomp.fingroup.gproduct]
sdprod_card [lemma, in mathcomp.fingroup.gproduct]
sdprod_normal_complP [lemma, in mathcomp.fingroup.gproduct]
sdprod_compl [lemma, in mathcomp.fingroup.gproduct]
sdprod_context [lemma, in mathcomp.fingroup.gproduct]
sdprod_Res_IirrK [lemma, in mathcomp.character.character]
sdprod_Res_IirrE [lemma, in mathcomp.character.character]
sdprod_Iirr0 [lemma, in mathcomp.character.character]
sdprod_Iirr_eq0 [lemma, in mathcomp.character.character]
sdprod_Iirr_inj [lemma, in mathcomp.character.character]
sdprod_IirrK [lemma, in mathcomp.character.character]
sdprod_IirrE [lemma, in mathcomp.character.character]
sdprod_Iirr [definition, in mathcomp.character.character]
Sdprod.defG [variable, in mathcomp.character.character]
Sdprod.G [variable, in mathcomp.character.character]
Sdprod.gT [variable, in mathcomp.character.character]
Sdprod.H [variable, in mathcomp.character.character]
Sdprod.K [variable, in mathcomp.character.character]
Sdprod.nKG [variable, in mathcomp.character.character]
sdprod1g [lemma, in mathcomp.fingroup.gproduct]
sdT [abbreviation, in mathcomp.fingroup.gproduct]
sdval [abbreviation, in mathcomp.fingroup.gproduct]
sd1 [definition, in mathcomp.solvable.burnside_app]
Sd1 [definition, in mathcomp.solvable.burnside_app]
sd1_inv [lemma, in mathcomp.solvable.burnside_app]
Sd1_inj [lemma, in mathcomp.solvable.burnside_app]
sd2 [definition, in mathcomp.solvable.burnside_app]
Sd2 [definition, in mathcomp.solvable.burnside_app]
sd2_inv [lemma, in mathcomp.solvable.burnside_app]
Sd2_inj [lemma, in mathcomp.solvable.burnside_app]
SecondIsomorphism [section, in mathcomp.fingroup.quotient]
SecondIsomorphism.gT [variable, in mathcomp.fingroup.quotient]
SecondIsomorphism.H [variable, in mathcomp.fingroup.quotient]
SecondIsomorphism.K [variable, in mathcomp.fingroup.quotient]
SecondIsomorphism.nKH [variable, in mathcomp.fingroup.quotient]
second_isog [lemma, in mathcomp.fingroup.quotient]
second_isom [lemma, in mathcomp.fingroup.quotient]
second_orthogonality_relation [lemma, in mathcomp.character.character]
section [inductive, in mathcomp.solvable.jordanholder]
Sections [section, in mathcomp.solvable.jordanholder]
Sections.gT [variable, in mathcomp.solvable.jordanholder]
section_repr_isog [lemma, in mathcomp.solvable.jordanholder]
section_reprP [lemma, in mathcomp.solvable.jordanholder]
section_repr [definition, in mathcomp.solvable.jordanholder]
section_isog [definition, in mathcomp.solvable.jordanholder]
section_group [definition, in mathcomp.solvable.jordanholder]
section_eqmx [lemma, in mathcomp.character.mxrepresentation]
section_eqmx_add [lemma, in mathcomp.character.mxrepresentation]
section_repr [definition, in mathcomp.character.mxrepresentation]
section_module [lemma, in mathcomp.character.mxrepresentation]
SemiDihedral [constructor, in mathcomp.solvable.extremal]
semidihedral_classP [lemma, in mathcomp.solvable.extremal]
semidihedral_structure [lemma, in mathcomp.solvable.extremal]
semidihedral_gtype [definition, in mathcomp.solvable.extremal]
semidirect_product [definition, in mathcomp.fingroup.gproduct]
SemiGroup [module, in mathcomp.ssreflect.bigop]
SemiGroupProperties [section, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian [section, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.Id [section, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.Id.opxx [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.op [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.opCA [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.x [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Id [section, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Id.op [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Id.opxx [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Id.x [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.R [variable, in mathcomp.ssreflect.bigop]
SemiGroup.com_law [abbreviation, in mathcomp.ssreflect.bigop]
SemiGroup.Exports [module, in mathcomp.ssreflect.bigop]
SemiGroup.law [abbreviation, in mathcomp.ssreflect.bigop]
SemiGroup.Theory [module, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmA [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmAC [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmACA [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmC [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmCA [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory [section, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.Commutative [section, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.Commutative.mul [variable, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.Plain [section, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.Plain.mul [variable, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.T [variable, in mathcomp.ssreflect.bigop]
SemiPolynomialTheory [section, in mathcomp.algebra.poly]
SemiPolynomialTheory.R [variable, in mathcomp.algebra.poly]
_ %:P [notation, in mathcomp.algebra.poly]
\poly_ ( _ < _ ) _ [notation, in mathcomp.algebra.poly]
semiprime [definition, in mathcomp.solvable.frobenius]
semiprimeJ [lemma, in mathcomp.solvable.frobenius]
semiprimeS [lemma, in mathcomp.solvable.frobenius]
semiprime_regular [lemma, in mathcomp.solvable.frobenius]
semiregular [definition, in mathcomp.solvable.frobenius]
semiregularJ [lemma, in mathcomp.solvable.frobenius]
semiregularS [lemma, in mathcomp.solvable.frobenius]
semiregular_prime [lemma, in mathcomp.solvable.frobenius]
semiregular_sym [lemma, in mathcomp.solvable.frobenius]
semiregular1l [lemma, in mathcomp.solvable.frobenius]
semiregular1r [lemma, in mathcomp.solvable.frobenius]
semiring_closed_subproof:2679 [binder, in mathcomp.algebra.ssralg]
semiring_closed_subproof:2666 [binder, in mathcomp.algebra.ssralg]
semiring_closed_subproof:2151 [binder, in mathcomp.algebra.ssralg]
semisimple_Socle [lemma, in mathcomp.character.mxrepresentation]
semi_additive_subproof:779 [binder, in mathcomp.algebra.ssralg]
separable [definition, in mathcomp.field.separable]
Separable [section, in mathcomp.field.separable]
separable [abbreviation, in mathcomp.field.separable]
separable [library]
separableP [lemma, in mathcomp.field.separable]
separablePn [lemma, in mathcomp.field.separable]
SeparablePoly [section, in mathcomp.field.separable]
SeparablePoly.R [variable, in mathcomp.field.separable]
separableS [lemma, in mathcomp.field.separable]
separableSl [lemma, in mathcomp.field.separable]
separableSr [lemma, in mathcomp.field.separable]
separable_Xn_sub_1 [lemma, in mathcomp.field.cyclotomic]
separable_Fadjoin_seq [lemma, in mathcomp.field.separable]
separable_trans [lemma, in mathcomp.field.separable]
separable_refl [lemma, in mathcomp.field.separable]
separable_generator_maximal [lemma, in mathcomp.field.separable]
separable_generatorP [lemma, in mathcomp.field.separable]
separable_generator_mem [lemma, in mathcomp.field.separable]
separable_generator [definition, in mathcomp.field.separable]
separable_inseparable_decomposition [lemma, in mathcomp.field.separable]
separable_sum [lemma, in mathcomp.field.separable]
separable_add [lemma, in mathcomp.field.separable]
separable_inseparable_element [lemma, in mathcomp.field.separable]
separable_exponent [lemma, in mathcomp.field.separable]
separable_elementS [lemma, in mathcomp.field.separable]
separable_root_der [lemma, in mathcomp.field.separable]
separable_nz_der [lemma, in mathcomp.field.separable]
separable_elementP [lemma, in mathcomp.field.separable]
separable_element [definition, in mathcomp.field.separable]
separable_map [lemma, in mathcomp.field.separable]
separable_prod_XsubC [lemma, in mathcomp.field.separable]
separable_root [lemma, in mathcomp.field.separable]
separable_mul [lemma, in mathcomp.field.separable]
separable_deriv_eq0 [lemma, in mathcomp.field.separable]
separable_nosquare [lemma, in mathcomp.field.separable]
separable_coprime [lemma, in mathcomp.field.separable]
separable_polyP [lemma, in mathcomp.field.separable]
separable_poly_neq0 [lemma, in mathcomp.field.separable]
separable_poly_unlockable [definition, in mathcomp.field.separable]
Separable.Derivation [section, in mathcomp.field.separable]
Separable.DerivationAlgebra [section, in mathcomp.field.separable]
Separable.DerivationAlgebra.D [variable, in mathcomp.field.separable]
Separable.DerivationAlgebra.derD [variable, in mathcomp.field.separable]
Separable.DerivationAlgebra.E [variable, in mathcomp.field.separable]
Separable.Derivation.D [variable, in mathcomp.field.separable]
Separable.Derivation.derD [variable, in mathcomp.field.separable]
Separable.Derivation.K [variable, in mathcomp.field.separable]
Separable.F [variable, in mathcomp.field.separable]
Separable.L [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem [section, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.FiniteCase [section, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.FiniteCase.cyclic_or_large [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.FiniteCase.K_is_large [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.FiniteCase.N [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.K [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.sepKy [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.x [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.y [variable, in mathcomp.field.separable]
Separable.SeparableElement [section, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation [section, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.D [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.derD [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.DerivationLinear [section, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.DerivationLinear.body [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.DerivationLinear.E [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.DerivationLinear.extendDerivationLinear [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.Dx [variable, in mathcomp.field.separable]
Separable.SeparableElement.K [variable, in mathcomp.field.separable]
Separable.SeparableElement.Kx_x [variable, in mathcomp.field.separable]
Separable.SeparableElement.sKxK [variable, in mathcomp.field.separable]
Separable.SeparableElement.x [variable, in mathcomp.field.separable]
seq [abbreviation, in mathcomp.ssreflect.seq]
seq [library]
SeqBseq [section, in mathcomp.ssreflect.tuple]
SeqBseq.m [variable, in mathcomp.ssreflect.tuple]
SeqBseq.n [variable, in mathcomp.ssreflect.tuple]
SeqBseq.rT [variable, in mathcomp.ssreflect.tuple]
SeqBseq.T [variable, in mathcomp.ssreflect.tuple]
SeqBseq.U [variable, in mathcomp.ssreflect.tuple]
SeqFinType [section, in mathcomp.ssreflect.fintype]
SeqFinType.s [variable, in mathcomp.ssreflect.fintype]
SeqFinType.T [variable, in mathcomp.ssreflect.fintype]
seqn [definition, in mathcomp.ssreflect.seq]
seqn_rec [definition, in mathcomp.ssreflect.seq]
seqn_type [definition, in mathcomp.ssreflect.seq]
SeqReplace [section, in mathcomp.ssreflect.fintype]
SeqReplace.T [variable, in mathcomp.ssreflect.fintype]
SeqSubType [section, in mathcomp.ssreflect.fintype]
SeqSubType.s [variable, in mathcomp.ssreflect.fintype]
SeqSubType.T [variable, in mathcomp.ssreflect.fintype]
seqs1 [lemma, in mathcomp.solvable.burnside_app]
SeqTuple [section, in mathcomp.ssreflect.tuple]
SeqTuple.m [variable, in mathcomp.ssreflect.tuple]
SeqTuple.n [variable, in mathcomp.ssreflect.tuple]
SeqTuple.rT [variable, in mathcomp.ssreflect.tuple]
SeqTuple.T [variable, in mathcomp.ssreflect.tuple]
SeqTuple.U [variable, in mathcomp.ssreflect.tuple]
Sequences [section, in mathcomp.ssreflect.seq]
Sequences.n0 [variable, in mathcomp.ssreflect.seq]
Sequences.SeqFind [section, in mathcomp.ssreflect.seq]
Sequences.SeqFind.a [variable, in mathcomp.ssreflect.seq]
Sequences.SubPred [section, in mathcomp.ssreflect.seq]
Sequences.SubPred.a1 [variable, in mathcomp.ssreflect.seq]
Sequences.SubPred.a2 [variable, in mathcomp.ssreflect.seq]
Sequences.SubPred.s12 [variable, in mathcomp.ssreflect.seq]
Sequences.T [variable, in mathcomp.ssreflect.seq]
Sequences.x0 [variable, in mathcomp.ssreflect.seq]
_ ++ _ (seq_scope) [notation, in mathcomp.ssreflect.seq]
seqv_sub_adjoin [lemma, in mathcomp.field.falgebra]
seq_tnthP [lemma, in mathcomp.ssreflect.tuple]
seq_predType [definition, in mathcomp.ssreflect.seq]
seq_eqclass [definition, in mathcomp.ssreflect.seq]
seq_ind2 [lemma, in mathcomp.ssreflect.seq]
seq_hasChoice [lemma, in mathcomp.ssreflect.choice]
seq_of_optK [lemma, in mathcomp.ssreflect.choice]
seq_of_opt [definition, in mathcomp.ssreflect.choice]
seq_of_cfun [definition, in mathcomp.character.classfun]
seq_iso3_L [definition, in mathcomp.solvable.burnside_app]
seq_iso_L [definition, in mathcomp.solvable.burnside_app]
seq_subE [lemma, in mathcomp.ssreflect.fintype]
seq_sub_default [lemma, in mathcomp.ssreflect.fintype]
seq_sub_isFinite [definition, in mathcomp.ssreflect.fintype]
seq_sub_axiom [lemma, in mathcomp.ssreflect.fintype]
seq_sub_isCountable [definition, in mathcomp.ssreflect.fintype]
seq_sub_pickleK [lemma, in mathcomp.ssreflect.fintype]
seq_sub_unpickle [definition, in mathcomp.ssreflect.fintype]
seq_sub_pickle [definition, in mathcomp.ssreflect.fintype]
seq_sub_enum [definition, in mathcomp.ssreflect.fintype]
seq_sub [record, in mathcomp.ssreflect.fintype]
seq1_basis [lemma, in mathcomp.algebra.vector]
seq1_free [lemma, in mathcomp.algebra.vector]
SeriesDefs [section, in mathcomp.solvable.nilpotent]
SeriesDefs.A [variable, in mathcomp.solvable.nilpotent]
SeriesDefs.gT [variable, in mathcomp.solvable.nilpotent]
SeriesDefs.n [variable, in mathcomp.solvable.nilpotent]
series_repr [definition, in mathcomp.character.mxrepresentation]
series_sol [lemma, in mathcomp.solvable.nilpotent]
setact [definition, in mathcomp.fingroup.action]
setactE [lemma, in mathcomp.fingroup.action]
setactJ [lemma, in mathcomp.fingroup.action]
setactVin [lemma, in mathcomp.fingroup.action]
setact_orbit [lemma, in mathcomp.fingroup.action]
setact_is_action [lemma, in mathcomp.fingroup.action]
setC [definition, in mathcomp.ssreflect.finset]
setCD [lemma, in mathcomp.ssreflect.finset]
setCI [lemma, in mathcomp.ssreflect.finset]
setCK [lemma, in mathcomp.ssreflect.finset]
setCP [lemma, in mathcomp.ssreflect.finset]
setCS [lemma, in mathcomp.ssreflect.finset]
setCT [lemma, in mathcomp.ssreflect.finset]
setCU [lemma, in mathcomp.ssreflect.finset]
setC_bigcap [lemma, in mathcomp.ssreflect.finset]
setC_bigcup [lemma, in mathcomp.ssreflect.finset]
setC_inj [lemma, in mathcomp.ssreflect.finset]
setC0 [lemma, in mathcomp.ssreflect.finset]
setC11 [lemma, in mathcomp.ssreflect.finset]
setD [definition, in mathcomp.ssreflect.finset]
setDDl [lemma, in mathcomp.ssreflect.finset]
setDDr [lemma, in mathcomp.ssreflect.finset]
setDE [lemma, in mathcomp.ssreflect.finset]
setDidPl [lemma, in mathcomp.ssreflect.finset]
setDIl [lemma, in mathcomp.ssreflect.finset]
setDIr [lemma, in mathcomp.ssreflect.finset]
setDP [lemma, in mathcomp.ssreflect.finset]
setDS [lemma, in mathcomp.ssreflect.finset]
setDSS [lemma, in mathcomp.ssreflect.finset]
setDT [lemma, in mathcomp.ssreflect.finset]
setDUl [lemma, in mathcomp.ssreflect.finset]
setDUr [lemma, in mathcomp.ssreflect.finset]
setDv [lemma, in mathcomp.ssreflect.finset]
setD_eq0 [lemma, in mathcomp.ssreflect.finset]
setD0 [lemma, in mathcomp.ssreflect.finset]
setD1K [lemma, in mathcomp.ssreflect.finset]
setD1P [lemma, in mathcomp.ssreflect.finset]
setD11 [lemma, in mathcomp.ssreflect.finset]
SetFixpoint [section, in mathcomp.ssreflect.finset]
SetFixpoint.Greatest [section, in mathcomp.ssreflect.finset]
SetFixpoint.Greatest.F [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Greatest.F_mono [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Greatest.T [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least [section, in mathcomp.ssreflect.finset]
SetFixpoint.Least.F [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least.F_mono [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least.iterF [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least.n [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least.T [variable, in mathcomp.ssreflect.finset]
setI [definition, in mathcomp.ssreflect.finset]
setIA [lemma, in mathcomp.ssreflect.finset]
setIAC [lemma, in mathcomp.ssreflect.finset]
setIACA [lemma, in mathcomp.ssreflect.finset]
setIC [lemma, in mathcomp.ssreflect.finset]
setICA [lemma, in mathcomp.ssreflect.finset]
setICr [lemma, in mathcomp.ssreflect.finset]
setID [lemma, in mathcomp.ssreflect.finset]
setIDA [lemma, in mathcomp.ssreflect.finset]
setIDAC [lemma, in mathcomp.ssreflect.finset]
setIdE [lemma, in mathcomp.ssreflect.finset]
setIdP [lemma, in mathcomp.ssreflect.finset]
setId2P [lemma, in mathcomp.ssreflect.finset]
setIg1 [lemma, in mathcomp.fingroup.fingroup]
setIid [lemma, in mathcomp.ssreflect.finset]
setIidPl [lemma, in mathcomp.ssreflect.finset]
setIidPr [lemma, in mathcomp.ssreflect.finset]
setIIl [lemma, in mathcomp.ssreflect.finset]
setIIr [lemma, in mathcomp.ssreflect.finset]
setIK [lemma, in mathcomp.ssreflect.finset]
setIP [lemma, in mathcomp.ssreflect.finset]
setIS [lemma, in mathcomp.ssreflect.finset]
setISS [lemma, in mathcomp.ssreflect.finset]
setIT [lemma, in mathcomp.ssreflect.finset]
setIUl [lemma, in mathcomp.ssreflect.finset]
setIUr [lemma, in mathcomp.ssreflect.finset]
setI_transversal_pblock [lemma, in mathcomp.ssreflect.finset]
setI_eq0 [lemma, in mathcomp.ssreflect.finset]
setI_powerset [lemma, in mathcomp.ssreflect.finset]
setI_group [definition, in mathcomp.fingroup.fingroup]
setI_normal_Hall [lemma, in mathcomp.solvable.pgroup]
setI_subnormal [lemma, in mathcomp.solvable.gseries]
setI_im_cpair [lemma, in mathcomp.solvable.center]
setI0 [lemma, in mathcomp.ssreflect.finset]
setI1g [lemma, in mathcomp.fingroup.fingroup]
setKI [lemma, in mathcomp.ssreflect.finset]
setKU [lemma, in mathcomp.ssreflect.finset]
setOps [section, in mathcomp.ssreflect.finset]
setOpsAlgebra [section, in mathcomp.ssreflect.finset]
setOpsAlgebra.T [variable, in mathcomp.ssreflect.finset]
setOpsDefs [section, in mathcomp.ssreflect.finset]
setOpsDefs.T [variable, in mathcomp.ssreflect.finset]
setOps.T [variable, in mathcomp.ssreflect.finset]
setP [lemma, in mathcomp.ssreflect.finset]
setSD [lemma, in mathcomp.ssreflect.finset]
setSI [lemma, in mathcomp.ssreflect.finset]
setSU [lemma, in mathcomp.ssreflect.finset]
setT [abbreviation, in mathcomp.ssreflect.finset]
setTD [lemma, in mathcomp.ssreflect.finset]
setTfor [definition, in mathcomp.ssreflect.finset]
setTI [lemma, in mathcomp.ssreflect.finset]
setTU [lemma, in mathcomp.ssreflect.finset]
SetType [section, in mathcomp.ssreflect.finset]
SetType.T [variable, in mathcomp.ssreflect.finset]
setT_group [definition, in mathcomp.fingroup.fingroup]
setU [definition, in mathcomp.ssreflect.finset]
setUA [lemma, in mathcomp.ssreflect.finset]
setUAC [lemma, in mathcomp.ssreflect.finset]
setUACA [lemma, in mathcomp.ssreflect.finset]
setUC [lemma, in mathcomp.ssreflect.finset]
setUCA [lemma, in mathcomp.ssreflect.finset]
setUCr [lemma, in mathcomp.ssreflect.finset]
setUid [lemma, in mathcomp.ssreflect.finset]
setUidPl [lemma, in mathcomp.ssreflect.finset]
setUidPr [lemma, in mathcomp.ssreflect.finset]
setUIl [lemma, in mathcomp.ssreflect.finset]
setUIr [lemma, in mathcomp.ssreflect.finset]
setUK [lemma, in mathcomp.ssreflect.finset]
setUP [lemma, in mathcomp.ssreflect.finset]
setUS [lemma, in mathcomp.ssreflect.finset]
setUSS [lemma, in mathcomp.ssreflect.finset]
setUT [lemma, in mathcomp.ssreflect.finset]
setUUl [lemma, in mathcomp.ssreflect.finset]
setUUr [lemma, in mathcomp.ssreflect.finset]
setU_eq0 [lemma, in mathcomp.ssreflect.finset]
setU0 [lemma, in mathcomp.ssreflect.finset]
setU1K [lemma, in mathcomp.ssreflect.finset]
setU1P [lemma, in mathcomp.ssreflect.finset]
setU1r [lemma, in mathcomp.ssreflect.finset]
setU11 [lemma, in mathcomp.ssreflect.finset]
setX [definition, in mathcomp.ssreflect.finset]
setXP [lemma, in mathcomp.ssreflect.finset]
setXS [lemma, in mathcomp.ssreflect.finset]
setX_gen [lemma, in mathcomp.fingroup.gproduct]
setX_dprod [lemma, in mathcomp.fingroup.gproduct]
setX_prod [lemma, in mathcomp.fingroup.gproduct]
setX_group [definition, in mathcomp.fingroup.gproduct]
set_gring_classM_coef [lemma, in mathcomp.character.integral_char]
set_of_coset [projection, in mathcomp.fingroup.quotient]
set_nth_default [lemma, in mathcomp.ssreflect.seq]
set_nthE [lemma, in mathcomp.ssreflect.seq]
set_set_nth [lemma, in mathcomp.ssreflect.seq]
set_nth_nil [lemma, in mathcomp.ssreflect.seq]
set_nth [definition, in mathcomp.ssreflect.seq]
set_partition_big [lemma, in mathcomp.ssreflect.finset]
set_partition_big_cond [lemma, in mathcomp.ssreflect.finset]
set_cons [lemma, in mathcomp.ssreflect.finset]
set_seq1 [lemma, in mathcomp.ssreflect.finset]
set_nil [lemma, in mathcomp.ssreflect.finset]
set_enum [lemma, in mathcomp.ssreflect.finset]
set_0Vmem [lemma, in mathcomp.ssreflect.finset]
set_predType [definition, in mathcomp.ssreflect.finset]
set_isSub [definition, in mathcomp.ssreflect.finset]
set_of [definition, in mathcomp.ssreflect.finset]
set_type [inductive, in mathcomp.ssreflect.finset]
set_action [definition, in mathcomp.fingroup.action]
set_invgM [lemma, in mathcomp.fingroup.fingroup]
set_invgK [lemma, in mathcomp.fingroup.fingroup]
set_mulgA [lemma, in mathcomp.fingroup.fingroup]
set_mul1g [lemma, in mathcomp.fingroup.fingroup]
set_invg [definition, in mathcomp.fingroup.fingroup]
set_mulg [definition, in mathcomp.fingroup.fingroup]
set_Frobenius_compl [lemma, in mathcomp.solvable.frobenius]
set0 [definition, in mathcomp.ssreflect.finset]
set0D [lemma, in mathcomp.ssreflect.finset]
set0I [lemma, in mathcomp.ssreflect.finset]
set0Pn [lemma, in mathcomp.ssreflect.finset]
set0U [lemma, in mathcomp.ssreflect.finset]
set1gE [lemma, in mathcomp.fingroup.fingroup]
set1gP [lemma, in mathcomp.fingroup.fingroup]
set1P [lemma, in mathcomp.ssreflect.finset]
set1Ul [lemma, in mathcomp.ssreflect.finset]
set1Ur [lemma, in mathcomp.ssreflect.finset]
set1_inj [lemma, in mathcomp.ssreflect.finset]
set1_group [definition, in mathcomp.fingroup.fingroup]
set11 [lemma, in mathcomp.ssreflect.finset]
set2P [lemma, in mathcomp.ssreflect.finset]
set21 [lemma, in mathcomp.ssreflect.finset]
set22 [lemma, in mathcomp.ssreflect.finset]
sG [abbreviation, in mathcomp.character.mxrepresentation]
sGD:175 [binder, in mathcomp.solvable.frobenius]
sGD:179 [binder, in mathcomp.solvable.frobenius]
sGD:182 [binder, in mathcomp.solvable.frobenius]
sGD:184 [binder, in mathcomp.solvable.frobenius]
sGD:659 [binder, in mathcomp.character.character]
sgr [abbreviation, in mathcomp.algebra.ssrint]
sgr [abbreviation, in mathcomp.algebra.rat]
sgrEz [lemma, in mathcomp.algebra.ssrint]
sgrMz [lemma, in mathcomp.algebra.ssrint]
sgrz [lemma, in mathcomp.algebra.ssrint]
sgr_numq [lemma, in mathcomp.algebra.rat]
sgr_numq_div [lemma, in mathcomp.algebra.rat]
sgr_denq [lemma, in mathcomp.algebra.rat]
sgr_scalq [lemma, in mathcomp.algebra.rat]
sgval [definition, in mathcomp.fingroup.fingroup]
sgvalK [lemma, in mathcomp.fingroup.fingroup]
sgvalM [lemma, in mathcomp.fingroup.fingroup]
sgvalmK [lemma, in mathcomp.fingroup.morphism]
sgval_sub [lemma, in mathcomp.fingroup.morphism]
sgval_morphism [definition, in mathcomp.fingroup.morphism]
sgz [definition, in mathcomp.algebra.ssrint]
Sgz [section, in mathcomp.algebra.ssrint]
sgzE [definition, in mathcomp.algebra.ssrint]
sgzM [lemma, in mathcomp.algebra.ssrint]
sgzN [lemma, in mathcomp.algebra.ssrint]
SgzNeg [constructor, in mathcomp.algebra.ssrint]
SgzNull [constructor, in mathcomp.algebra.ssrint]
sgzN1 [lemma, in mathcomp.algebra.ssrint]
sgzP [lemma, in mathcomp.algebra.ssrint]
SgzPos [constructor, in mathcomp.algebra.ssrint]
SgzReal [section, in mathcomp.algebra.ssrint]
SgzReal.R [variable, in mathcomp.algebra.ssrint]
sgzX [lemma, in mathcomp.algebra.ssrint]
sgz_lead_primitive [lemma, in mathcomp.algebra.intdiv]
sgz_contents [lemma, in mathcomp.algebra.intdiv]
sgz_eq [lemma, in mathcomp.algebra.ssrint]
sgz_smul [lemma, in mathcomp.algebra.ssrint]
sgz_le0 [lemma, in mathcomp.algebra.ssrint]
sgz_ge0 [lemma, in mathcomp.algebra.ssrint]
sgz_lt0 [lemma, in mathcomp.algebra.ssrint]
sgz_gt0 [lemma, in mathcomp.algebra.ssrint]
sgz_odd [lemma, in mathcomp.algebra.ssrint]
sgz_eq0 [lemma, in mathcomp.algebra.ssrint]
sgz_val [inductive, in mathcomp.algebra.ssrint]
sgz_cp0 [lemma, in mathcomp.algebra.ssrint]
sgz_id [lemma, in mathcomp.algebra.ssrint]
sgz_int [lemma, in mathcomp.algebra.ssrint]
sgz_sgr [lemma, in mathcomp.algebra.ssrint]
sgz_def [lemma, in mathcomp.algebra.ssrint]
Sgz.R [variable, in mathcomp.algebra.ssrint]
sgz0 [lemma, in mathcomp.algebra.ssrint]
sgz1 [lemma, in mathcomp.algebra.ssrint]
sG_Vg:245 [binder, in mathcomp.solvable.cyclic]
sG_1g:244 [binder, in mathcomp.solvable.cyclic]
sG_Ag:243 [binder, in mathcomp.solvable.cyclic]
sG_M:242 [binder, in mathcomp.solvable.cyclic]
sG_V:239 [binder, in mathcomp.solvable.cyclic]
sG_MP:237 [binder, in mathcomp.solvable.cyclic]
sG_VP:234 [binder, in mathcomp.solvable.cyclic]
sG_1:232 [binder, in mathcomp.solvable.cyclic]
sG:1308 [binder, in mathcomp.character.mxrepresentation]
sG:1331 [binder, in mathcomp.character.mxrepresentation]
sG:156 [binder, in mathcomp.character.character]
sg:264 [binder, in mathcomp.field.closed_field]
sh [definition, in mathcomp.solvable.burnside_app]
Sh [definition, in mathcomp.solvable.burnside_app]
shape [definition, in mathcomp.ssreflect.seq]
shape_rev [lemma, in mathcomp.ssreflect.seq]
sHG:631 [binder, in mathcomp.character.character]
shorten [definition, in mathcomp.ssreflect.path]
shortenP [lemma, in mathcomp.ssreflect.path]
ShortenSpec [constructor, in mathcomp.ssreflect.path]
shorten_spec [inductive, in mathcomp.ssreflect.path]
sh_inv [lemma, in mathcomp.solvable.burnside_app]
Sh_inj [lemma, in mathcomp.solvable.burnside_app]
sh:1665 [binder, in mathcomp.ssreflect.seq]
sh:1669 [binder, in mathcomp.ssreflect.seq]
sh:1672 [binder, in mathcomp.ssreflect.seq]
sh:1674 [binder, in mathcomp.ssreflect.seq]
sh:1679 [binder, in mathcomp.ssreflect.seq]
sh:1681 [binder, in mathcomp.ssreflect.seq]
sh:1685 [binder, in mathcomp.ssreflect.seq]
sh:1687 [binder, in mathcomp.ssreflect.seq]
sh:1708 [binder, in mathcomp.ssreflect.seq]
sh:1711 [binder, in mathcomp.ssreflect.seq]
sh:1714 [binder, in mathcomp.ssreflect.seq]
sh:1718 [binder, in mathcomp.ssreflect.seq]
sh:1720 [binder, in mathcomp.ssreflect.seq]
sh:1722 [binder, in mathcomp.ssreflect.seq]
sh:1724 [binder, in mathcomp.ssreflect.seq]
sh:1727 [binder, in mathcomp.ssreflect.seq]
sh:1734 [binder, in mathcomp.ssreflect.seq]
sh:1758 [binder, in mathcomp.ssreflect.seq]
signr_scalq [lemma, in mathcomp.algebra.rat]
sign_morph [definition, in mathcomp.solvable.alt]
sigW [lemma, in mathcomp.ssreflect.choice]
sig_eqW [lemma, in mathcomp.ssreflect.choice]
sig_big_dep [lemma, in mathcomp.ssreflect.bigop]
sig_big_dep_idem [lemma, in mathcomp.ssreflect.bigop]
sig2W [lemma, in mathcomp.ssreflect.choice]
sig2_eqW [lemma, in mathcomp.ssreflect.choice]
Simmxity [section, in mathcomp.algebra.mxpoly]
Simmxity.Simmx [section, in mathcomp.algebra.mxpoly]
simmxLR [lemma, in mathcomp.algebra.mxpoly]
simmxP [lemma, in mathcomp.algebra.mxpoly]
simmxPp [lemma, in mathcomp.algebra.mxpoly]
simmxRL [lemma, in mathcomp.algebra.mxpoly]
simmxW [lemma, in mathcomp.algebra.mxpoly]
simmx_minpoly [lemma, in mathcomp.algebra.mxpoly]
simmx_in_to [abbreviation, in mathcomp.algebra.mxpoly]
simmx_in [abbreviation, in mathcomp.algebra.mxpoly]
simmx_for [abbreviation, in mathcomp.algebra.mxpoly]
simmx_to_for [definition, in mathcomp.algebra.mxpoly]
simp [abbreviation, in mathcomp.algebra.polydiv]
simp [abbreviation, in mathcomp.algebra.matrix]
simp [abbreviation, in mathcomp.algebra.poly]
simp [abbreviation, in mathcomp.algebra.mxalgebra]
Simple [section, in mathcomp.solvable.gseries]
simple [definition, in mathcomp.solvable.gseries]
simpleP [lemma, in mathcomp.solvable.gseries]
simple_Alt5 [lemma, in mathcomp.solvable.alt]
simple_Alt5_base [lemma, in mathcomp.solvable.alt]
simple_Alt_3 [lemma, in mathcomp.solvable.alt]
simple_compsP [lemma, in mathcomp.solvable.jordanholder]
simple_Socle [lemma, in mathcomp.character.mxrepresentation]
simple_maxnormal [lemma, in mathcomp.solvable.gseries]
simple_sol_prime [lemma, in mathcomp.solvable.maximal]
simplrefl [abbreviation, in mathcomp.ssreflect.ssrAC]
simU:946 [binder, in mathcomp.character.mxrepresentation]
size [definition, in mathcomp.ssreflect.seq]
sizeY [definition, in mathcomp.algebra.polyXY]
sizeYE [lemma, in mathcomp.algebra.polyXY]
sizeY_mulX [lemma, in mathcomp.algebra.polyXY]
sizeY_eq0 [lemma, in mathcomp.algebra.polyXY]
size_rat_int_poly [lemma, in mathcomp.algebra.intdiv]
size_zprimitive [lemma, in mathcomp.algebra.intdiv]
size_widen_bseq [lemma, in mathcomp.ssreflect.tuple]
size_cast_bseq [lemma, in mathcomp.ssreflect.tuple]
size_insub_bseq [lemma, in mathcomp.ssreflect.tuple]
size_bseq [lemma, in mathcomp.ssreflect.tuple]
size_tuple [lemma, in mathcomp.ssreflect.tuple]
size_Cyclotomic [lemma, in mathcomp.field.cyclotomic]
size_cyclotomic [lemma, in mathcomp.field.cyclotomic]
size_permutations [lemma, in mathcomp.ssreflect.seq]
size_tally_seq [lemma, in mathcomp.ssreflect.seq]
size_allpairs [lemma, in mathcomp.ssreflect.seq]
size_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
size_suffix [lemma, in mathcomp.ssreflect.seq]
size_prefix [lemma, in mathcomp.ssreflect.seq]
size_infix [lemma, in mathcomp.ssreflect.seq]
size_reshape [lemma, in mathcomp.ssreflect.seq]
size_flatten [lemma, in mathcomp.ssreflect.seq]
size_zip [lemma, in mathcomp.ssreflect.seq]
size_scanl [lemma, in mathcomp.ssreflect.seq]
size_pairmap [lemma, in mathcomp.ssreflect.seq]
size_mkseq [lemma, in mathcomp.ssreflect.seq]
size_iota [lemma, in mathcomp.ssreflect.seq]
size_pmap_sub [lemma, in mathcomp.ssreflect.seq]
size_pmap [lemma, in mathcomp.ssreflect.seq]
size_map [lemma, in mathcomp.ssreflect.seq]
size_rem [lemma, in mathcomp.ssreflect.seq]
size_subseq_leqif [lemma, in mathcomp.ssreflect.seq]
size_subseq [lemma, in mathcomp.ssreflect.seq]
size_mask [lemma, in mathcomp.ssreflect.seq]
size_rotr [lemma, in mathcomp.ssreflect.seq]
size_incr_nth [lemma, in mathcomp.ssreflect.seq]
size_undup [lemma, in mathcomp.ssreflect.seq]
size_eq0 [lemma, in mathcomp.ssreflect.seq]
size_rev [lemma, in mathcomp.ssreflect.seq]
size_rot [lemma, in mathcomp.ssreflect.seq]
size_take_min [lemma, in mathcomp.ssreflect.seq]
size_take [lemma, in mathcomp.ssreflect.seq]
size_takel [lemma, in mathcomp.ssreflect.seq]
size_drop [lemma, in mathcomp.ssreflect.seq]
size_filter [lemma, in mathcomp.ssreflect.seq]
size_set_nth [lemma, in mathcomp.ssreflect.seq]
size_belast [lemma, in mathcomp.ssreflect.seq]
size_rcons [lemma, in mathcomp.ssreflect.seq]
size_cat [lemma, in mathcomp.ssreflect.seq]
size_nseq [lemma, in mathcomp.ssreflect.seq]
size_ncons [lemma, in mathcomp.ssreflect.seq]
size_behead [lemma, in mathcomp.ssreflect.seq]
size_minCpoly [lemma, in mathcomp.field.algC]
size_minPoly [lemma, in mathcomp.field.fieldext]
size_Fadjoin_poly [lemma, in mathcomp.field.fieldext]
size_mod_mxminpoly [lemma, in mathcomp.algebra.mxpoly]
size_mxminpoly [lemma, in mathcomp.algebra.mxpoly]
size_char_poly [lemma, in mathcomp.algebra.mxpoly]
size_cfclass [lemma, in mathcomp.character.inertia]
size_traject [lemma, in mathcomp.ssreflect.path]
size_sort [lemma, in mathcomp.ssreflect.path]
size_merge_sort_push [lemma, in mathcomp.ssreflect.path]
size_merge [lemma, in mathcomp.ssreflect.path]
size_poly_XmY [lemma, in mathcomp.algebra.polyXY]
size_poly_XaY [lemma, in mathcomp.algebra.polyXY]
size_abelian_type [lemma, in mathcomp.solvable.abelian]
size_orbit [lemma, in mathcomp.ssreflect.fingraph]
size_basis [lemma, in mathcomp.algebra.vector]
size_enum_ord [lemma, in mathcomp.ssreflect.fintype]
size_codom [lemma, in mathcomp.ssreflect.fintype]
size_image [lemma, in mathcomp.ssreflect.fintype]
size_map_poly [lemma, in mathcomp.algebra.poly]
size_comp_poly2 [lemma, in mathcomp.algebra.poly]
size_comp_poly [lemma, in mathcomp.algebra.poly]
size_exp [lemma, in mathcomp.algebra.poly]
size_prod_eq1 [lemma, in mathcomp.algebra.poly]
size_prod_seq_eq1 [lemma, in mathcomp.algebra.poly]
size_mul_eq1 [lemma, in mathcomp.algebra.poly]
size_prod_seq [lemma, in mathcomp.algebra.poly]
size_prod [lemma, in mathcomp.algebra.poly]
size_Cmul [lemma, in mathcomp.algebra.poly]
size_scale [lemma, in mathcomp.algebra.poly]
size_mul [lemma, in mathcomp.algebra.poly]
size_drop_poly [lemma, in mathcomp.algebra.poly]
size_take_poly [lemma, in mathcomp.algebra.poly]
size_odd_poly_eq [lemma, in mathcomp.algebra.poly]
size_odd_poly [lemma, in mathcomp.algebra.poly]
size_even_poly_eq [lemma, in mathcomp.algebra.poly]
size_even_poly [lemma, in mathcomp.algebra.poly]
size_comp_poly_leq [lemma, in mathcomp.algebra.poly]
size_map_polyC [lemma, in mathcomp.algebra.poly]
size_map_inj_poly [lemma, in mathcomp.algebra.poly]
size_map_poly_id0 [lemma, in mathcomp.algebra.poly]
size_Xn_sub_1 [lemma, in mathcomp.algebra.poly]
size_exp_XsubC [lemma, in mathcomp.algebra.poly]
size_prod_XsubC [lemma, in mathcomp.algebra.poly]
size_Mmonic [lemma, in mathcomp.algebra.poly]
size_monicM [lemma, in mathcomp.algebra.poly]
size_mulXn [lemma, in mathcomp.algebra.poly]
size_polyXn [lemma, in mathcomp.algebra.poly]
size_XmulC [lemma, in mathcomp.algebra.poly]
size_mulX [lemma, in mathcomp.algebra.poly]
size_MXaddC [lemma, in mathcomp.algebra.poly]
size_XaddC [lemma, in mathcomp.algebra.poly]
size_XsubC [lemma, in mathcomp.algebra.poly]
size_polyX [lemma, in mathcomp.algebra.poly]
size_scale_leq [lemma, in mathcomp.algebra.poly]
size_Msign [lemma, in mathcomp.algebra.poly]
size_opp [lemma, in mathcomp.algebra.poly]
size_exp_leq [lemma, in mathcomp.algebra.poly]
size_prod_leq [lemma, in mathcomp.algebra.poly]
size_proper_mul [lemma, in mathcomp.algebra.poly]
size_mul_leq [lemma, in mathcomp.algebra.poly]
size_poly1 [lemma, in mathcomp.algebra.poly]
size_sum [lemma, in mathcomp.algebra.poly]
size_addl [lemma, in mathcomp.algebra.poly]
size_add [lemma, in mathcomp.algebra.poly]
size_polyC_leq1 [lemma, in mathcomp.algebra.poly]
size_poly1P [lemma, in mathcomp.algebra.poly]
size_poly_gt0 [lemma, in mathcomp.algebra.poly]
size_poly_leq0P [lemma, in mathcomp.algebra.poly]
size_poly_leq0 [lemma, in mathcomp.algebra.poly]
size_poly_eq0 [lemma, in mathcomp.algebra.poly]
size_poly0 [lemma, in mathcomp.algebra.poly]
size_poly_eq [lemma, in mathcomp.algebra.poly]
size_poly [lemma, in mathcomp.algebra.poly]
size_Poly [lemma, in mathcomp.algebra.poly]
size_cons_poly [lemma, in mathcomp.algebra.poly]
size_polyC [lemma, in mathcomp.algebra.poly]
size_mk_monic [lemma, in mathcomp.algebra.qpoly]
size_mk_monic_gt0 [lemma, in mathcomp.algebra.qpoly]
size_mk_monic_gt1 [lemma, in mathcomp.algebra.qpoly]
size_lagrange [lemma, in mathcomp.algebra.qpoly]
size_lagrange_ [lemma, in mathcomp.algebra.qpoly]
size_npoly0 [lemma, in mathcomp.algebra.qpoly]
size_npoly [lemma, in mathcomp.algebra.qpoly]
size0nil [lemma, in mathcomp.ssreflect.seq]
size1_zip [lemma, in mathcomp.ssreflect.seq]
size1_polyC [lemma, in mathcomp.algebra.poly]
size2_zip [lemma, in mathcomp.ssreflect.seq]
skew_field_dimS [lemma, in mathcomp.field.falgebra]
skew_field_module_dimS [lemma, in mathcomp.field.falgebra]
skew_field_module_semisimple [lemma, in mathcomp.field.falgebra]
skew_field_algid1 [lemma, in mathcomp.field.falgebra]
sk:318 [binder, in mathcomp.ssreflect.eqtype]
small_nil_class [lemma, in mathcomp.solvable.sylow]
smulr_closed_subproof:2142 [binder, in mathcomp.algebra.ssralg]
snd_morphism [definition, in mathcomp.fingroup.gproduct]
snd_morphM [lemma, in mathcomp.fingroup.gproduct]
snd_is_scalable [lemma, in mathcomp.algebra.ssralg]
snd_is_multiplicative [lemma, in mathcomp.algebra.ssralg]
snd_is_semi_additive [lemma, in mathcomp.algebra.ssralg]
soc [abbreviation, in mathcomp.character.character]
Socle [definition, in mathcomp.character.mxrepresentation]
socleP [lemma, in mathcomp.character.mxrepresentation]
socleType [record, in mathcomp.character.mxrepresentation]
socle_rsimP [lemma, in mathcomp.character.mxrepresentation]
socle_irr [lemma, in mathcomp.character.mxrepresentation]
Socle_iso [lemma, in mathcomp.character.mxrepresentation]
Socle_direct [lemma, in mathcomp.character.mxrepresentation]
Socle_semisimple [lemma, in mathcomp.character.mxrepresentation]
Socle_module [lemma, in mathcomp.character.mxrepresentation]
socle_can_subproof [lemma, in mathcomp.character.mxrepresentation]
socle_mem [lemma, in mathcomp.character.mxrepresentation]
socle_repr [definition, in mathcomp.character.mxrepresentation]
socle_module [definition, in mathcomp.character.mxrepresentation]
socle_simple [lemma, in mathcomp.character.mxrepresentation]
socle_mult [definition, in mathcomp.character.mxrepresentation]
socle_val [definition, in mathcomp.character.mxrepresentation]
socle_base [definition, in mathcomp.character.mxrepresentation]
socle_sort [inductive, in mathcomp.character.mxrepresentation]
socle_enum [definition, in mathcomp.character.mxrepresentation]
socle_exists [lemma, in mathcomp.character.mxrepresentation]
socle_base_enum [projection, in mathcomp.character.mxrepresentation]
socle_of_Iirr_bij [lemma, in mathcomp.character.character]
socle_of_IirrK [lemma, in mathcomp.character.character]
socle_Iirr0 [lemma, in mathcomp.character.character]
socle_of_Iirr [definition, in mathcomp.character.character]
Solvable [section, in mathcomp.solvable.nilpotent]
solvable [definition, in mathcomp.solvable.nilpotent]
SolvablePrimeFactor [section, in mathcomp.solvable.maximal]
SolvablePrimeFactor.G [variable, in mathcomp.solvable.maximal]
SolvablePrimeFactor.gT [variable, in mathcomp.solvable.maximal]
solvableS [lemma, in mathcomp.solvable.nilpotent]
solvable_irr_extendible_from_det [lemma, in mathcomp.character.inertia]
solvable_has_lin_char [lemma, in mathcomp.character.character]
solvable_norm_abelem [lemma, in mathcomp.solvable.maximal]
Solvable.gT [variable, in mathcomp.solvable.nilpotent]
solvable1 [lemma, in mathcomp.solvable.nilpotent]
Solver [section, in mathcomp.algebra.vector]
Solver.K [variable, in mathcomp.algebra.vector]
Solver.lhs [variable, in mathcomp.algebra.vector]
Solver.lhsf [variable, in mathcomp.algebra.vector]
Solver.n [variable, in mathcomp.algebra.vector]
Solver.rhs [variable, in mathcomp.algebra.vector]
Solver.vT [variable, in mathcomp.algebra.vector]
solve_monicpoly:370 [binder, in mathcomp.field.closed_field]
solve_monicpoly:2005 [binder, in mathcomp.algebra.ssralg]
sol_coprime_Sylow_subset [lemma, in mathcomp.solvable.hall]
sol_coprime_Sylow_trans [lemma, in mathcomp.solvable.hall]
sol_coprime_Sylow_exists [lemma, in mathcomp.solvable.hall]
sol_prime_factor_exists [lemma, in mathcomp.solvable.maximal]
sol_der1_proper [lemma, in mathcomp.solvable.nilpotent]
SomeHall [section, in mathcomp.solvable.sylow]
SomeHall.gT [variable, in mathcomp.solvable.sylow]
some_big_AC_mk_monoid [lemma, in mathcomp.ssreflect.bigop]
sop [definition, in mathcomp.solvable.burnside_app]
sop_morph [lemma, in mathcomp.solvable.burnside_app]
sop_spec [lemma, in mathcomp.solvable.burnside_app]
sop_inj [lemma, in mathcomp.solvable.burnside_app]
sort [definition, in mathcomp.ssreflect.path]
sortE [lemma, in mathcomp.ssreflect.path]
sorted [abbreviation, in mathcomp.ssreflect.path]
sorted [abbreviation, in mathcomp.ssreflect.path]
sorted [definition, in mathcomp.ssreflect.path]
sortedP [lemma, in mathcomp.ssreflect.path]
sorted_subseq_sort_in [lemma, in mathcomp.ssreflect.path]
sorted_subseq_sort [lemma, in mathcomp.ssreflect.path]
sorted_mask_sort_in [lemma, in mathcomp.ssreflect.path]
sorted_mask_sort [lemma, in mathcomp.ssreflect.path]
sorted_sort_in [lemma, in mathcomp.ssreflect.path]
sorted_sort [lemma, in mathcomp.ssreflect.path]
sorted_merge [lemma, in mathcomp.ssreflect.path]
sorted_eq_in [lemma, in mathcomp.ssreflect.path]
sorted_uniq_in [lemma, in mathcomp.ssreflect.path]
sorted_leq_index [lemma, in mathcomp.ssreflect.path]
sorted_ltn_index [lemma, in mathcomp.ssreflect.path]
sorted_eq [lemma, in mathcomp.ssreflect.path]
sorted_uniq [lemma, in mathcomp.ssreflect.path]
sorted_leq_index_in [lemma, in mathcomp.ssreflect.path]
sorted_ltn_index_in [lemma, in mathcomp.ssreflect.path]
sorted_map [lemma, in mathcomp.ssreflect.path]
sorted_leq_nth [lemma, in mathcomp.ssreflect.path]
sorted_ltn_nth [lemma, in mathcomp.ssreflect.path]
sorted_filter [lemma, in mathcomp.ssreflect.path]
sorted_mask [lemma, in mathcomp.ssreflect.path]
sorted_pairwise [lemma, in mathcomp.ssreflect.path]
sorted_leq_nth_in [lemma, in mathcomp.ssreflect.path]
sorted_ltn_nth_in [lemma, in mathcomp.ssreflect.path]
sorted_filter_in [lemma, in mathcomp.ssreflect.path]
sorted_mask_in [lemma, in mathcomp.ssreflect.path]
sorted_pairwise_in [lemma, in mathcomp.ssreflect.path]
sorted_relI [lemma, in mathcomp.ssreflect.path]
sorted_divisors_ltn [lemma, in mathcomp.ssreflect.prime]
sorted_divisors [lemma, in mathcomp.ssreflect.prime]
sorted_primes [lemma, in mathcomp.ssreflect.prime]
SortMap [section, in mathcomp.ssreflect.path]
SortMap.f [variable, in mathcomp.ssreflect.path]
SortMap.leT [variable, in mathcomp.ssreflect.path]
SortMap.Monotonicity [section, in mathcomp.ssreflect.path]
SortMap.Monotonicity.f_mono [variable, in mathcomp.ssreflect.path]
SortMap.Monotonicity.leT [variable, in mathcomp.ssreflect.path]
SortMap.Monotonicity.leT' [variable, in mathcomp.ssreflect.path]
SortMap.T [variable, in mathcomp.ssreflect.path]
SortMap.T' [variable, in mathcomp.ssreflect.path]
SortSeq [section, in mathcomp.ssreflect.path]
SortSeq.leElex [variable, in mathcomp.ssreflect.path]
SortSeq.leT [variable, in mathcomp.ssreflect.path]
SortSeq.leT_tr [variable, in mathcomp.ssreflect.path]
SortSeq.leT_total [variable, in mathcomp.ssreflect.path]
SortSeq.Stability [section, in mathcomp.ssreflect.path]
SortSeq.Stability.leT_lex [variable, in mathcomp.ssreflect.path]
SortSeq.Stability.leT_total [variable, in mathcomp.ssreflect.path]
SortSeq.Stability.leT' [variable, in mathcomp.ssreflect.path]
SortSeq.Stability.leT'_tr [variable, in mathcomp.ssreflect.path]
SortSeq.T [variable, in mathcomp.ssreflect.path]
sort_bseq [definition, in mathcomp.ssreflect.tuple]
sort_bseqP [lemma, in mathcomp.ssreflect.tuple]
sort_tuple [definition, in mathcomp.ssreflect.tuple]
sort_tupleP [lemma, in mathcomp.ssreflect.tuple]
sort_sorted_in [lemma, in mathcomp.ssreflect.path]
sort_sorted [lemma, in mathcomp.ssreflect.path]
sort_stable_in [lemma, in mathcomp.ssreflect.path]
sort_stable [lemma, in mathcomp.ssreflect.path]
sort_pairwise_stable [lemma, in mathcomp.ssreflect.path]
sort_iota_stable [lemma, in mathcomp.ssreflect.path]
sort_uniq [lemma, in mathcomp.ssreflect.path]
sort_map [lemma, in mathcomp.ssreflect.path]
sort_rec1 [definition, in mathcomp.ssreflect.path]
sp [abbreviation, in mathcomp.algebra.matrix]
sp [abbreviation, in mathcomp.algebra.matrix]
sp [abbreviation, in mathcomp.algebra.matrix]
sp [abbreviation, in mathcomp.algebra.matrix]
sp [abbreviation, in mathcomp.algebra.matrix]
sp [abbreviation, in mathcomp.algebra.matrix]
sp [abbreviation, in mathcomp.algebra.matrix]
sp [abbreviation, in mathcomp.algebra.matrix]
sp [abbreviation, in mathcomp.algebra.matrix]
Space [constructor, in mathcomp.algebra.vector]
space [inductive, in mathcomp.algebra.vector]
span [definition, in mathcomp.algebra.vector]
span_orthogonal [lemma, in mathcomp.character.classfun]
span_bigcat [lemma, in mathcomp.algebra.vector]
span_basis [lemma, in mathcomp.algebra.vector]
span_cat [lemma, in mathcomp.algebra.vector]
span_cons [lemma, in mathcomp.algebra.vector]
span_seq1 [lemma, in mathcomp.algebra.vector]
span_nil [lemma, in mathcomp.algebra.vector]
span_def [lemma, in mathcomp.algebra.vector]
span_subvP [lemma, in mathcomp.algebra.vector]
span_unlockable [definition, in mathcomp.algebra.vector]
span_expanded_def [definition, in mathcomp.algebra.vector]
span_key [lemma, in mathcomp.algebra.vector]
Special [section, in mathcomp.solvable.maximal]
special [definition, in mathcomp.solvable.maximal]
SpecializeExtremals [section, in mathcomp.solvable.extremal]
SpecializeExtremals.m [variable, in mathcomp.solvable.extremal]
SpecializeExtremals.p [variable, in mathcomp.solvable.extremal]
SpecializeExtremals.q [variable, in mathcomp.solvable.extremal]
Special.A [variable, in mathcomp.solvable.maximal]
Special.G [variable, in mathcomp.solvable.maximal]
Special.gT [variable, in mathcomp.solvable.maximal]
Special.p [variable, in mathcomp.solvable.maximal]
Split [constructor, in mathcomp.ssreflect.path]
split [inductive, in mathcomp.ssreflect.path]
split [definition, in mathcomp.ssreflect.fintype]
SplitHi [constructor, in mathcomp.ssreflect.fintype]
splitK [lemma, in mathcomp.ssreflect.fintype]
Splitl [constructor, in mathcomp.ssreflect.path]
splitl [inductive, in mathcomp.ssreflect.path]
SplitLo [constructor, in mathcomp.ssreflect.fintype]
SplitOrdHi [constructor, in mathcomp.ssreflect.fintype]
SplitOrdLo [constructor, in mathcomp.ssreflect.fintype]
splitP [lemma, in mathcomp.ssreflect.path]
splitP [lemma, in mathcomp.ssreflect.fintype]
splitPl [lemma, in mathcomp.ssreflect.path]
splitPr [lemma, in mathcomp.ssreflect.path]
splitP2r [lemma, in mathcomp.ssreflect.path]
Splitr [constructor, in mathcomp.ssreflect.path]
splitr [inductive, in mathcomp.ssreflect.path]
splitsP [lemma, in mathcomp.fingroup.gproduct]
splits_over [definition, in mathcomp.fingroup.gproduct]
Splitting [section, in mathcomp.field.qfpoly]
SplittingFieldExports [module, in mathcomp.field.galois]
[ splittingFieldType _ of _ ] (form_scope) [notation, in mathcomp.field.galois]
[ splittingFieldType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.galois]
splittingFieldFor [definition, in mathcomp.field.galois]
SplittingFieldFor [section, in mathcomp.field.galois]
splittingFieldForS [lemma, in mathcomp.field.galois]
SplittingFieldFor.F [variable, in mathcomp.field.galois]
SplittingFieldFor.L [variable, in mathcomp.field.galois]
splittingFieldP [lemma, in mathcomp.field.galois]
splittingFieldP_subproof:152 [binder, in mathcomp.field.galois]
SplittingFieldTheory [section, in mathcomp.field.galois]
SplittingFieldTheory.F [variable, in mathcomp.field.galois]
SplittingFieldTheory.L [variable, in mathcomp.field.galois]
splittingPoly [lemma, in mathcomp.field.galois]
splitting_galoisField [lemma, in mathcomp.field.galois]
splitting_normalField [lemma, in mathcomp.field.galois]
splitting_field_normal [lemma, in mathcomp.field.galois]
splitting_field_axiom [definition, in mathcomp.field.galois]
splitting_cyclic_primitive_root [lemma, in mathcomp.character.mxrepresentation]
Splitting.F [variable, in mathcomp.field.qfpoly]
Splitting.h [variable, in mathcomp.field.qfpoly]
Splitting.hI [variable, in mathcomp.field.qfpoly]
split_find [lemma, in mathcomp.ssreflect.seq]
split_find_spec [inductive, in mathcomp.ssreflect.seq]
split_find_nth [lemma, in mathcomp.ssreflect.seq]
split_find_nth_spec [inductive, in mathcomp.ssreflect.seq]
split_ordP [lemma, in mathcomp.ssreflect.fintype]
split_ord_spec [inductive, in mathcomp.ssreflect.fintype]
split_spec [inductive, in mathcomp.ssreflect.fintype]
split_subproof [lemma, in mathcomp.ssreflect.fintype]
split1 [lemma, in mathcomp.algebra.zmodp]
split1_extraspecial [lemma, in mathcomp.solvable.maximal]
Split2r [constructor, in mathcomp.ssreflect.path]
split2r [inductive, in mathcomp.ssreflect.path]
sP:126 [binder, in mathcomp.ssreflect.choice]
sP:128 [binder, in mathcomp.ssreflect.choice]
sP:141 [binder, in mathcomp.ssreflect.choice]
sP:147 [binder, in mathcomp.ssreflect.choice]
sP:149 [binder, in mathcomp.ssreflect.choice]
sp:173 [binder, in mathcomp.field.closed_field]
sP:19 [binder, in mathcomp.ssreflect.tuple]
sP:20 [binder, in mathcomp.ssreflect.tuple]
sP:227 [binder, in mathcomp.ssreflect.tuple]
sP:234 [binder, in mathcomp.ssreflect.tuple]
sp:279 [binder, in mathcomp.field.closed_field]
sq [abbreviation, in mathcomp.algebra.matrix]
sq [abbreviation, in mathcomp.algebra.matrix]
sq [abbreviation, in mathcomp.algebra.matrix]
sq [abbreviation, in mathcomp.algebra.matrix]
sq [abbreviation, in mathcomp.algebra.matrix]
sqmx_ind [lemma, in mathcomp.algebra.matrix]
sqrCi:85 [binder, in mathcomp.algebra.ssrnum]
sqrnB [lemma, in mathcomp.ssreflect.ssrnat]
sqrnD [lemma, in mathcomp.ssreflect.ssrnat]
sqrnD_sub [lemma, in mathcomp.ssreflect.ssrnat]
sqrn_inj [lemma, in mathcomp.ssreflect.ssrnat]
sqrn_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
sqrt_cfnorm_gt0 [lemma, in mathcomp.character.classfun]
sqrt_cfnorm_eq0 [lemma, in mathcomp.character.classfun]
sqrt_cfnorm_ge0 [lemma, in mathcomp.character.classfun]
sqr_Cint_ge1 [abbreviation, in mathcomp.field.algC]
square [definition, in mathcomp.solvable.burnside_app]
SquareBlockMatrix [section, in mathcomp.algebra.matrix]
SquareBlockMatrixRing [section, in mathcomp.algebra.matrix]
SquareBlockMatrixZmod [section, in mathcomp.algebra.matrix]
\mxdiag_ _ _ (ring_scope) [notation, in mathcomp.algebra.matrix]
square_coloring_number8 [definition, in mathcomp.solvable.burnside_app]
square_coloring_number4 [definition, in mathcomp.solvable.burnside_app]
square_coloring_number2 [definition, in mathcomp.solvable.burnside_app]
sq:122 [binder, in mathcomp.field.closed_field]
sq:136 [binder, in mathcomp.field.closed_field]
sq:153 [binder, in mathcomp.field.closed_field]
sq:162 [binder, in mathcomp.field.closed_field]
sq:172 [binder, in mathcomp.field.closed_field]
sq:3 [binder, in mathcomp.algebra.polydiv]
sr [abbreviation, in mathcomp.character.mxrepresentation]
sr:129 [binder, in mathcomp.field.closed_field]
ssetI [definition, in mathcomp.ssreflect.finset]
ssimS [abbreviation, in mathcomp.character.mxrepresentation]
ssrAC [library]
ssralg [library]
ssrbool [library]
ssreflect [library]
ssrfun [library]
ssrint [library]
ssrmatching [library]
ssrnat [library]
ssrnotations [library]
ssrnum [library]
ssval [projection, in mathcomp.ssreflect.fintype]
ssvalP [projection, in mathcomp.ssreflect.fintype]
ss1:1677 [binder, in mathcomp.ssreflect.seq]
ss1:1706 [binder, in mathcomp.ssreflect.seq]
ss1:1771 [binder, in mathcomp.ssreflect.seq]
ss2:1678 [binder, in mathcomp.ssreflect.seq]
ss2:1707 [binder, in mathcomp.ssreflect.seq]
ss2:1772 [binder, in mathcomp.ssreflect.seq]
ss:1676 [binder, in mathcomp.ssreflect.seq]
ss:1684 [binder, in mathcomp.ssreflect.seq]
ss:1689 [binder, in mathcomp.ssreflect.seq]
ss:1694 [binder, in mathcomp.ssreflect.seq]
ss:1698 [binder, in mathcomp.ssreflect.seq]
ss:1702 [binder, in mathcomp.ssreflect.seq]
ss:1703 [binder, in mathcomp.ssreflect.seq]
ss:1705 [binder, in mathcomp.ssreflect.seq]
ss:1731 [binder, in mathcomp.ssreflect.seq]
ss:1744 [binder, in mathcomp.ssreflect.seq]
ss:1754 [binder, in mathcomp.ssreflect.seq]
sS:233 [binder, in mathcomp.character.mxabelem]
Ss:435 [binder, in mathcomp.algebra.vector]
ss:445 [binder, in mathcomp.ssreflect.path]
ss:449 [binder, in mathcomp.ssreflect.path]
ss:452 [binder, in mathcomp.ssreflect.path]
ss:457 [binder, in mathcomp.ssreflect.path]
ss:469 [binder, in mathcomp.ssreflect.path]
ss:472 [binder, in mathcomp.ssreflect.path]
ss:473 [binder, in mathcomp.ssreflect.path]
ss:566 [binder, in mathcomp.ssreflect.path]
ss:570 [binder, in mathcomp.ssreflect.path]
ss:572 [binder, in mathcomp.ssreflect.path]
sT [abbreviation, in mathcomp.ssreflect.finset]
sT [abbreviation, in mathcomp.fingroup.fingroup]
sT [abbreviation, in mathcomp.ssreflect.fintype]
Stability [section, in mathcomp.algebra.mxalgebra]
Stability_subseq_in.leT [variable, in mathcomp.ssreflect.path]
Stability_subseq_in.T [variable, in mathcomp.ssreflect.path]
Stability_subseq_in [section, in mathcomp.ssreflect.path]
Stability_subseq.leT_tr [variable, in mathcomp.ssreflect.path]
Stability_subseq.leT_total [variable, in mathcomp.ssreflect.path]
Stability_subseq.leT [variable, in mathcomp.ssreflect.path]
Stability_subseq.T [variable, in mathcomp.ssreflect.path]
Stability_subseq [section, in mathcomp.ssreflect.path]
Stability_mask_in.le_sT_tr [variable, in mathcomp.ssreflect.path]
Stability_mask_in.le_sT_total [variable, in mathcomp.ssreflect.path]
Stability_mask_in.le_sT [variable, in mathcomp.ssreflect.path]
Stability_mask_in.leT_tr [variable, in mathcomp.ssreflect.path]
Stability_mask_in.leT_total [variable, in mathcomp.ssreflect.path]
Stability_mask_in.leT [variable, in mathcomp.ssreflect.path]
Stability_mask_in.P [variable, in mathcomp.ssreflect.path]
Stability_mask_in.T [variable, in mathcomp.ssreflect.path]
Stability_mask_in [section, in mathcomp.ssreflect.path]
Stability_mask.leT_tr [variable, in mathcomp.ssreflect.path]
Stability_mask.leT_total [variable, in mathcomp.ssreflect.path]
Stability_mask.leT [variable, in mathcomp.ssreflect.path]
Stability_mask.T [variable, in mathcomp.ssreflect.path]
Stability_mask [section, in mathcomp.ssreflect.path]
Stability_iota.pop_stable [variable, in mathcomp.ssreflect.path]
Stability_iota.push_stable [variable, in mathcomp.ssreflect.path]
Stability_iota.lt_lex [variable, in mathcomp.ssreflect.path]
Stability_iota.leN_total [variable, in mathcomp.ssreflect.path]
Stability_iota.leN [variable, in mathcomp.ssreflect.path]
Stability_iota [section, in mathcomp.ssreflect.path]
Stability.Commutation [section, in mathcomp.algebra.mxalgebra]
Stability.Commutation.n [variable, in mathcomp.algebra.mxalgebra]
Stability.F [variable, in mathcomp.algebra.mxalgebra]
Stability.FixedDim [section, in mathcomp.algebra.mxalgebra]
Stability.FixedDim.f [variable, in mathcomp.algebra.mxalgebra]
Stability.FixedDim.g [variable, in mathcomp.algebra.mxalgebra]
Stability.FixedDim.m [variable, in mathcomp.algebra.mxalgebra]
Stability.FixedDim.n [variable, in mathcomp.algebra.mxalgebra]
Stability.FixedDim.V [variable, in mathcomp.algebra.mxalgebra]
Stability.FixedDim.W [variable, in mathcomp.algebra.mxalgebra]
stable [lemma, in mathcomp.solvable.burnside_app]
stableCmx [lemma, in mathcomp.algebra.mxalgebra]
StableCompositionSeries [section, in mathcomp.solvable.jordanholder]
StableCompositionSeries.A [variable, in mathcomp.solvable.jordanholder]
StableCompositionSeries.aT [variable, in mathcomp.solvable.jordanholder]
StableCompositionSeries.D [variable, in mathcomp.solvable.jordanholder]
StableCompositionSeries.MaxAinvProps [section, in mathcomp.solvable.jordanholder]
StableCompositionSeries.MaxAinvProps.K [variable, in mathcomp.solvable.jordanholder]
StableCompositionSeries.MaxAinvProps.N [variable, in mathcomp.solvable.jordanholder]
StableCompositionSeries.rT [variable, in mathcomp.solvable.jordanholder]
StableCompositionSeries.to [variable, in mathcomp.solvable.jordanholder]
stableDmx [lemma, in mathcomp.algebra.mxalgebra]
stablemx [abbreviation, in mathcomp.algebra.mxalgebra]
stablemx [abbreviation, in mathcomp.algebra.mxalgebra]
stablemxC [lemma, in mathcomp.algebra.mxalgebra]
stablemxD [lemma, in mathcomp.algebra.mxalgebra]
stablemxM [lemma, in mathcomp.algebra.mxalgebra]
stablemxN [lemma, in mathcomp.algebra.mxalgebra]
stablemx_restrict [lemma, in mathcomp.algebra.mxpoly]
stablemx_comp [lemma, in mathcomp.algebra.mxpoly]
stablemx_unit [lemma, in mathcomp.algebra.mxalgebra]
stablemx_sums [lemma, in mathcomp.algebra.mxalgebra]
stablemx_full [lemma, in mathcomp.algebra.mxalgebra]
stablemx_row_base [lemma, in mathcomp.algebra.mxalgebra]
stablemx0 [lemma, in mathcomp.algebra.mxalgebra]
stableNmx [lemma, in mathcomp.algebra.mxalgebra]
stable_rowg_mxK [lemma, in mathcomp.character.mxabelem]
stable_factor [definition, in mathcomp.solvable.gseries]
stable0mx [lemma, in mathcomp.algebra.mxalgebra]
stab_ntransitiveI [lemma, in mathcomp.solvable.primitive_action]
stab_ntransitive [lemma, in mathcomp.solvable.primitive_action]
stab_semiprime [lemma, in mathcomp.solvable.frobenius]
StandardRepresentation [section, in mathcomp.character.character]
StandardRepresentation.DsumRepr [section, in mathcomp.character.character]
StandardRepresentation.DsumRepr.n [variable, in mathcomp.character.character]
StandardRepresentation.DsumRepr.rG [variable, in mathcomp.character.character]
StandardRepresentation.G [variable, in mathcomp.character.character]
StandardRepresentation.gT [variable, in mathcomp.character.character]
StandardRepresentation.ProdRepr [section, in mathcomp.character.character]
StandardRepresentation.ProdRepr.n1 [variable, in mathcomp.character.character]
StandardRepresentation.ProdRepr.n2 [variable, in mathcomp.character.character]
StandardRepresentation.ProdRepr.rG1 [variable, in mathcomp.character.character]
StandardRepresentation.ProdRepr.rG2 [variable, in mathcomp.character.character]
StandardRepresentation.R [variable, in mathcomp.character.character]
standard_grepr [definition, in mathcomp.character.character]
standard_irr_coef [definition, in mathcomp.character.character]
standard_socle [definition, in mathcomp.character.character]
standard_irr [definition, in mathcomp.character.character]
strategy:4 [binder, in mathcomp.ssreflect.ssrAC]
strict_adjunction [lemma, in mathcomp.ssreflect.fingraph]
strongest_coprime_quotient_cent [lemma, in mathcomp.solvable.hall]
StrongJordanHolder [section, in mathcomp.solvable.jordanholder]
StrongJordanHolderUniqueness [lemma, in mathcomp.solvable.jordanholder]
StrongJordanHolder.A [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.aT [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.AuxiliaryLemmas [section, in mathcomp.solvable.jordanholder]
StrongJordanHolder.AuxiliaryLemmas.A [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.AuxiliaryLemmas.aT [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.AuxiliaryLemmas.D [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.AuxiliaryLemmas.rT [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.AuxiliaryLemmas.to [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.D [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.rT [variable, in mathcomp.solvable.jordanholder]
StrongJordanHolder.to [variable, in mathcomp.solvable.jordanholder]
strong_Primitive_Element_Theorem [lemma, in mathcomp.field.separable]
sT:10 [binder, in mathcomp.field.algebraics_fundamentals]
sT:156 [binder, in mathcomp.solvable.frobenius]
sT:177 [binder, in mathcomp.ssreflect.choice]
sT:20 [binder, in mathcomp.ssreflect.ssrfun]
sT:200 [binder, in mathcomp.ssreflect.choice]
sT:203 [binder, in mathcomp.ssreflect.choice]
sT:207 [binder, in mathcomp.ssreflect.choice]
sT:211 [binder, in mathcomp.ssreflect.choice]
sT:215 [binder, in mathcomp.ssreflect.choice]
sT:220 [binder, in mathcomp.ssreflect.choice]
st:2242 [binder, in mathcomp.ssreflect.seq]
sT:225 [binder, in mathcomp.ssreflect.choice]
st:2426 [binder, in mathcomp.ssreflect.seq]
sT:25 [binder, in mathcomp.ssreflect.ssrfun]
sT:266 [binder, in mathcomp.ssreflect.eqtype]
sT:31 [binder, in mathcomp.ssreflect.ssrfun]
sT:363 [binder, in mathcomp.ssreflect.eqtype]
sT:366 [binder, in mathcomp.ssreflect.eqtype]
sT:37 [binder, in mathcomp.solvable.frobenius]
sT:37 [binder, in mathcomp.ssreflect.ssrfun]
sT:376 [binder, in mathcomp.ssreflect.eqtype]
sT:3950 [binder, in mathcomp.ssreflect.order]
sT:4 [binder, in mathcomp.solvable.burnside_app]
sT:719 [binder, in mathcomp.ssreflect.fintype]
sT:723 [binder, in mathcomp.ssreflect.fintype]
sT:727 [binder, in mathcomp.ssreflect.fintype]
sT:733 [binder, in mathcomp.ssreflect.fintype]
sT:741 [binder, in mathcomp.ssreflect.fintype]
Sub [abbreviation, in mathcomp.ssreflect.eqtype]
sub [abbreviation, in mathcomp.ssreflect.eqtype]
subact [definition, in mathcomp.fingroup.action]
subaction [definition, in mathcomp.fingroup.action]
SubAction [section, in mathcomp.fingroup.action]
SubAction.aT [variable, in mathcomp.fingroup.action]
SubAction.D [variable, in mathcomp.fingroup.action]
SubAction.rT [variable, in mathcomp.fingroup.action]
SubAction.sP [variable, in mathcomp.fingroup.action]
SubAction.sT [variable, in mathcomp.fingroup.action]
SubAction.to [variable, in mathcomp.fingroup.action]
subact_is_action [lemma, in mathcomp.fingroup.action]
subact_dom_group [definition, in mathcomp.fingroup.action]
subact_dom [definition, in mathcomp.fingroup.action]
subalg_closed_subproof:2753 [binder, in mathcomp.algebra.ssralg]
subalg_closed_subproof:2736 [binder, in mathcomp.algebra.ssralg]
subalg_closed_subproof:2201 [binder, in mathcomp.algebra.ssralg]
subBnAC [lemma, in mathcomp.ssreflect.ssrnat]
subcentP [lemma, in mathcomp.solvable.center]
subcent_dprod [lemma, in mathcomp.fingroup.gproduct]
subcent_sdprod [lemma, in mathcomp.fingroup.gproduct]
subcent_TImulg [lemma, in mathcomp.fingroup.gproduct]
subcent_char [lemma, in mathcomp.solvable.center]
subcent_normal [lemma, in mathcomp.solvable.center]
subcent_norm [lemma, in mathcomp.solvable.center]
subcent_sub [lemma, in mathcomp.solvable.center]
subcent1C [lemma, in mathcomp.solvable.center]
subcent1P [lemma, in mathcomp.solvable.center]
subcent1_cycle_normal [lemma, in mathcomp.solvable.center]
subcent1_cycle_norm [lemma, in mathcomp.solvable.center]
subcent1_cycle_sub [lemma, in mathcomp.solvable.center]
subcent1_sub [lemma, in mathcomp.solvable.center]
subcent1_id [lemma, in mathcomp.solvable.center]
subcent1_extraspecial_maximal [lemma, in mathcomp.solvable.maximal]
SubCountable_isFiniteTheory.sfT [variable, in mathcomp.ssreflect.fintype]
SubCountable_isFiniteTheory.P [variable, in mathcomp.ssreflect.fintype]
SubCountable_isFiniteTheory.T [variable, in mathcomp.ssreflect.fintype]
SubCountable_isFiniteTheory [section, in mathcomp.ssreflect.fintype]
subCset [lemma, in mathcomp.ssreflect.finset]
SubDaddsmxSpec [constructor, in mathcomp.algebra.mxalgebra]
subDnAC [lemma, in mathcomp.ssreflect.ssrnat]
subDnCA [lemma, in mathcomp.ssreflect.ssrnat]
subDnCAC [lemma, in mathcomp.ssreflect.ssrnat]
subdom [abbreviation, in mathcomp.fingroup.action]
subDset [lemma, in mathcomp.ssreflect.finset]
SubDsumsmxSpec [constructor, in mathcomp.algebra.mxalgebra]
subD1set [lemma, in mathcomp.ssreflect.finset]
subEproper [lemma, in mathcomp.ssreflect.finset]
SubEqType [section, in mathcomp.ssreflect.eqtype]
SubEqType.P [variable, in mathcomp.ssreflect.eqtype]
SubEqType.sT [variable, in mathcomp.ssreflect.eqtype]
SubEqType.T [variable, in mathcomp.ssreflect.eqtype]
SubFalgType [section, in mathcomp.field.falgebra]
SubFalgType.A [variable, in mathcomp.field.falgebra]
SubFalgType.aT [variable, in mathcomp.field.falgebra]
SubFalgType.K [variable, in mathcomp.field.falgebra]
subFExtend [definition, in mathcomp.field.fieldext]
subfext_inv [definition, in mathcomp.field.fieldext]
subfext_mul [definition, in mathcomp.field.fieldext]
subfext_opp [definition, in mathcomp.field.fieldext]
subfext_add [definition, in mathcomp.field.fieldext]
subfext0 [definition, in mathcomp.field.fieldext]
subfext0_morph [definition, in mathcomp.field.fieldext]
subfext1 [definition, in mathcomp.field.fieldext]
subfext1_morph [definition, in mathcomp.field.fieldext]
SubFieldExtension [section, in mathcomp.field.fieldext]
SubFieldExtension.F [variable, in mathcomp.field.fieldext]
SubFieldExtension.iota [variable, in mathcomp.field.fieldext]
SubFieldExtension.iotaFz [variable, in mathcomp.field.fieldext]
SubFieldExtension.iotaPz_modp [variable, in mathcomp.field.fieldext]
SubFieldExtension.iotaPz_repr [variable, in mathcomp.field.fieldext]
SubFieldExtension.Irreducible [section, in mathcomp.field.fieldext]
SubFieldExtension.Irreducible.irr_p [variable, in mathcomp.field.fieldext]
SubFieldExtension.Irreducible.nz_p [variable, in mathcomp.field.fieldext]
SubFieldExtension.L [variable, in mathcomp.field.fieldext]
SubFieldExtension.n [variable, in mathcomp.field.fieldext]
SubFieldExtension.NonZero [section, in mathcomp.field.fieldext]
SubFieldExtension.NonZero.nz_p [variable, in mathcomp.field.fieldext]
SubFieldExtension.nz_p0 [variable, in mathcomp.field.fieldext]
SubFieldExtension.n_gt0 [variable, in mathcomp.field.fieldext]
SubFieldExtension.p [variable, in mathcomp.field.fieldext]
SubFieldExtension.poly_rV_modp_K [variable, in mathcomp.field.fieldext]
SubFieldExtension.pz0 [variable, in mathcomp.field.fieldext]
SubFieldExtension.p0 [variable, in mathcomp.field.fieldext]
SubFieldExtension.p0z0 [variable, in mathcomp.field.fieldext]
SubFieldExtension.p0_mon [variable, in mathcomp.field.fieldext]
SubFieldExtension.subfx_poly_invE [variable, in mathcomp.field.fieldext]
SubFieldExtension.wf_p [variable, in mathcomp.field.fieldext]
SubFieldExtension.z [variable, in mathcomp.field.fieldext]
SubFieldExtension.z0 [variable, in mathcomp.field.fieldext]
SubFieldExtension.z0Ciota [variable, in mathcomp.field.fieldext]
_ ^iota (ring_scope) [notation, in mathcomp.field.fieldext]
SubFieldExtType [definition, in mathcomp.field.fieldext]
subfield_closed [lemma, in mathcomp.field.fieldext]
subfield_subproof:2653 [binder, in mathcomp.algebra.ssralg]
SubFinType [section, in mathcomp.ssreflect.fintype]
SubFinType.P [variable, in mathcomp.ssreflect.fintype]
SubFinType.T [variable, in mathcomp.ssreflect.fintype]
subfxE [lemma, in mathcomp.field.fieldext]
subfxEroot [lemma, in mathcomp.field.fieldext]
SubfxVect [definition, in mathcomp.field.fieldext]
subfx_irreducibleP [lemma, in mathcomp.field.fieldext]
subfx_inj_base [lemma, in mathcomp.field.fieldext]
subfx_injZ [lemma, in mathcomp.field.fieldext]
subfx_inj_root [lemma, in mathcomp.field.fieldext]
subfx_inj_eval [lemma, in mathcomp.field.fieldext]
subfx_evalZ [lemma, in mathcomp.field.fieldext]
subfx_scaleAr [lemma, in mathcomp.field.fieldext]
subfx_scaleAl [lemma, in mathcomp.field.fieldext]
subfx_scalerDl [lemma, in mathcomp.field.fieldext]
subfx_scalerDr [lemma, in mathcomp.field.fieldext]
subfx_scaler1r [lemma, in mathcomp.field.fieldext]
subfx_scalerA [lemma, in mathcomp.field.fieldext]
subfx_scale [definition, in mathcomp.field.fieldext]
subfx_eval_is_multiplicative [lemma, in mathcomp.field.fieldext]
subfx_eval_is_additive [lemma, in mathcomp.field.fieldext]
subfx_root [definition, in mathcomp.field.fieldext]
subfx_eval_morph [definition, in mathcomp.field.fieldext]
subfx_eval [definition, in mathcomp.field.fieldext]
subfx_inj_is_multiplicative [lemma, in mathcomp.field.fieldext]
subfx_inj_is_additive [lemma, in mathcomp.field.fieldext]
subfx_inv0 [lemma, in mathcomp.field.fieldext]
subfx_fieldAxiom [lemma, in mathcomp.field.fieldext]
subfx_inv_rep [definition, in mathcomp.field.fieldext]
subfx_poly_inv [definition, in mathcomp.field.fieldext]
subfx_mul_rep [definition, in mathcomp.field.fieldext]
subfx_inj [definition, in mathcomp.field.fieldext]
subg [definition, in mathcomp.fingroup.fingroup]
Subg [constructor, in mathcomp.fingroup.fingroup]
subgacentE [lemma, in mathcomp.fingroup.action]
subgacent1E [lemma, in mathcomp.fingroup.action]
subGcfker [lemma, in mathcomp.character.character]
subgK [lemma, in mathcomp.fingroup.fingroup]
subgM [lemma, in mathcomp.fingroup.fingroup]
subgmK [lemma, in mathcomp.fingroup.morphism]
subgP [lemma, in mathcomp.fingroup.fingroup]
subgroups [definition, in mathcomp.fingroup.fingroup]
subgroup_transitiveP [lemma, in mathcomp.fingroup.action]
subgroup_transitivePin [lemma, in mathcomp.fingroup.action]
subg_default [lemma, in mathcomp.fingroup.fingroup]
subg_mulP [lemma, in mathcomp.fingroup.fingroup]
subg_invP [lemma, in mathcomp.fingroup.fingroup]
subg_oneP [lemma, in mathcomp.fingroup.fingroup]
subg_mul [definition, in mathcomp.fingroup.fingroup]
subg_inv [definition, in mathcomp.fingroup.fingroup]
subg_one [definition, in mathcomp.fingroup.fingroup]
subg_inj [lemma, in mathcomp.fingroup.fingroup]
subg_of_Sub [definition, in mathcomp.fingroup.fingroup]
subg_of [inductive, in mathcomp.fingroup.fingroup]
subg_mx_abs_irr [lemma, in mathcomp.character.mxrepresentation]
subg_mx_irr [lemma, in mathcomp.character.mxrepresentation]
subg_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
subg_repr [definition, in mathcomp.character.mxrepresentation]
subg_mx_repr [lemma, in mathcomp.character.mxrepresentation]
subg_morphism [definition, in mathcomp.fingroup.morphism]
subG1 [lemma, in mathcomp.fingroup.fingroup]
subG1_contra [lemma, in mathcomp.fingroup.fingroup]
subHall_Sylow [lemma, in mathcomp.solvable.pgroup]
subHall_Hall [lemma, in mathcomp.solvable.pgroup]
subIset [lemma, in mathcomp.ssreflect.finset]
subitv [definition, in mathcomp.algebra.interval]
subitvE [lemma, in mathcomp.algebra.interval]
subitvP [lemma, in mathcomp.algebra.interval]
subitvPl [lemma, in mathcomp.algebra.interval]
subitvPr [lemma, in mathcomp.algebra.interval]
subitv_trans [lemma, in mathcomp.algebra.interval]
subitv_anti [lemma, in mathcomp.algebra.interval]
subitv_refl [lemma, in mathcomp.algebra.interval]
subK [abbreviation, in mathcomp.ssreflect.eqtype]
SubK [lemma, in mathcomp.ssreflect.eqtype]
subKn [lemma, in mathcomp.ssreflect.ssrnat]
SubK_subproof:256 [binder, in mathcomp.ssreflect.eqtype]
submod_mx_irr [lemma, in mathcomp.character.mxrepresentation]
submod_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
submod_repr [definition, in mathcomp.character.mxrepresentation]
submod_mx_repr [lemma, in mathcomp.character.mxrepresentation]
submod_mx [definition, in mathcomp.character.mxrepresentation]
submod_closed_subproof:2719 [binder, in mathcomp.algebra.ssralg]
submod_closed_subproof:2526 [binder, in mathcomp.algebra.ssralg]
submod_closed_subproof:2188 [binder, in mathcomp.algebra.ssralg]
SubMorphism [section, in mathcomp.fingroup.morphism]
SubMorphism.G [variable, in mathcomp.fingroup.morphism]
SubMorphism.gT [variable, in mathcomp.fingroup.morphism]
submxblock [definition, in mathcomp.algebra.matrix]
submxblockB [lemma, in mathcomp.algebra.matrix]
submxblockD [lemma, in mathcomp.algebra.matrix]
submxblockEh [lemma, in mathcomp.algebra.matrix]
submxblockEv [lemma, in mathcomp.algebra.matrix]
submxblockK [lemma, in mathcomp.algebra.matrix]
submxblockN [lemma, in mathcomp.algebra.matrix]
submxblock_diag [lemma, in mathcomp.algebra.matrix]
submxblock_sum [lemma, in mathcomp.algebra.matrix]
submxblock0 [lemma, in mathcomp.algebra.matrix]
submxcol [definition, in mathcomp.algebra.matrix]
submxcolB [lemma, in mathcomp.algebra.matrix]
submxcolD [lemma, in mathcomp.algebra.matrix]
submxcolK [lemma, in mathcomp.algebra.matrix]
submxcolN [lemma, in mathcomp.algebra.matrix]
submxcol_mul [lemma, in mathcomp.algebra.matrix]
submxcol_sum [lemma, in mathcomp.algebra.matrix]
submxcol_matrix [lemma, in mathcomp.algebra.matrix]
submxcol0 [lemma, in mathcomp.algebra.matrix]
submxE [lemma, in mathcomp.algebra.mxalgebra]
submxElt [lemma, in mathcomp.algebra.mxalgebra]
submxK [lemma, in mathcomp.algebra.matrix]
submxMfree [lemma, in mathcomp.algebra.mxalgebra]
submxMl [lemma, in mathcomp.algebra.mxalgebra]
submxMr [lemma, in mathcomp.algebra.mxalgebra]
submxP [lemma, in mathcomp.algebra.mxalgebra]
submxrow [definition, in mathcomp.algebra.matrix]
submxrowB [lemma, in mathcomp.algebra.matrix]
submxrowD [lemma, in mathcomp.algebra.matrix]
submxrowK [lemma, in mathcomp.algebra.matrix]
submxrowN [lemma, in mathcomp.algebra.matrix]
submxrow_sum [lemma, in mathcomp.algebra.matrix]
submxrow_matrix [lemma, in mathcomp.algebra.matrix]
submxrow0 [lemma, in mathcomp.algebra.matrix]
submx_rowsub [lemma, in mathcomp.algebra.mxalgebra]
submx_full [lemma, in mathcomp.algebra.mxalgebra]
submx_trans [lemma, in mathcomp.algebra.mxalgebra]
submx_refl [lemma, in mathcomp.algebra.mxalgebra]
submx_unlockable [definition, in mathcomp.algebra.mxalgebra]
submx0 [lemma, in mathcomp.algebra.mxalgebra]
submx0null [lemma, in mathcomp.algebra.mxalgebra]
submx1 [lemma, in mathcomp.algebra.mxalgebra]
subn [definition, in mathcomp.ssreflect.ssrnat]
subnA [lemma, in mathcomp.ssreflect.ssrnat]
subnAC [lemma, in mathcomp.ssreflect.ssrnat]
subnBA [lemma, in mathcomp.ssreflect.ssrnat]
subnBAC [lemma, in mathcomp.ssreflect.ssrnat]
subnBl_leq [lemma, in mathcomp.ssreflect.ssrnat]
subnBr_leq [lemma, in mathcomp.ssreflect.ssrnat]
subnCBA [lemma, in mathcomp.ssreflect.ssrnat]
subnDA [lemma, in mathcomp.ssreflect.ssrnat]
subnDAC [lemma, in mathcomp.ssreflect.ssrnat]
subnDl [lemma, in mathcomp.ssreflect.ssrnat]
subnDr [lemma, in mathcomp.ssreflect.ssrnat]
subnE [lemma, in mathcomp.ssreflect.ssrnat]
subnK [lemma, in mathcomp.ssreflect.ssrnat]
subnKC [lemma, in mathcomp.ssreflect.ssrnat]
subnn [lemma, in mathcomp.ssreflect.ssrnat]
Subnormal [section, in mathcomp.solvable.gseries]
subnormal [definition, in mathcomp.solvable.gseries]
subnormalEl [lemma, in mathcomp.solvable.gseries]
subnormalEr [lemma, in mathcomp.solvable.gseries]
subnormalEsupport [lemma, in mathcomp.solvable.gseries]
subnormalP [lemma, in mathcomp.solvable.gseries]
subnormal_sub [lemma, in mathcomp.solvable.gseries]
subnormal_trans [lemma, in mathcomp.solvable.gseries]
subnormal_refl [lemma, in mathcomp.solvable.gseries]
Subnormal.gT [variable, in mathcomp.solvable.gseries]
Subnormal.path_setIgr [variable, in mathcomp.solvable.gseries]
Subnormal.setIgr [variable, in mathcomp.solvable.gseries]
Subnormal.sub_setIgr [variable, in mathcomp.solvable.gseries]
subnS [lemma, in mathcomp.ssreflect.ssrnat]
subnSK [lemma, in mathcomp.ssreflect.ssrnat]
subn_exp [lemma, in mathcomp.ssreflect.binomial]
subn_sqr [lemma, in mathcomp.ssreflect.ssrnat]
subn_if_gt [lemma, in mathcomp.ssreflect.ssrnat]
subn_minl [lemma, in mathcomp.ssreflect.ssrnat]
subn_maxl [lemma, in mathcomp.ssreflect.ssrnat]
subn_eq0 [lemma, in mathcomp.ssreflect.ssrnat]
subn_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
subn_rec [definition, in mathcomp.ssreflect.ssrnat]
subn0 [lemma, in mathcomp.ssreflect.ssrnat]
subn1 [lemma, in mathcomp.ssreflect.ssrnat]
subn2 [lemma, in mathcomp.ssreflect.ssrnat]
subP [abbreviation, in mathcomp.ssreflect.eqtype]
SubP [lemma, in mathcomp.ssreflect.eqtype]
subq [definition, in mathcomp.algebra.rat]
subq_ge0 [lemma, in mathcomp.algebra.rat]
subring_closed_subproof:2705 [binder, in mathcomp.algebra.ssralg]
subring_closed_subproof:2692 [binder, in mathcomp.algebra.ssralg]
subring_closed_subproof:2474 [binder, in mathcomp.algebra.ssralg]
subring_closed_subproof:2160 [binder, in mathcomp.algebra.ssralg]
subseq [definition, in mathcomp.ssreflect.seq]
Subseq [section, in mathcomp.ssreflect.seq]
subseqP [lemma, in mathcomp.ssreflect.seq]
subseq_pairwise [lemma, in mathcomp.ssreflect.seq]
subseq_rem [lemma, in mathcomp.ssreflect.seq]
subseq_uniqP [lemma, in mathcomp.ssreflect.seq]
subseq_filter [lemma, in mathcomp.ssreflect.seq]
subseq_rot [lemma, in mathcomp.ssreflect.seq]
subseq_cat2r [lemma, in mathcomp.ssreflect.seq]
subseq_cat2l [lemma, in mathcomp.ssreflect.seq]
subseq_rev [lemma, in mathcomp.ssreflect.seq]
subseq_uniq [lemma, in mathcomp.ssreflect.seq]
subseq_rcons [lemma, in mathcomp.ssreflect.seq]
subseq_cons [lemma, in mathcomp.ssreflect.seq]
subseq_anti [lemma, in mathcomp.ssreflect.seq]
subseq_trans [lemma, in mathcomp.ssreflect.seq]
subseq_refl [lemma, in mathcomp.ssreflect.seq]
subseq_sort_in [lemma, in mathcomp.ssreflect.path]
subseq_sort [lemma, in mathcomp.ssreflect.path]
subseq_sorted [lemma, in mathcomp.ssreflect.path]
subseq_path [lemma, in mathcomp.ssreflect.path]
subseq_sorted_in [lemma, in mathcomp.ssreflect.path]
subseq_path_in [lemma, in mathcomp.ssreflect.path]
Subseq.T [variable, in mathcomp.ssreflect.seq]
subseq0 [lemma, in mathcomp.ssreflect.seq]
subseries_repr [definition, in mathcomp.character.mxrepresentation]
subsetC [lemma, in mathcomp.ssreflect.finset]
subsetD [lemma, in mathcomp.ssreflect.finset]
subsetDl [lemma, in mathcomp.ssreflect.finset]
subsetDP [lemma, in mathcomp.ssreflect.finset]
subsetDr [lemma, in mathcomp.ssreflect.finset]
subsetD1 [lemma, in mathcomp.ssreflect.finset]
subsetD1P [lemma, in mathcomp.ssreflect.finset]
subsetE [lemma, in mathcomp.ssreflect.fintype]
subsetI [lemma, in mathcomp.ssreflect.finset]
subsetIidl [lemma, in mathcomp.ssreflect.finset]
subsetIidr [lemma, in mathcomp.ssreflect.finset]
subsetIl [lemma, in mathcomp.ssreflect.finset]
subsetIP [lemma, in mathcomp.ssreflect.finset]
subsetIr [lemma, in mathcomp.ssreflect.finset]
subsetP [lemma, in mathcomp.ssreflect.fintype]
subsetPn [lemma, in mathcomp.ssreflect.fintype]
subsets_disjoint [lemma, in mathcomp.ssreflect.finset]
subsetT [lemma, in mathcomp.ssreflect.finset]
subsetT_hint [lemma, in mathcomp.ssreflect.finset]
subsetU [lemma, in mathcomp.ssreflect.finset]
subsetUl [lemma, in mathcomp.ssreflect.finset]
subsetUr [lemma, in mathcomp.ssreflect.finset]
subsetU1 [lemma, in mathcomp.ssreflect.finset]
subsetv [definition, in mathcomp.algebra.vector]
subset_itv_co_cc [lemma, in mathcomp.algebra.interval]
subset_itv_oc_cc [lemma, in mathcomp.algebra.interval]
subset_itv_oo_co [lemma, in mathcomp.algebra.interval]
subset_itv_oo_oc [lemma, in mathcomp.algebra.interval]
subset_itv_oo_cc [lemma, in mathcomp.algebra.interval]
subset_itv [lemma, in mathcomp.algebra.interval]
subset_mapP [lemma, in mathcomp.ssreflect.seq]
subset_iter [lemma, in mathcomp.ssreflect.finset]
subset_iterS [lemma, in mathcomp.ssreflect.finset]
subset_le_big_cond [lemma, in mathcomp.ssreflect.finset]
subset_neq0 [lemma, in mathcomp.ssreflect.finset]
subset_leqif_cards [lemma, in mathcomp.ssreflect.finset]
subset_faithful [lemma, in mathcomp.fingroup.action]
subset_gen [lemma, in mathcomp.fingroup.fingroup]
subset_closure [lemma, in mathcomp.ssreflect.fingraph]
subset_dfs [lemma, in mathcomp.ssreflect.fingraph]
subset_disjoint [lemma, in mathcomp.ssreflect.fintype]
subset_filter [lemma, in mathcomp.ssreflect.fintype]
subset_cat2 [lemma, in mathcomp.ssreflect.fintype]
subset_catr [lemma, in mathcomp.ssreflect.fintype]
subset_catl [lemma, in mathcomp.ssreflect.fintype]
subset_cons2 [lemma, in mathcomp.ssreflect.fintype]
subset_cons [lemma, in mathcomp.ssreflect.fintype]
subset_all [lemma, in mathcomp.ssreflect.fintype]
subset_trans [lemma, in mathcomp.ssreflect.fintype]
subset_leqif_card [lemma, in mathcomp.ssreflect.fintype]
subset_cardP [lemma, in mathcomp.ssreflect.fintype]
subset_eqP [lemma, in mathcomp.ssreflect.fintype]
subset_pred1 [lemma, in mathcomp.ssreflect.fintype]
subset_predT [lemma, in mathcomp.ssreflect.fintype]
subset_leq_card [lemma, in mathcomp.ssreflect.fintype]
subset_unlock [definition, in mathcomp.ssreflect.fintype]
subset_le_big [lemma, in mathcomp.ssreflect.bigop]
subset0 [lemma, in mathcomp.ssreflect.finset]
subset1 [lemma, in mathcomp.ssreflect.finset]
subSKn [lemma, in mathcomp.ssreflect.ssrnat]
subSn [lemma, in mathcomp.ssreflect.ssrnat]
subSnn [lemma, in mathcomp.ssreflect.ssrnat]
subSocle_direct [lemma, in mathcomp.character.mxrepresentation]
subSocle_iso [lemma, in mathcomp.character.mxrepresentation]
subSocle_semisimple [lemma, in mathcomp.character.mxrepresentation]
subSocle_module [lemma, in mathcomp.character.mxrepresentation]
subSpec [constructor, in mathcomp.ssreflect.eqtype]
subSS [lemma, in mathcomp.ssreflect.ssrnat]
subTset [lemma, in mathcomp.ssreflect.finset]
SubType [section, in mathcomp.ssreflect.eqtype]
SubType.P [variable, in mathcomp.ssreflect.eqtype]
SubType.T [variable, in mathcomp.ssreflect.eqtype]
SubType.Theory [section, in mathcomp.ssreflect.eqtype]
SubType.Theory.insub_eq_aux [variable, in mathcomp.ssreflect.eqtype]
SubType.Theory.sT [variable, in mathcomp.ssreflect.eqtype]
subUset [lemma, in mathcomp.ssreflect.finset]
subUsetP [lemma, in mathcomp.ssreflect.finset]
subV [abbreviation, in mathcomp.algebra.vector]
SubVector [section, in mathcomp.algebra.vector]
SubVector.K [variable, in mathcomp.algebra.vector]
SubVector.U [variable, in mathcomp.algebra.vector]
SubVector.vT [variable, in mathcomp.algebra.vector]
subvf [lemma, in mathcomp.algebra.vector]
subvP [lemma, in mathcomp.algebra.vector]
subvPn [lemma, in mathcomp.algebra.vector]
subvP_adjoin [lemma, in mathcomp.field.falgebra]
Subvs [constructor, in mathcomp.algebra.vector]
subvsP [lemma, in mathcomp.algebra.vector]
subvs_fieldMixin [lemma, in mathcomp.field.fieldext]
subvs_vect_iso [lemma, in mathcomp.algebra.vector]
subvs_inj [lemma, in mathcomp.algebra.vector]
subvs_of [inductive, in mathcomp.algebra.vector]
subvs_scaleAr [lemma, in mathcomp.field.falgebra]
subvs_scaleAl [lemma, in mathcomp.field.falgebra]
subvs_mulDr [lemma, in mathcomp.field.falgebra]
subvs_mulDl [lemma, in mathcomp.field.falgebra]
subvs_mul1 [lemma, in mathcomp.field.falgebra]
subvs_mu1l [lemma, in mathcomp.field.falgebra]
subvs_mulA [lemma, in mathcomp.field.falgebra]
subvs_mul [definition, in mathcomp.field.falgebra]
subvs_one [definition, in mathcomp.field.falgebra]
subvv [lemma, in mathcomp.algebra.vector]
subv_bigcapP [lemma, in mathcomp.algebra.vector]
subv_cap [lemma, in mathcomp.algebra.vector]
subv_sumP [lemma, in mathcomp.algebra.vector]
subv_add [lemma, in mathcomp.algebra.vector]
subv_anti [lemma, in mathcomp.algebra.vector]
subv_trans [lemma, in mathcomp.algebra.vector]
subv_adjoin_seq [lemma, in mathcomp.field.falgebra]
subv_adjoin [lemma, in mathcomp.field.falgebra]
subv_cent1 [lemma, in mathcomp.field.falgebra]
subv0 [lemma, in mathcomp.algebra.vector]
subxx [lemma, in mathcomp.ssreflect.fintype]
subxx_hint [lemma, in mathcomp.ssreflect.fintype]
subX_agenv [lemma, in mathcomp.field.falgebra]
subzn [lemma, in mathcomp.algebra.ssrint]
subzSS [lemma, in mathcomp.algebra.ssrint]
sub_cosetpre_quo [lemma, in mathcomp.fingroup.quotient]
sub_quotient_pre [lemma, in mathcomp.fingroup.quotient]
sub_cosetpre [lemma, in mathcomp.fingroup.quotient]
sub_im_coset [lemma, in mathcomp.fingroup.quotient]
sub_conjC_vchar [lemma, in mathcomp.character.vcharacter]
sub_aut_zchar [lemma, in mathcomp.character.vcharacter]
sub_pairwise [lemma, in mathcomp.ssreflect.seq]
sub_in_pairwise [lemma, in mathcomp.ssreflect.seq]
sub_allrel [lemma, in mathcomp.ssreflect.seq]
sub_in_allrel [lemma, in mathcomp.ssreflect.seq]
sub_map [lemma, in mathcomp.ssreflect.seq]
sub_all [lemma, in mathcomp.ssreflect.seq]
sub_count [lemma, in mathcomp.ssreflect.seq]
sub_has [lemma, in mathcomp.ssreflect.seq]
sub_find [lemma, in mathcomp.ssreflect.seq]
sub_der1_abelian [lemma, in mathcomp.solvable.commutator]
sub_der1_normal [lemma, in mathcomp.solvable.commutator]
sub_der1_norm [lemma, in mathcomp.solvable.commutator]
sub_Zp_1 [lemma, in mathcomp.algebra.zmodp]
sub_imset_pre [lemma, in mathcomp.ssreflect.finset]
sub_baseField [lemma, in mathcomp.field.fieldext]
sub_adjoin1v [lemma, in mathcomp.field.fieldext]
sub_adjoin_separable_generator [lemma, in mathcomp.field.separable]
sub_inseparable [lemma, in mathcomp.field.separable]
sub_eigenspace_conjmx [lemma, in mathcomp.algebra.mxpoly]
sub_kermxpoly_conjmx [lemma, in mathcomp.algebra.mxpoly]
sub_inertia_Ind [lemma, in mathcomp.character.inertia]
sub_inertia_Res [lemma, in mathcomp.character.inertia]
sub_Inertia [lemma, in mathcomp.character.inertia]
sub_inertia [lemma, in mathcomp.character.inertia]
sub_astabQR [lemma, in mathcomp.fingroup.action]
sub_astabQ [lemma, in mathcomp.fingroup.action]
sub_afixRs_norm [lemma, in mathcomp.fingroup.action]
sub_afixRs_norms [lemma, in mathcomp.fingroup.action]
sub_act_proof [lemma, in mathcomp.fingroup.action]
sub_astab1 [lemma, in mathcomp.fingroup.action]
sub_astab1_in [lemma, in mathcomp.fingroup.action]
sub_cfker_mod [lemma, in mathcomp.character.classfun]
sub_morphim_cfker [lemma, in mathcomp.character.classfun]
sub_cfker_morph [lemma, in mathcomp.character.classfun]
sub_cfker_Res [lemma, in mathcomp.character.classfun]
sub_iso_to [lemma, in mathcomp.character.classfun]
sub_orthonormal [lemma, in mathcomp.character.classfun]
sub_pairwise_orthogonal [lemma, in mathcomp.character.classfun]
sub_abelem_rV_im [lemma, in mathcomp.character.mxabelem]
sub_rVabelem_im [lemma, in mathcomp.character.mxabelem]
sub_rVabelem [lemma, in mathcomp.character.mxabelem]
sub_im_abelem_rV [lemma, in mathcomp.character.mxabelem]
sub_rowg_mx [lemma, in mathcomp.character.mxabelem]
sub_abelian_normal [lemma, in mathcomp.fingroup.fingroup]
sub_abelian_norm [lemma, in mathcomp.fingroup.fingroup]
sub_abelian_cent2 [lemma, in mathcomp.fingroup.fingroup]
sub_abelian_cent [lemma, in mathcomp.fingroup.fingroup]
sub_cent1 [lemma, in mathcomp.fingroup.fingroup]
sub_gcore [lemma, in mathcomp.fingroup.fingroup]
sub_gen [lemma, in mathcomp.fingroup.fingroup]
sub_class_support [lemma, in mathcomp.fingroup.fingroup]
sub_conjgV [lemma, in mathcomp.fingroup.fingroup]
sub_conjg [lemma, in mathcomp.fingroup.fingroup]
sub_rcosetV [lemma, in mathcomp.fingroup.fingroup]
sub_rcoset [lemma, in mathcomp.fingroup.fingroup]
sub_lcosetV [lemma, in mathcomp.fingroup.fingroup]
sub_lcoset [lemma, in mathcomp.fingroup.fingroup]
sub_nilpotent_cent2 [lemma, in mathcomp.solvable.sylow]
sub_pcore [lemma, in mathcomp.solvable.pgroup]
sub_in_pcore [lemma, in mathcomp.solvable.pgroup]
sub_Hall_pcore [lemma, in mathcomp.solvable.pgroup]
sub_normal_Hall [lemma, in mathcomp.solvable.pgroup]
sub_pHall [lemma, in mathcomp.solvable.pgroup]
sub_in_constt [lemma, in mathcomp.solvable.pgroup]
sub_p_elt [lemma, in mathcomp.solvable.pgroup]
sub_pgroup [lemma, in mathcomp.solvable.pgroup]
sub_sorted [lemma, in mathcomp.ssreflect.path]
sub_cycle [lemma, in mathcomp.ssreflect.path]
sub_path [lemma, in mathcomp.ssreflect.path]
sub_in_sorted [lemma, in mathcomp.ssreflect.path]
sub_in_cycle [lemma, in mathcomp.ssreflect.path]
sub_in_path [lemma, in mathcomp.ssreflect.path]
sub_pnat_coprime [lemma, in mathcomp.ssreflect.prime]
sub_in_pnat [lemma, in mathcomp.ssreflect.prime]
sub_in_partn [lemma, in mathcomp.ssreflect.prime]
sub_annihilant_neq0 [lemma, in mathcomp.algebra.polyXY]
sub_annihilantP [lemma, in mathcomp.algebra.polyXY]
sub_annihilant_in_ideal [lemma, in mathcomp.algebra.polyXY]
sub_annihilant [definition, in mathcomp.algebra.polyXY]
sub_Ldiv [lemma, in mathcomp.solvable.abelian]
sub_LdivT [lemma, in mathcomp.solvable.abelian]
sub_gt0:2589 [binder, in mathcomp.algebra.ssrnum]
sub_ge0:2549 [binder, in mathcomp.algebra.ssrnum]
sub_isog [lemma, in mathcomp.fingroup.morphism]
sub_isom [lemma, in mathcomp.fingroup.morphism]
sub_morphpre_injm [lemma, in mathcomp.fingroup.morphism]
sub_morphpre_im [lemma, in mathcomp.fingroup.morphism]
sub_morphim_pre [lemma, in mathcomp.fingroup.morphism]
sub_center_normal [lemma, in mathcomp.solvable.center]
sub_cyclic_char [lemma, in mathcomp.solvable.cyclic]
sub_span [lemma, in mathcomp.algebra.vector]
sub_ordK [lemma, in mathcomp.ssreflect.fintype]
sub_ord [definition, in mathcomp.ssreflect.fintype]
sub_ord_proof [lemma, in mathcomp.ssreflect.fintype]
sub_proper_trans [lemma, in mathcomp.ssreflect.fintype]
sub_in_le_big [lemma, in mathcomp.ssreflect.bigop]
sub_le_big_seq_cond [lemma, in mathcomp.ssreflect.bigop]
sub_le_big_seq [lemma, in mathcomp.ssreflect.bigop]
sub_le_big [lemma, in mathcomp.ssreflect.bigop]
sub_type [definition, in mathcomp.ssreflect.eqtype]
sub_spec [abbreviation, in mathcomp.ssreflect.eqtype]
Sub_spec [inductive, in mathcomp.ssreflect.eqtype]
Sub_rect:253 [binder, in mathcomp.ssreflect.eqtype]
sub_sort:245 [binder, in mathcomp.ssreflect.eqtype]
sub_agenv [lemma, in mathcomp.field.falgebra]
sub_dsumsmx [lemma, in mathcomp.algebra.mxalgebra]
sub_dsumsmx_spec [inductive, in mathcomp.algebra.mxalgebra]
sub_daddsmx [lemma, in mathcomp.algebra.mxalgebra]
sub_daddsmx_spec [inductive, in mathcomp.algebra.mxalgebra]
sub_bigcapmxP [lemma, in mathcomp.algebra.mxalgebra]
sub_capmx [lemma, in mathcomp.algebra.mxalgebra]
sub_capmx_gen [lemma, in mathcomp.algebra.mxalgebra]
sub_kermx [lemma, in mathcomp.algebra.mxalgebra]
sub_kermxP [lemma, in mathcomp.algebra.mxalgebra]
sub_sumsmxP [lemma, in mathcomp.algebra.mxalgebra]
sub_sums_genmxP [lemma, in mathcomp.algebra.mxalgebra]
sub_addsmxP [lemma, in mathcomp.algebra.mxalgebra]
sub_rVP [lemma, in mathcomp.algebra.mxalgebra]
sub_ltmx_trans [lemma, in mathcomp.algebra.mxalgebra]
sub0mx [lemma, in mathcomp.algebra.mxalgebra]
sub0n [lemma, in mathcomp.ssreflect.ssrnat]
sub0seq [lemma, in mathcomp.ssreflect.seq]
sub0set [lemma, in mathcomp.ssreflect.finset]
sub0v [lemma, in mathcomp.algebra.vector]
sub1b [lemma, in mathcomp.ssreflect.ssrnat]
sub1G [lemma, in mathcomp.fingroup.fingroup]
sub1mx [lemma, in mathcomp.algebra.mxalgebra]
sub1seq [lemma, in mathcomp.ssreflect.seq]
sub1set [lemma, in mathcomp.ssreflect.finset]
sub1v [lemma, in mathcomp.field.fieldext]
sub1_agenv [lemma, in mathcomp.field.falgebra]
Sub:248 [binder, in mathcomp.ssreflect.eqtype]
sub:783 [binder, in mathcomp.algebra.matrix]
succn [abbreviation, in mathcomp.ssreflect.ssrnat]
succnK [lemma, in mathcomp.ssreflect.ssrnat]
succn_inj [lemma, in mathcomp.ssreflect.ssrnat]
suffix [definition, in mathcomp.ssreflect.seq]
suffixE [lemma, in mathcomp.ssreflect.seq]
suffixP [lemma, in mathcomp.ssreflect.seq]
suffixs0 [lemma, in mathcomp.ssreflect.seq]
suffixW [lemma, in mathcomp.ssreflect.seq]
suffix_drop [lemma, in mathcomp.ssreflect.seq]
suffix_uniq [lemma, in mathcomp.ssreflect.seq]
suffix_prefix_trans [lemma, in mathcomp.ssreflect.seq]
suffix_infix_trans [lemma, in mathcomp.ssreflect.seq]
suffix_infix [lemma, in mathcomp.ssreflect.seq]
suffix_cons [lemma, in mathcomp.ssreflect.seq]
suffix_catr [lemma, in mathcomp.ssreflect.seq]
suffix_catl [lemma, in mathcomp.ssreflect.seq]
suffix_rcons [lemma, in mathcomp.ssreflect.seq]
suffix_trans [lemma, in mathcomp.ssreflect.seq]
suffix_suffix [lemma, in mathcomp.ssreflect.seq]
suffix_revLR [lemma, in mathcomp.ssreflect.seq]
suffix_rev [lemma, in mathcomp.ssreflect.seq]
suffix_refl [lemma, in mathcomp.ssreflect.seq]
suffix_subseq [lemma, in mathcomp.ssreflect.seq]
suffix_sorted [lemma, in mathcomp.ssreflect.path]
suffix0s [lemma, in mathcomp.ssreflect.seq]
suffix1s [lemma, in mathcomp.ssreflect.seq]
sumA:212 [binder, in mathcomp.field.falgebra]
SumEqType [section, in mathcomp.ssreflect.eqtype]
SumEqType.T1 [variable, in mathcomp.ssreflect.eqtype]
SumEqType.T2 [variable, in mathcomp.ssreflect.eqtype]
SumFinType [section, in mathcomp.ssreflect.fintype]
SumFinType.T1 [variable, in mathcomp.ssreflect.fintype]
SumFinType.T2 [variable, in mathcomp.ssreflect.fintype]
sumfv [lemma, in mathcomp.algebra.vector]
sumKx [abbreviation, in mathcomp.field.fieldext]
summxE [lemma, in mathcomp.algebra.matrix]
summx_sub_sums [lemma, in mathcomp.algebra.mxalgebra]
summx_sub [lemma, in mathcomp.algebra.mxalgebra]
sumMz [lemma, in mathcomp.algebra.ssrint]
sumn [definition, in mathcomp.ssreflect.seq]
sumnB [lemma, in mathcomp.ssreflect.bigop]
sumnE [lemma, in mathcomp.ssreflect.bigop]
sumn_flatten [lemma, in mathcomp.ssreflect.seq]
sumn_set_nth0 [lemma, in mathcomp.ssreflect.seq]
sumn_set_nth_ltn [lemma, in mathcomp.ssreflect.seq]
sumn_set_nth [lemma, in mathcomp.ssreflect.seq]
sumn_rev [lemma, in mathcomp.ssreflect.seq]
sumn_rot [lemma, in mathcomp.ssreflect.seq]
sumn_rcons [lemma, in mathcomp.ssreflect.seq]
sumn_count [lemma, in mathcomp.ssreflect.seq]
sumn_cat [lemma, in mathcomp.ssreflect.seq]
sumn_nseq [lemma, in mathcomp.ssreflect.seq]
sumn_ncons [lemma, in mathcomp.ssreflect.seq]
sumsmxMr [lemma, in mathcomp.algebra.mxalgebra]
sumsmxMr_gen [lemma, in mathcomp.algebra.mxalgebra]
sumsmxS [lemma, in mathcomp.algebra.mxalgebra]
sumsmx_semisimple [lemma, in mathcomp.character.mxrepresentation]
sumsmx_module [lemma, in mathcomp.character.mxrepresentation]
sumsmx_subP [lemma, in mathcomp.algebra.mxalgebra]
sumsmx_sup [lemma, in mathcomp.algebra.mxalgebra]
sumV [abbreviation, in mathcomp.algebra.vector]
SumvPi [section, in mathcomp.algebra.vector]
SumvPi.K [variable, in mathcomp.algebra.vector]
SumvPi.vT [variable, in mathcomp.algebra.vector]
sumv_pi_nat_sum [lemma, in mathcomp.algebra.vector]
sumv_pi_sum [lemma, in mathcomp.algebra.vector]
sumv_pi [abbreviation, in mathcomp.algebra.vector]
sumv_pi_uniq_sum [lemma, in mathcomp.algebra.vector]
sumv_pi_for [definition, in mathcomp.algebra.vector]
sumv_sup [lemma, in mathcomp.algebra.vector]
sumX:568 [binder, in mathcomp.algebra.vector]
sum_norm2_char_generators [lemma, in mathcomp.character.integral_char]
sum_of_opair [definition, in mathcomp.ssreflect.choice]
sum_index_rcosets_cycle [lemma, in mathcomp.solvable.finmodule]
sum_nat_cond_const [lemma, in mathcomp.ssreflect.finset]
sum_card_class [lemma, in mathcomp.fingroup.action]
sum_by_classes [lemma, in mathcomp.character.classfun]
sum_cfunE [lemma, in mathcomp.character.classfun]
sum_irr_degree [lemma, in mathcomp.character.mxrepresentation]
sum_mxsimple_direct_sub [lemma, in mathcomp.character.mxrepresentation]
sum_mxsimple_direct_compl [lemma, in mathcomp.character.mxrepresentation]
sum_totient_dvd [lemma, in mathcomp.solvable.cyclic]
sum_ncycle_totient [lemma, in mathcomp.solvable.cyclic]
sum_ffun [lemma, in mathcomp.algebra.ssralg]
sum_ffunE [lemma, in mathcomp.algebra.ssralg]
sum_lfunE [lemma, in mathcomp.algebra.vector]
sum_norm_irr_quo [lemma, in mathcomp.character.character]
sum_enum_uniq [lemma, in mathcomp.ssreflect.fintype]
sum_enum [definition, in mathcomp.ssreflect.fintype]
sum_drop_poly [lemma, in mathcomp.algebra.poly]
sum_odd_poly [lemma, in mathcomp.algebra.poly]
sum_even_poly [lemma, in mathcomp.algebra.poly]
sum_nat_seq_eq1 [lemma, in mathcomp.ssreflect.bigop]
sum_nat_eq1 [lemma, in mathcomp.ssreflect.bigop]
sum_nat_seq_neq0 [lemma, in mathcomp.ssreflect.bigop]
sum_nat_seq_eq0 [lemma, in mathcomp.ssreflect.bigop]
sum_nat_eq0 [lemma, in mathcomp.ssreflect.bigop]
sum_nat_const_nat [lemma, in mathcomp.ssreflect.bigop]
sum_nat_const [lemma, in mathcomp.ssreflect.bigop]
sum_eqE [lemma, in mathcomp.ssreflect.eqtype]
sum_eqP [lemma, in mathcomp.ssreflect.eqtype]
sum_eq [definition, in mathcomp.ssreflect.eqtype]
sum_mxsum [definition, in mathcomp.algebra.mxalgebra]
sum1dep_card [lemma, in mathcomp.ssreflect.finset]
sum1_size [lemma, in mathcomp.ssreflect.bigop]
sum1_count [lemma, in mathcomp.ssreflect.bigop]
sum1_card [lemma, in mathcomp.ssreflect.bigop]
sum12g:156 [binder, in mathcomp.character.integral_char]
Support [section, in mathcomp.ssreflect.finfun]
support [abbreviation, in mathcomp.algebra.ssralg]
supportE [lemma, in mathcomp.ssreflect.finfun]
supportP [lemma, in mathcomp.ssreflect.finfun]
support_zchar [lemma, in mathcomp.character.vcharacter]
support_for [definition, in mathcomp.ssreflect.finfun]
support_cfAut [lemma, in mathcomp.character.classfun]
support_cfuni [lemma, in mathcomp.character.classfun]
support_cfun [lemma, in mathcomp.character.classfun]
Support.aT [variable, in mathcomp.ssreflect.finfun]
Support.rT [variable, in mathcomp.ssreflect.finfun]
sup_field_module [lemma, in mathcomp.field.fieldext]
Surgery [section, in mathcomp.algebra.poly]
Surgery.R [variable, in mathcomp.algebra.poly]
sv [definition, in mathcomp.solvable.burnside_app]
Sv [definition, in mathcomp.solvable.burnside_app]
sval [abbreviation, in mathcomp.ssreflect.ssrfun]
sv_inv [lemma, in mathcomp.solvable.burnside_app]
Sv_inj [lemma, in mathcomp.solvable.burnside_app]
Sv:2375 [binder, in mathcomp.algebra.ssralg]
Sv:2412 [binder, in mathcomp.algebra.ssralg]
Sv:2448 [binder, in mathcomp.algebra.ssralg]
Sv:2485 [binder, in mathcomp.algebra.ssralg]
Sv:2540 [binder, in mathcomp.algebra.ssralg]
Sv:2617 [binder, in mathcomp.algebra.ssralg]
Sv:3617 [binder, in mathcomp.ssreflect.order]
Sv:3712 [binder, in mathcomp.ssreflect.order]
Sv:3799 [binder, in mathcomp.ssreflect.order]
swapXY [definition, in mathcomp.algebra.polyXY]
swapXYK [lemma, in mathcomp.algebra.polyXY]
swapXY_map [lemma, in mathcomp.algebra.polyXY]
swapXY_poly_XmY [lemma, in mathcomp.algebra.polyXY]
swapXY_poly_XaY [lemma, in mathcomp.algebra.polyXY]
swapXY_comp_poly [lemma, in mathcomp.algebra.polyXY]
swapXY_is_scalable [lemma, in mathcomp.algebra.polyXY]
swapXY_is_multiplicative [lemma, in mathcomp.algebra.polyXY]
swapXY_eq0 [lemma, in mathcomp.algebra.polyXY]
swapXY_map_polyC [lemma, in mathcomp.algebra.polyXY]
swapXY_is_additive [lemma, in mathcomp.algebra.polyXY]
swapXY_Y [lemma, in mathcomp.algebra.polyXY]
swapXY_X [lemma, in mathcomp.algebra.polyXY]
swapXY_polyC [lemma, in mathcomp.algebra.polyXY]
swapXY_unlockable [definition, in mathcomp.algebra.polyXY]
swapXY_def [definition, in mathcomp.algebra.polyXY]
swapXY_key [lemma, in mathcomp.algebra.polyXY]
SwizzleAdd [abbreviation, in mathcomp.algebra.matrix]
SwizzleAdd [abbreviation, in mathcomp.algebra.matrix]
SwizzleLin [abbreviation, in mathcomp.algebra.matrix]
swizzle_mx_is_scalable [lemma, in mathcomp.algebra.matrix]
swizzle_mx_is_additive [lemma, in mathcomp.algebra.matrix]
swizzle_mx_is_semi_additive [lemma, in mathcomp.algebra.matrix]
swizzle_mx [definition, in mathcomp.algebra.matrix]
sW:1031 [binder, in mathcomp.character.mxrepresentation]
Syl [definition, in mathcomp.solvable.pgroup]
Sylow [section, in mathcomp.solvable.sylow]
Sylow [definition, in mathcomp.solvable.pgroup]
sylow [library]
SylowJ [lemma, in mathcomp.solvable.pgroup]
SylowP [lemma, in mathcomp.solvable.pgroup]
SylowSolvableAct [section, in mathcomp.solvable.hall]
SylowSolvableAct.gT [variable, in mathcomp.solvable.hall]
SylowSolvableAct.p [variable, in mathcomp.solvable.hall]
Sylow_subnorm [lemma, in mathcomp.solvable.sylow]
Sylow_gen [lemma, in mathcomp.solvable.sylow]
Sylow_transversal_gen [lemma, in mathcomp.solvable.sylow]
Sylow_setI_normal [lemma, in mathcomp.solvable.sylow]
Sylow_Jsub [lemma, in mathcomp.solvable.sylow]
Sylow_subJ [lemma, in mathcomp.solvable.sylow]
Sylow_trans [lemma, in mathcomp.solvable.sylow]
Sylow_exists [lemma, in mathcomp.solvable.sylow]
Sylow_superset [lemma, in mathcomp.solvable.sylow]
Sylow's_theorem [lemma, in mathcomp.solvable.sylow]
Sylow.G [variable, in mathcomp.solvable.sylow]
Sylow.gT [variable, in mathcomp.solvable.sylow]
Sylow.p [variable, in mathcomp.solvable.sylow]
Sylow1 [lemma, in mathcomp.solvable.pgroup]
Sylvester_mxE [lemma, in mathcomp.algebra.mxpoly]
Sylvester_mx [definition, in mathcomp.algebra.mxpoly]
Syl_trans [lemma, in mathcomp.solvable.sylow]
Sym [definition, in mathcomp.solvable.alt]
Sym [definition, in mathcomp.fingroup.perm]
SymAltDef [section, in mathcomp.solvable.alt]
SymAltDef.n [variable, in mathcomp.solvable.alt]
SymAltDef.T [variable, in mathcomp.solvable.alt]
'Alt_T [notation, in mathcomp.solvable.alt]
'Sym_T [notation, in mathcomp.solvable.alt]
SymE [lemma, in mathcomp.fingroup.action]
Symmetry [section, in mathcomp.fingroup.perm]
Symmetry [section, in mathcomp.fingroup.action]
Symmetry.S [variable, in mathcomp.fingroup.perm]
Symmetry.S [variable, in mathcomp.fingroup.action]
Symmetry.T [variable, in mathcomp.fingroup.perm]
Symmetry.T [variable, in mathcomp.fingroup.action]
symplectic_type_group_structure [lemma, in mathcomp.solvable.extremal]
Sym_trans [lemma, in mathcomp.solvable.alt]
Sym_group [definition, in mathcomp.solvable.alt]
Sym_group [definition, in mathcomp.fingroup.perm]
Sym_group_set [lemma, in mathcomp.fingroup.perm]
sym_connect_sym [lemma, in mathcomp.ssreflect.fingraph]
sz_rs:221 [binder, in mathcomp.solvable.cyclic]
S_:20 [binder, in mathcomp.algebra.mxpoly]
s_a:1116 [binder, in mathcomp.algebra.ssralg]
s_gt0:765 [binder, in mathcomp.ssreflect.fintype]
S_:1344 [binder, in mathcomp.algebra.mxalgebra]
S_:1322 [binder, in mathcomp.algebra.mxalgebra]
S_:1284 [binder, in mathcomp.algebra.mxalgebra]
s':1210 [binder, in mathcomp.ssreflect.seq]
s':1268 [binder, in mathcomp.ssreflect.seq]
s':1889 [binder, in mathcomp.ssreflect.seq]
s':2367 [binder, in mathcomp.ssreflect.bigop]
s':2379 [binder, in mathcomp.ssreflect.bigop]
s':2392 [binder, in mathcomp.ssreflect.bigop]
s':2403 [binder, in mathcomp.ssreflect.bigop]
s':2418 [binder, in mathcomp.ssreflect.bigop]
s':2430 [binder, in mathcomp.ssreflect.bigop]
S':2523 [binder, in mathcomp.ssreflect.seq]
s':257 [binder, in mathcomp.ssreflect.fintype]
s':259 [binder, in mathcomp.ssreflect.fintype]
s':315 [binder, in mathcomp.ssreflect.tuple]
s':317 [binder, in mathcomp.ssreflect.tuple]
s':346 [binder, in mathcomp.ssreflect.tuple]
s':349 [binder, in mathcomp.ssreflect.tuple]
s':50 [binder, in mathcomp.fingroup.presentation]
s':551 [binder, in mathcomp.ssreflect.seq]
s':552 [binder, in mathcomp.ssreflect.seq]
s':553 [binder, in mathcomp.ssreflect.seq]
s':735 [binder, in mathcomp.ssreflect.seq]
s':89 [binder, in mathcomp.ssreflect.path]
s0 [definition, in mathcomp.solvable.burnside_app]
S0 [definition, in mathcomp.solvable.burnside_app]
S0f [definition, in mathcomp.solvable.burnside_app]
S0_inv [lemma, in mathcomp.solvable.burnside_app]
s05 [definition, in mathcomp.solvable.burnside_app]
S05 [definition, in mathcomp.solvable.burnside_app]
S05f [definition, in mathcomp.solvable.burnside_app]
S05_inj [lemma, in mathcomp.solvable.burnside_app]
s0:236 [binder, in mathcomp.solvable.cyclic]
s0:241 [binder, in mathcomp.solvable.cyclic]
s0:54 [binder, in mathcomp.solvable.extremal]
s0:56 [binder, in mathcomp.solvable.extremal]
s1 [definition, in mathcomp.solvable.burnside_app]
S1 [definition, in mathcomp.solvable.burnside_app]
S1f [definition, in mathcomp.solvable.burnside_app]
s1y:907 [binder, in mathcomp.ssreflect.seq]
S1_inv [lemma, in mathcomp.solvable.burnside_app]
s1':1798 [binder, in mathcomp.ssreflect.seq]
s1':2568 [binder, in mathcomp.ssreflect.seq]
s1':2580 [binder, in mathcomp.ssreflect.seq]
s1':536 [binder, in mathcomp.ssreflect.path]
s14 [definition, in mathcomp.solvable.burnside_app]
S14 [definition, in mathcomp.solvable.burnside_app]
S14f [definition, in mathcomp.solvable.burnside_app]
S14_inj [lemma, in mathcomp.solvable.burnside_app]
s1:101 [binder, in mathcomp.ssreflect.seq]
s1:1015 [binder, in mathcomp.ssreflect.seq]
s1:1062 [binder, in mathcomp.ssreflect.seq]
s1:1070 [binder, in mathcomp.ssreflect.seq]
s1:1076 [binder, in mathcomp.ssreflect.seq]
s1:1080 [binder, in mathcomp.ssreflect.seq]
s1:1083 [binder, in mathcomp.ssreflect.seq]
s1:1091 [binder, in mathcomp.ssreflect.seq]
s1:1095 [binder, in mathcomp.ssreflect.seq]
s1:1097 [binder, in mathcomp.ssreflect.seq]
s1:11 [binder, in mathcomp.fingroup.presentation]
s1:1101 [binder, in mathcomp.ssreflect.seq]
s1:1106 [binder, in mathcomp.ssreflect.seq]
s1:1113 [binder, in mathcomp.ssreflect.seq]
s1:1116 [binder, in mathcomp.ssreflect.seq]
s1:1119 [binder, in mathcomp.ssreflect.seq]
S1:112 [binder, in mathcomp.character.classfun]
S1:114 [binder, in mathcomp.fingroup.action]
s1:1162 [binder, in mathcomp.ssreflect.seq]
s1:121 [binder, in mathcomp.solvable.jordanholder]
s1:1220 [binder, in mathcomp.ssreflect.seq]
s1:1222 [binder, in mathcomp.ssreflect.seq]
s1:1228 [binder, in mathcomp.ssreflect.seq]
s1:1236 [binder, in mathcomp.ssreflect.seq]
s1:1239 [binder, in mathcomp.ssreflect.seq]
s1:1242 [binder, in mathcomp.ssreflect.seq]
s1:1247 [binder, in mathcomp.ssreflect.seq]
s1:1251 [binder, in mathcomp.ssreflect.seq]
s1:1253 [binder, in mathcomp.ssreflect.seq]
s1:1255 [binder, in mathcomp.ssreflect.order]
s1:1265 [binder, in mathcomp.ssreflect.order]
s1:1267 [binder, in mathcomp.ssreflect.order]
s1:1269 [binder, in mathcomp.ssreflect.order]
s1:1273 [binder, in mathcomp.ssreflect.seq]
s1:1280 [binder, in mathcomp.ssreflect.seq]
s1:1282 [binder, in mathcomp.ssreflect.seq]
s1:13 [binder, in mathcomp.ssreflect.ssrAC]
S1:1311 [binder, in mathcomp.algebra.mxalgebra]
s1:137 [binder, in mathcomp.ssreflect.seq]
s1:1460 [binder, in mathcomp.ssreflect.seq]
s1:1472 [binder, in mathcomp.ssreflect.seq]
s1:1481 [binder, in mathcomp.ssreflect.seq]
s1:1510 [binder, in mathcomp.ssreflect.seq]
s1:152 [binder, in mathcomp.ssreflect.seq]
s1:1534 [binder, in mathcomp.ssreflect.seq]
s1:1547 [binder, in mathcomp.ssreflect.seq]
s1:1550 [binder, in mathcomp.ssreflect.seq]
S1:157 [binder, in mathcomp.character.classfun]
s1:1586 [binder, in mathcomp.ssreflect.seq]
s1:1634 [binder, in mathcomp.ssreflect.seq]
s1:1645 [binder, in mathcomp.ssreflect.seq]
s1:1649 [binder, in mathcomp.ssreflect.seq]
S1:176 [binder, in mathcomp.character.classfun]
s1:1782 [binder, in mathcomp.ssreflect.seq]
s1:1787 [binder, in mathcomp.ssreflect.seq]
s1:1792 [binder, in mathcomp.ssreflect.seq]
s1:1796 [binder, in mathcomp.ssreflect.seq]
s1:1800 [binder, in mathcomp.ssreflect.seq]
s1:1802 [binder, in mathcomp.ssreflect.seq]
s1:1807 [binder, in mathcomp.ssreflect.seq]
s1:1810 [binder, in mathcomp.ssreflect.seq]
s1:1815 [binder, in mathcomp.ssreflect.seq]
s1:1817 [binder, in mathcomp.ssreflect.seq]
s1:1822 [binder, in mathcomp.ssreflect.seq]
s1:1824 [binder, in mathcomp.ssreflect.seq]
s1:1826 [binder, in mathcomp.ssreflect.seq]
s1:1828 [binder, in mathcomp.ssreflect.seq]
s1:1830 [binder, in mathcomp.ssreflect.seq]
s1:1832 [binder, in mathcomp.ssreflect.seq]
s1:1835 [binder, in mathcomp.ssreflect.seq]
s1:1839 [binder, in mathcomp.ssreflect.seq]
s1:1843 [binder, in mathcomp.ssreflect.seq]
s1:1847 [binder, in mathcomp.ssreflect.seq]
s1:1851 [binder, in mathcomp.ssreflect.seq]
s1:1855 [binder, in mathcomp.ssreflect.seq]
s1:1861 [binder, in mathcomp.ssreflect.seq]
s1:1865 [binder, in mathcomp.ssreflect.seq]
s1:1867 [binder, in mathcomp.ssreflect.seq]
s1:1869 [binder, in mathcomp.ssreflect.seq]
s1:1873 [binder, in mathcomp.ssreflect.seq]
s1:1876 [binder, in mathcomp.ssreflect.seq]
s1:1878 [binder, in mathcomp.ssreflect.seq]
s1:1880 [binder, in mathcomp.ssreflect.seq]
s1:1883 [binder, in mathcomp.ssreflect.seq]
s1:1886 [binder, in mathcomp.ssreflect.seq]
s1:1890 [binder, in mathcomp.ssreflect.seq]
s1:1892 [binder, in mathcomp.ssreflect.seq]
s1:1894 [binder, in mathcomp.ssreflect.seq]
s1:1896 [binder, in mathcomp.ssreflect.seq]
s1:1904 [binder, in mathcomp.ssreflect.seq]
s1:1907 [binder, in mathcomp.ssreflect.seq]
s1:1909 [binder, in mathcomp.ssreflect.seq]
s1:1912 [binder, in mathcomp.ssreflect.seq]
s1:1916 [binder, in mathcomp.ssreflect.seq]
s1:1919 [binder, in mathcomp.ssreflect.seq]
s1:1921 [binder, in mathcomp.ssreflect.seq]
s1:1924 [binder, in mathcomp.ssreflect.seq]
s1:1928 [binder, in mathcomp.ssreflect.seq]
s1:1931 [binder, in mathcomp.ssreflect.seq]
s1:1934 [binder, in mathcomp.ssreflect.seq]
s1:1937 [binder, in mathcomp.ssreflect.seq]
s1:194 [binder, in mathcomp.ssreflect.seq]
s1:1940 [binder, in mathcomp.ssreflect.seq]
s1:1943 [binder, in mathcomp.ssreflect.seq]
s1:1945 [binder, in mathcomp.ssreflect.seq]
s1:1947 [binder, in mathcomp.ssreflect.seq]
s1:1957 [binder, in mathcomp.ssreflect.seq]
s1:1959 [binder, in mathcomp.ssreflect.seq]
s1:1961 [binder, in mathcomp.ssreflect.seq]
s1:1973 [binder, in mathcomp.ssreflect.seq]
s1:1976 [binder, in mathcomp.ssreflect.seq]
s1:1979 [binder, in mathcomp.ssreflect.seq]
s1:1981 [binder, in mathcomp.ssreflect.seq]
s1:1983 [binder, in mathcomp.ssreflect.seq]
s1:1985 [binder, in mathcomp.ssreflect.seq]
s1:2082 [binder, in mathcomp.ssreflect.seq]
s1:21 [binder, in mathcomp.solvable.jordanholder]
s1:216 [binder, in mathcomp.ssreflect.seq]
s1:220 [binder, in mathcomp.ssreflect.seq]
s1:2208 [binder, in mathcomp.ssreflect.seq]
s1:222 [binder, in mathcomp.ssreflect.seq]
s1:2222 [binder, in mathcomp.ssreflect.seq]
s1:226 [binder, in mathcomp.ssreflect.seq]
s1:232 [binder, in mathcomp.fingroup.perm]
s1:234 [binder, in mathcomp.fingroup.perm]
s1:237 [binder, in mathcomp.fingroup.perm]
s1:2394 [binder, in mathcomp.ssreflect.seq]
s1:2407 [binder, in mathcomp.ssreflect.seq]
s1:246 [binder, in mathcomp.ssreflect.path]
s1:248 [binder, in mathcomp.ssreflect.path]
s1:250 [binder, in mathcomp.ssreflect.path]
s1:252 [binder, in mathcomp.ssreflect.path]
s1:253 [binder, in mathcomp.ssreflect.fintype]
s1:2552 [binder, in mathcomp.ssreflect.seq]
s1:2557 [binder, in mathcomp.ssreflect.seq]
s1:2562 [binder, in mathcomp.ssreflect.seq]
s1:2567 [binder, in mathcomp.ssreflect.seq]
s1:257 [binder, in mathcomp.ssreflect.path]
s1:2573 [binder, in mathcomp.ssreflect.seq]
s1:2579 [binder, in mathcomp.ssreflect.seq]
s1:259 [binder, in mathcomp.ssreflect.path]
s1:260 [binder, in mathcomp.ssreflect.fintype]
S1:2628 [binder, in mathcomp.algebra.matrix]
s1:267 [binder, in mathcomp.ssreflect.fintype]
s1:2677 [binder, in mathcomp.ssreflect.seq]
s1:269 [binder, in mathcomp.ssreflect.path]
s1:27 [binder, in mathcomp.field.algnum]
s1:271 [binder, in mathcomp.ssreflect.path]
s1:274 [binder, in mathcomp.ssreflect.path]
s1:276 [binder, in mathcomp.ssreflect.path]
s1:28 [binder, in mathcomp.field.algnum]
s1:291 [binder, in mathcomp.ssreflect.path]
s1:293 [binder, in mathcomp.ssreflect.path]
s1:298 [binder, in mathcomp.ssreflect.seq]
s1:301 [binder, in mathcomp.ssreflect.seq]
s1:326 [binder, in mathcomp.ssreflect.seq]
s1:329 [binder, in mathcomp.ssreflect.seq]
s1:331 [binder, in mathcomp.ssreflect.seq]
s1:35 [binder, in mathcomp.ssreflect.seq]
s1:353 [binder, in mathcomp.ssreflect.fintype]
s1:358 [binder, in mathcomp.ssreflect.fintype]
s1:383 [binder, in mathcomp.ssreflect.seq]
s1:387 [binder, in mathcomp.ssreflect.seq]
S1:415 [binder, in mathcomp.algebra.vector]
s1:43 [binder, in mathcomp.ssreflect.seq]
s1:437 [binder, in mathcomp.ssreflect.path]
s1:44 [binder, in mathcomp.solvable.jordanholder]
s1:4433 [binder, in mathcomp.ssreflect.order]
s1:4438 [binder, in mathcomp.ssreflect.order]
s1:444 [binder, in mathcomp.ssreflect.path]
s1:4445 [binder, in mathcomp.ssreflect.order]
s1:4449 [binder, in mathcomp.ssreflect.order]
s1:4454 [binder, in mathcomp.ssreflect.order]
s1:4466 [binder, in mathcomp.ssreflect.order]
s1:447 [binder, in mathcomp.ssreflect.seq]
s1:4471 [binder, in mathcomp.ssreflect.order]
s1:4474 [binder, in mathcomp.ssreflect.order]
s1:4479 [binder, in mathcomp.ssreflect.order]
s1:448 [binder, in mathcomp.ssreflect.path]
s1:4495 [binder, in mathcomp.ssreflect.order]
s1:4500 [binder, in mathcomp.ssreflect.order]
s1:4505 [binder, in mathcomp.ssreflect.order]
s1:4507 [binder, in mathcomp.ssreflect.order]
s1:4511 [binder, in mathcomp.ssreflect.order]
s1:4520 [binder, in mathcomp.ssreflect.order]
s1:4524 [binder, in mathcomp.ssreflect.order]
s1:4528 [binder, in mathcomp.ssreflect.order]
s1:4532 [binder, in mathcomp.ssreflect.order]
s1:4536 [binder, in mathcomp.ssreflect.order]
s1:4539 [binder, in mathcomp.ssreflect.order]
s1:4543 [binder, in mathcomp.ssreflect.order]
s1:4547 [binder, in mathcomp.ssreflect.order]
s1:456 [binder, in mathcomp.ssreflect.seq]
s1:456 [binder, in mathcomp.ssreflect.path]
s1:462 [binder, in mathcomp.ssreflect.path]
s1:463 [binder, in mathcomp.ssreflect.seq]
s1:464 [binder, in mathcomp.ssreflect.path]
s1:465 [binder, in mathcomp.ssreflect.seq]
s1:468 [binder, in mathcomp.ssreflect.path]
s1:469 [binder, in mathcomp.ssreflect.seq]
s1:480 [binder, in mathcomp.ssreflect.path]
s1:482 [binder, in mathcomp.ssreflect.path]
S1:484 [binder, in mathcomp.character.classfun]
s1:488 [binder, in mathcomp.ssreflect.path]
S1:490 [binder, in mathcomp.character.classfun]
s1:490 [binder, in mathcomp.ssreflect.path]
S1:492 [binder, in mathcomp.character.classfun]
s1:506 [binder, in mathcomp.ssreflect.path]
s1:508 [binder, in mathcomp.ssreflect.path]
s1:510 [binder, in mathcomp.ssreflect.path]
s1:511 [binder, in mathcomp.ssreflect.path]
s1:512 [binder, in mathcomp.ssreflect.seq]
s1:513 [binder, in mathcomp.ssreflect.path]
s1:52 [binder, in mathcomp.ssreflect.seq]
S1:52 [binder, in mathcomp.solvable.primitive_action]
S1:521 [binder, in mathcomp.character.classfun]
s1:522 [binder, in mathcomp.ssreflect.path]
s1:524 [binder, in mathcomp.ssreflect.path]
s1:526 [binder, in mathcomp.ssreflect.path]
s1:532 [binder, in mathcomp.ssreflect.path]
s1:533 [binder, in mathcomp.ssreflect.order]
s1:535 [binder, in mathcomp.ssreflect.path]
s1:536 [binder, in mathcomp.ssreflect.order]
S1:538 [binder, in mathcomp.character.classfun]
s1:538 [binder, in mathcomp.ssreflect.order]
s1:540 [binder, in mathcomp.ssreflect.order]
s1:543 [binder, in mathcomp.ssreflect.order]
s1:545 [binder, in mathcomp.ssreflect.order]
s1:548 [binder, in mathcomp.ssreflect.path]
s1:55 [binder, in mathcomp.ssreflect.seq]
S1:556 [binder, in mathcomp.algebra.poly]
s1:569 [binder, in mathcomp.ssreflect.seq]
s1:569 [binder, in mathcomp.ssreflect.path]
s1:57 [binder, in mathcomp.ssreflect.seq]
s1:571 [binder, in mathcomp.ssreflect.seq]
s1:571 [binder, in mathcomp.ssreflect.path]
s1:573 [binder, in mathcomp.ssreflect.seq]
s1:601 [binder, in mathcomp.ssreflect.seq]
s1:603 [binder, in mathcomp.ssreflect.seq]
s1:605 [binder, in mathcomp.ssreflect.seq]
s1:619 [binder, in mathcomp.ssreflect.seq]
s1:621 [binder, in mathcomp.ssreflect.seq]
S1:64 [binder, in mathcomp.fingroup.perm]
s1:655 [binder, in mathcomp.ssreflect.seq]
s1:660 [binder, in mathcomp.ssreflect.path]
s1:664 [binder, in mathcomp.ssreflect.path]
s1:681 [binder, in mathcomp.ssreflect.seq]
s1:686 [binder, in mathcomp.ssreflect.seq]
s1:691 [binder, in mathcomp.ssreflect.seq]
s1:694 [binder, in mathcomp.ssreflect.seq]
s1:697 [binder, in mathcomp.ssreflect.seq]
S1:70 [binder, in mathcomp.character.vcharacter]
s1:702 [binder, in mathcomp.ssreflect.seq]
s1:707 [binder, in mathcomp.ssreflect.seq]
s1:712 [binder, in mathcomp.ssreflect.seq]
s1:717 [binder, in mathcomp.ssreflect.seq]
s1:722 [binder, in mathcomp.ssreflect.seq]
S1:74 [binder, in mathcomp.character.vcharacter]
S1:79 [binder, in mathcomp.character.vcharacter]
s1:791 [binder, in mathcomp.ssreflect.seq]
s1:802 [binder, in mathcomp.ssreflect.seq]
s1:809 [binder, in mathcomp.ssreflect.seq]
S1:82 [binder, in mathcomp.character.vcharacter]
s1:828 [binder, in mathcomp.ssreflect.seq]
s1:831 [binder, in mathcomp.ssreflect.seq]
s1:835 [binder, in mathcomp.ssreflect.seq]
s1:837 [binder, in mathcomp.ssreflect.seq]
s1:839 [binder, in mathcomp.ssreflect.seq]
s1:841 [binder, in mathcomp.ssreflect.seq]
s1:843 [binder, in mathcomp.ssreflect.seq]
s1:850 [binder, in mathcomp.ssreflect.seq]
s1:852 [binder, in mathcomp.ssreflect.seq]
s1:855 [binder, in mathcomp.ssreflect.seq]
s1:858 [binder, in mathcomp.ssreflect.seq]
s1:86 [binder, in mathcomp.ssreflect.seq]
s1:862 [binder, in mathcomp.ssreflect.seq]
s1:865 [binder, in mathcomp.ssreflect.seq]
s1:868 [binder, in mathcomp.ssreflect.seq]
s1:879 [binder, in mathcomp.ssreflect.seq]
s1:884 [binder, in mathcomp.ssreflect.seq]
s1:886 [binder, in mathcomp.ssreflect.seq]
s1:894 [binder, in mathcomp.ssreflect.seq]
s1:897 [binder, in mathcomp.ssreflect.seq]
s1:900 [binder, in mathcomp.ssreflect.seq]
s1:902 [binder, in mathcomp.ssreflect.seq]
s1:904 [binder, in mathcomp.ssreflect.seq]
s1:908 [binder, in mathcomp.ssreflect.seq]
s1:910 [binder, in mathcomp.ssreflect.seq]
s1:912 [binder, in mathcomp.ssreflect.seq]
s1:914 [binder, in mathcomp.ssreflect.seq]
s1:916 [binder, in mathcomp.ssreflect.seq]
s1:918 [binder, in mathcomp.ssreflect.seq]
s1:92 [binder, in mathcomp.ssreflect.seq]
s1:923 [binder, in mathcomp.ssreflect.seq]
s1:926 [binder, in mathcomp.ssreflect.seq]
s1:929 [binder, in mathcomp.ssreflect.seq]
s1:933 [binder, in mathcomp.ssreflect.seq]
s1:936 [binder, in mathcomp.ssreflect.seq]
s1:943 [binder, in mathcomp.ssreflect.seq]
s1:98 [binder, in mathcomp.ssreflect.seq]
s2 [definition, in mathcomp.solvable.burnside_app]
S2 [definition, in mathcomp.solvable.burnside_app]
S2f [definition, in mathcomp.solvable.burnside_app]
S2_inv [lemma, in mathcomp.solvable.burnside_app]
s2':1804 [binder, in mathcomp.ssreflect.seq]
s2':1834 [binder, in mathcomp.ssreflect.seq]
s2':2575 [binder, in mathcomp.ssreflect.seq]
s2':2582 [binder, in mathcomp.ssreflect.seq]
s2':538 [binder, in mathcomp.ssreflect.path]
s23 [definition, in mathcomp.solvable.burnside_app]
S23 [definition, in mathcomp.solvable.burnside_app]
S23f [definition, in mathcomp.solvable.burnside_app]
s23_inv [lemma, in mathcomp.solvable.burnside_app]
S23_inv [lemma, in mathcomp.solvable.burnside_app]
s2:1016 [binder, in mathcomp.ssreflect.seq]
s2:102 [binder, in mathcomp.ssreflect.seq]
s2:1063 [binder, in mathcomp.ssreflect.seq]
s2:1071 [binder, in mathcomp.ssreflect.seq]
s2:1077 [binder, in mathcomp.ssreflect.seq]
s2:1081 [binder, in mathcomp.ssreflect.seq]
s2:1084 [binder, in mathcomp.ssreflect.seq]
s2:1092 [binder, in mathcomp.ssreflect.seq]
s2:1096 [binder, in mathcomp.ssreflect.seq]
s2:1098 [binder, in mathcomp.ssreflect.seq]
s2:1102 [binder, in mathcomp.ssreflect.seq]
s2:1107 [binder, in mathcomp.ssreflect.seq]
s2:1114 [binder, in mathcomp.ssreflect.seq]
s2:1117 [binder, in mathcomp.ssreflect.seq]
s2:1120 [binder, in mathcomp.ssreflect.seq]
S2:113 [binder, in mathcomp.character.classfun]
S2:115 [binder, in mathcomp.fingroup.action]
s2:1163 [binder, in mathcomp.ssreflect.seq]
s2:12 [binder, in mathcomp.fingroup.presentation]
s2:122 [binder, in mathcomp.solvable.jordanholder]
s2:1221 [binder, in mathcomp.ssreflect.seq]
s2:1223 [binder, in mathcomp.ssreflect.seq]
s2:1229 [binder, in mathcomp.ssreflect.seq]
s2:1237 [binder, in mathcomp.ssreflect.seq]
s2:1240 [binder, in mathcomp.ssreflect.seq]
s2:1243 [binder, in mathcomp.ssreflect.seq]
s2:1248 [binder, in mathcomp.ssreflect.seq]
s2:1252 [binder, in mathcomp.ssreflect.seq]
s2:1254 [binder, in mathcomp.ssreflect.seq]
s2:1256 [binder, in mathcomp.ssreflect.order]
s2:1266 [binder, in mathcomp.ssreflect.order]
s2:1268 [binder, in mathcomp.ssreflect.order]
s2:1270 [binder, in mathcomp.ssreflect.order]
s2:1274 [binder, in mathcomp.ssreflect.seq]
s2:1281 [binder, in mathcomp.ssreflect.seq]
s2:1283 [binder, in mathcomp.ssreflect.seq]
S2:1312 [binder, in mathcomp.algebra.mxalgebra]
s2:138 [binder, in mathcomp.ssreflect.seq]
s2:14 [binder, in mathcomp.ssreflect.ssrAC]
s2:1461 [binder, in mathcomp.ssreflect.seq]
s2:1473 [binder, in mathcomp.ssreflect.seq]
s2:1482 [binder, in mathcomp.ssreflect.seq]
s2:1511 [binder, in mathcomp.ssreflect.seq]
s2:153 [binder, in mathcomp.ssreflect.seq]
s2:1535 [binder, in mathcomp.ssreflect.seq]
s2:1548 [binder, in mathcomp.ssreflect.seq]
S2:158 [binder, in mathcomp.character.classfun]
s2:1587 [binder, in mathcomp.ssreflect.seq]
s2:1635 [binder, in mathcomp.ssreflect.seq]
s2:1646 [binder, in mathcomp.ssreflect.seq]
s2:1650 [binder, in mathcomp.ssreflect.seq]
s2:168 [binder, in mathcomp.ssreflect.seq]
S2:177 [binder, in mathcomp.character.classfun]
s2:1783 [binder, in mathcomp.ssreflect.seq]
s2:1788 [binder, in mathcomp.ssreflect.seq]
s2:1793 [binder, in mathcomp.ssreflect.seq]
s2:1797 [binder, in mathcomp.ssreflect.seq]
s2:1801 [binder, in mathcomp.ssreflect.seq]
s2:1803 [binder, in mathcomp.ssreflect.seq]
s2:1808 [binder, in mathcomp.ssreflect.seq]
s2:1811 [binder, in mathcomp.ssreflect.seq]
s2:1816 [binder, in mathcomp.ssreflect.seq]
s2:1818 [binder, in mathcomp.ssreflect.seq]
s2:1823 [binder, in mathcomp.ssreflect.seq]
s2:1825 [binder, in mathcomp.ssreflect.seq]
s2:1827 [binder, in mathcomp.ssreflect.seq]
s2:1829 [binder, in mathcomp.ssreflect.seq]
s2:1831 [binder, in mathcomp.ssreflect.seq]
s2:1833 [binder, in mathcomp.ssreflect.seq]
s2:1836 [binder, in mathcomp.ssreflect.seq]
s2:1840 [binder, in mathcomp.ssreflect.seq]
s2:1844 [binder, in mathcomp.ssreflect.seq]
s2:1848 [binder, in mathcomp.ssreflect.seq]
s2:1852 [binder, in mathcomp.ssreflect.seq]
s2:1856 [binder, in mathcomp.ssreflect.seq]
s2:1863 [binder, in mathcomp.ssreflect.seq]
s2:1866 [binder, in mathcomp.ssreflect.seq]
s2:1868 [binder, in mathcomp.ssreflect.seq]
s2:1870 [binder, in mathcomp.ssreflect.seq]
s2:1874 [binder, in mathcomp.ssreflect.seq]
s2:1877 [binder, in mathcomp.ssreflect.seq]
s2:1879 [binder, in mathcomp.ssreflect.seq]
s2:1881 [binder, in mathcomp.ssreflect.seq]
s2:1884 [binder, in mathcomp.ssreflect.seq]
s2:1887 [binder, in mathcomp.ssreflect.seq]
s2:1891 [binder, in mathcomp.ssreflect.seq]
s2:1893 [binder, in mathcomp.ssreflect.seq]
s2:1895 [binder, in mathcomp.ssreflect.seq]
s2:1897 [binder, in mathcomp.ssreflect.seq]
s2:1905 [binder, in mathcomp.ssreflect.seq]
s2:1908 [binder, in mathcomp.ssreflect.seq]
s2:1910 [binder, in mathcomp.ssreflect.seq]
s2:1913 [binder, in mathcomp.ssreflect.seq]
s2:1917 [binder, in mathcomp.ssreflect.seq]
s2:1920 [binder, in mathcomp.ssreflect.seq]
s2:1922 [binder, in mathcomp.ssreflect.seq]
s2:1925 [binder, in mathcomp.ssreflect.seq]
s2:1927 [binder, in mathcomp.ssreflect.seq]
s2:1930 [binder, in mathcomp.ssreflect.seq]
s2:1933 [binder, in mathcomp.ssreflect.seq]
s2:1936 [binder, in mathcomp.ssreflect.seq]
s2:1939 [binder, in mathcomp.ssreflect.seq]
s2:1942 [binder, in mathcomp.ssreflect.seq]
s2:1946 [binder, in mathcomp.ssreflect.seq]
s2:1948 [binder, in mathcomp.ssreflect.seq]
s2:195 [binder, in mathcomp.ssreflect.seq]
s2:1958 [binder, in mathcomp.ssreflect.seq]
s2:1960 [binder, in mathcomp.ssreflect.seq]
s2:1962 [binder, in mathcomp.ssreflect.seq]
s2:1974 [binder, in mathcomp.ssreflect.seq]
s2:1977 [binder, in mathcomp.ssreflect.seq]
s2:1980 [binder, in mathcomp.ssreflect.seq]
s2:1982 [binder, in mathcomp.ssreflect.seq]
s2:1984 [binder, in mathcomp.ssreflect.seq]
s2:1986 [binder, in mathcomp.ssreflect.seq]
s2:2083 [binder, in mathcomp.ssreflect.seq]
s2:217 [binder, in mathcomp.ssreflect.seq]
s2:22 [binder, in mathcomp.solvable.jordanholder]
s2:221 [binder, in mathcomp.ssreflect.seq]
s2:2210 [binder, in mathcomp.ssreflect.seq]
s2:2224 [binder, in mathcomp.ssreflect.seq]
s2:223 [binder, in mathcomp.ssreflect.seq]
s2:227 [binder, in mathcomp.ssreflect.seq]
s2:233 [binder, in mathcomp.fingroup.perm]
s2:235 [binder, in mathcomp.fingroup.perm]
s2:238 [binder, in mathcomp.fingroup.perm]
s2:2396 [binder, in mathcomp.ssreflect.seq]
s2:2409 [binder, in mathcomp.ssreflect.seq]
s2:247 [binder, in mathcomp.ssreflect.path]
s2:249 [binder, in mathcomp.ssreflect.path]
s2:251 [binder, in mathcomp.ssreflect.path]
s2:253 [binder, in mathcomp.ssreflect.path]
s2:254 [binder, in mathcomp.ssreflect.fintype]
s2:2553 [binder, in mathcomp.ssreflect.seq]
s2:2558 [binder, in mathcomp.ssreflect.seq]
s2:2563 [binder, in mathcomp.ssreflect.seq]
s2:2569 [binder, in mathcomp.ssreflect.seq]
s2:2574 [binder, in mathcomp.ssreflect.seq]
s2:258 [binder, in mathcomp.ssreflect.path]
s2:2581 [binder, in mathcomp.ssreflect.seq]
s2:260 [binder, in mathcomp.ssreflect.path]
s2:261 [binder, in mathcomp.ssreflect.fintype]
S2:2629 [binder, in mathcomp.algebra.matrix]
s2:2678 [binder, in mathcomp.ssreflect.seq]
s2:268 [binder, in mathcomp.ssreflect.fintype]
s2:270 [binder, in mathcomp.ssreflect.path]
s2:272 [binder, in mathcomp.ssreflect.path]
s2:275 [binder, in mathcomp.ssreflect.path]
s2:277 [binder, in mathcomp.ssreflect.path]
s2:292 [binder, in mathcomp.ssreflect.path]
s2:294 [binder, in mathcomp.ssreflect.path]
s2:299 [binder, in mathcomp.ssreflect.seq]
s2:302 [binder, in mathcomp.ssreflect.seq]
s2:327 [binder, in mathcomp.ssreflect.seq]
s2:330 [binder, in mathcomp.ssreflect.seq]
s2:332 [binder, in mathcomp.ssreflect.seq]
s2:354 [binder, in mathcomp.ssreflect.fintype]
s2:359 [binder, in mathcomp.ssreflect.fintype]
s2:36 [binder, in mathcomp.ssreflect.seq]
s2:384 [binder, in mathcomp.ssreflect.seq]
s2:388 [binder, in mathcomp.ssreflect.seq]
S2:416 [binder, in mathcomp.algebra.vector]
s2:44 [binder, in mathcomp.ssreflect.seq]
s2:440 [binder, in mathcomp.ssreflect.path]
s2:4434 [binder, in mathcomp.ssreflect.order]
s2:4439 [binder, in mathcomp.ssreflect.order]
s2:4447 [binder, in mathcomp.ssreflect.order]
s2:4450 [binder, in mathcomp.ssreflect.order]
s2:4455 [binder, in mathcomp.ssreflect.order]
s2:4467 [binder, in mathcomp.ssreflect.order]
s2:4473 [binder, in mathcomp.ssreflect.order]
s2:4475 [binder, in mathcomp.ssreflect.order]
s2:448 [binder, in mathcomp.ssreflect.seq]
s2:4481 [binder, in mathcomp.ssreflect.order]
s2:4496 [binder, in mathcomp.ssreflect.order]
s2:45 [binder, in mathcomp.solvable.jordanholder]
s2:4501 [binder, in mathcomp.ssreflect.order]
s2:4506 [binder, in mathcomp.ssreflect.order]
s2:4508 [binder, in mathcomp.ssreflect.order]
s2:4512 [binder, in mathcomp.ssreflect.order]
s2:4522 [binder, in mathcomp.ssreflect.order]
s2:4526 [binder, in mathcomp.ssreflect.order]
s2:4530 [binder, in mathcomp.ssreflect.order]
s2:4534 [binder, in mathcomp.ssreflect.order]
s2:4537 [binder, in mathcomp.ssreflect.order]
s2:4540 [binder, in mathcomp.ssreflect.order]
s2:4544 [binder, in mathcomp.ssreflect.order]
s2:4548 [binder, in mathcomp.ssreflect.order]
s2:457 [binder, in mathcomp.ssreflect.seq]
s2:463 [binder, in mathcomp.ssreflect.path]
s2:464 [binder, in mathcomp.ssreflect.seq]
s2:465 [binder, in mathcomp.ssreflect.path]
s2:466 [binder, in mathcomp.ssreflect.seq]
s2:470 [binder, in mathcomp.ssreflect.seq]
s2:481 [binder, in mathcomp.ssreflect.path]
s2:483 [binder, in mathcomp.ssreflect.path]
S2:485 [binder, in mathcomp.character.classfun]
s2:489 [binder, in mathcomp.ssreflect.path]
S2:491 [binder, in mathcomp.character.classfun]
s2:491 [binder, in mathcomp.ssreflect.path]
S2:493 [binder, in mathcomp.character.classfun]
s2:507 [binder, in mathcomp.ssreflect.path]
s2:509 [binder, in mathcomp.ssreflect.path]
s2:513 [binder, in mathcomp.ssreflect.seq]
s2:514 [binder, in mathcomp.ssreflect.path]
S2:522 [binder, in mathcomp.character.classfun]
s2:523 [binder, in mathcomp.ssreflect.path]
s2:525 [binder, in mathcomp.ssreflect.path]
s2:527 [binder, in mathcomp.ssreflect.path]
s2:53 [binder, in mathcomp.ssreflect.seq]
S2:53 [binder, in mathcomp.solvable.primitive_action]
s2:533 [binder, in mathcomp.ssreflect.path]
s2:534 [binder, in mathcomp.ssreflect.order]
s2:537 [binder, in mathcomp.ssreflect.path]
s2:537 [binder, in mathcomp.ssreflect.order]
S2:539 [binder, in mathcomp.character.classfun]
s2:539 [binder, in mathcomp.ssreflect.order]
s2:541 [binder, in mathcomp.ssreflect.order]
s2:544 [binder, in mathcomp.ssreflect.order]
s2:546 [binder, in mathcomp.ssreflect.order]
s2:549 [binder, in mathcomp.ssreflect.path]
S2:557 [binder, in mathcomp.algebra.poly]
s2:56 [binder, in mathcomp.ssreflect.seq]
s2:570 [binder, in mathcomp.ssreflect.seq]
s2:572 [binder, in mathcomp.ssreflect.seq]
s2:574 [binder, in mathcomp.ssreflect.seq]
s2:58 [binder, in mathcomp.ssreflect.seq]
s2:602 [binder, in mathcomp.ssreflect.seq]
s2:604 [binder, in mathcomp.ssreflect.seq]
s2:606 [binder, in mathcomp.ssreflect.seq]
s2:620 [binder, in mathcomp.ssreflect.seq]
s2:622 [binder, in mathcomp.ssreflect.seq]
S2:65 [binder, in mathcomp.fingroup.perm]
s2:656 [binder, in mathcomp.ssreflect.seq]
s2:661 [binder, in mathcomp.ssreflect.path]
s2:665 [binder, in mathcomp.ssreflect.path]
s2:682 [binder, in mathcomp.ssreflect.seq]
s2:687 [binder, in mathcomp.ssreflect.seq]
s2:690 [binder, in mathcomp.ssreflect.seq]
s2:695 [binder, in mathcomp.ssreflect.seq]
s2:698 [binder, in mathcomp.ssreflect.seq]
s2:703 [binder, in mathcomp.ssreflect.seq]
s2:708 [binder, in mathcomp.ssreflect.seq]
S2:71 [binder, in mathcomp.character.vcharacter]
s2:713 [binder, in mathcomp.ssreflect.seq]
s2:718 [binder, in mathcomp.ssreflect.seq]
s2:723 [binder, in mathcomp.ssreflect.seq]
S2:75 [binder, in mathcomp.character.vcharacter]
s2:792 [binder, in mathcomp.ssreflect.seq]
S2:80 [binder, in mathcomp.character.vcharacter]
s2:803 [binder, in mathcomp.ssreflect.seq]
s2:810 [binder, in mathcomp.ssreflect.seq]
s2:829 [binder, in mathcomp.ssreflect.seq]
S2:83 [binder, in mathcomp.character.vcharacter]
s2:832 [binder, in mathcomp.ssreflect.seq]
s2:836 [binder, in mathcomp.ssreflect.seq]
s2:838 [binder, in mathcomp.ssreflect.seq]
s2:840 [binder, in mathcomp.ssreflect.seq]
s2:842 [binder, in mathcomp.ssreflect.seq]
s2:844 [binder, in mathcomp.ssreflect.seq]
s2:851 [binder, in mathcomp.ssreflect.seq]
s2:853 [binder, in mathcomp.ssreflect.seq]
s2:856 [binder, in mathcomp.ssreflect.seq]
s2:859 [binder, in mathcomp.ssreflect.seq]
s2:863 [binder, in mathcomp.ssreflect.seq]
s2:866 [binder, in mathcomp.ssreflect.seq]
s2:869 [binder, in mathcomp.ssreflect.seq]
s2:87 [binder, in mathcomp.ssreflect.seq]
s2:880 [binder, in mathcomp.ssreflect.seq]
s2:885 [binder, in mathcomp.ssreflect.seq]
s2:887 [binder, in mathcomp.ssreflect.seq]
s2:895 [binder, in mathcomp.ssreflect.seq]
s2:898 [binder, in mathcomp.ssreflect.seq]
s2:901 [binder, in mathcomp.ssreflect.seq]
s2:903 [binder, in mathcomp.ssreflect.seq]
s2:905 [binder, in mathcomp.ssreflect.seq]
s2:909 [binder, in mathcomp.ssreflect.seq]
s2:911 [binder, in mathcomp.ssreflect.seq]
s2:913 [binder, in mathcomp.ssreflect.seq]
s2:915 [binder, in mathcomp.ssreflect.seq]
s2:917 [binder, in mathcomp.ssreflect.seq]
s2:919 [binder, in mathcomp.ssreflect.seq]
s2:924 [binder, in mathcomp.ssreflect.seq]
s2:927 [binder, in mathcomp.ssreflect.seq]
s2:93 [binder, in mathcomp.ssreflect.seq]
s2:930 [binder, in mathcomp.ssreflect.seq]
s2:934 [binder, in mathcomp.ssreflect.seq]
s2:937 [binder, in mathcomp.ssreflect.seq]
s2:944 [binder, in mathcomp.ssreflect.seq]
s2:99 [binder, in mathcomp.ssreflect.seq]
s3 [definition, in mathcomp.solvable.burnside_app]
S3 [definition, in mathcomp.solvable.burnside_app]
S3f [definition, in mathcomp.solvable.burnside_app]
S3_inv [lemma, in mathcomp.solvable.burnside_app]
s3':1842 [binder, in mathcomp.ssreflect.seq]
s3:1078 [binder, in mathcomp.ssreflect.seq]
s3:1244 [binder, in mathcomp.ssreflect.seq]
s3:1249 [binder, in mathcomp.ssreflect.seq]
s3:1799 [binder, in mathcomp.ssreflect.seq]
s3:1809 [binder, in mathcomp.ssreflect.seq]
s3:1812 [binder, in mathcomp.ssreflect.seq]
s3:1841 [binder, in mathcomp.ssreflect.seq]
s3:1845 [binder, in mathcomp.ssreflect.seq]
s3:1882 [binder, in mathcomp.ssreflect.seq]
s3:1923 [binder, in mathcomp.ssreflect.seq]
s3:1926 [binder, in mathcomp.ssreflect.seq]
s3:1929 [binder, in mathcomp.ssreflect.seq]
s3:1932 [binder, in mathcomp.ssreflect.seq]
s3:1935 [binder, in mathcomp.ssreflect.seq]
s3:1938 [binder, in mathcomp.ssreflect.seq]
s3:1941 [binder, in mathcomp.ssreflect.seq]
s3:1944 [binder, in mathcomp.ssreflect.seq]
s3:262 [binder, in mathcomp.ssreflect.fintype]
s3:467 [binder, in mathcomp.ssreflect.seq]
s3:54 [binder, in mathcomp.ssreflect.seq]
s3:607 [binder, in mathcomp.ssreflect.seq]
s3:699 [binder, in mathcomp.ssreflect.seq]
s3:704 [binder, in mathcomp.ssreflect.seq]
s3:709 [binder, in mathcomp.ssreflect.seq]
s3:714 [binder, in mathcomp.ssreflect.seq]
s3:719 [binder, in mathcomp.ssreflect.seq]
s3:724 [binder, in mathcomp.ssreflect.seq]
s3:845 [binder, in mathcomp.ssreflect.seq]
s3:854 [binder, in mathcomp.ssreflect.seq]
s3:864 [binder, in mathcomp.ssreflect.seq]
s3:867 [binder, in mathcomp.ssreflect.seq]
s3:870 [binder, in mathcomp.ssreflect.seq]
s3:928 [binder, in mathcomp.ssreflect.seq]
s3:935 [binder, in mathcomp.ssreflect.seq]
s4 [definition, in mathcomp.solvable.burnside_app]
S4 [definition, in mathcomp.solvable.burnside_app]
S4f [definition, in mathcomp.solvable.burnside_app]
S4_inv [lemma, in mathcomp.solvable.burnside_app]
s4:1079 [binder, in mathcomp.ssreflect.seq]
s4:1245 [binder, in mathcomp.ssreflect.seq]
s4:468 [binder, in mathcomp.ssreflect.seq]
s4:700 [binder, in mathcomp.ssreflect.seq]
s4:705 [binder, in mathcomp.ssreflect.seq]
s4:710 [binder, in mathcomp.ssreflect.seq]
s4:715 [binder, in mathcomp.ssreflect.seq]
s4:720 [binder, in mathcomp.ssreflect.seq]
s4:725 [binder, in mathcomp.ssreflect.seq]
s4:871 [binder, in mathcomp.ssreflect.seq]
s5 [definition, in mathcomp.solvable.burnside_app]
S5 [definition, in mathcomp.solvable.burnside_app]
S5f [definition, in mathcomp.solvable.burnside_app]
S5_inv [lemma, in mathcomp.solvable.burnside_app]
s6 [definition, in mathcomp.solvable.burnside_app]
S6 [definition, in mathcomp.solvable.burnside_app]
S6f [definition, in mathcomp.solvable.burnside_app]
S6_inv [lemma, in mathcomp.solvable.burnside_app]
s:1 [binder, in mathcomp.field.algnum]
s:10 [binder, in mathcomp.ssreflect.seq]
s:10 [binder, in mathcomp.ssreflect.ssrAC]
s:10 [binder, in mathcomp.fingroup.presentation]
s:1001 [binder, in mathcomp.ssreflect.seq]
s:1004 [binder, in mathcomp.ssreflect.seq]
s:101 [binder, in mathcomp.solvable.jordanholder]
s:101 [binder, in mathcomp.ssreflect.path]
s:1010 [binder, in mathcomp.ssreflect.seq]
S:1011 [binder, in mathcomp.character.classfun]
s:1012 [binder, in mathcomp.ssreflect.seq]
s:1020 [binder, in mathcomp.ssreflect.seq]
s:1023 [binder, in mathcomp.ssreflect.seq]
s:1028 [binder, in mathcomp.ssreflect.seq]
s:103 [binder, in mathcomp.solvable.jordanholder]
s:1031 [binder, in mathcomp.ssreflect.seq]
s:1033 [binder, in mathcomp.ssreflect.seq]
s:1035 [binder, in mathcomp.ssreflect.seq]
s:1035 [binder, in mathcomp.algebra.ssralg]
s:1037 [binder, in mathcomp.ssreflect.seq]
s:1041 [binder, in mathcomp.ssreflect.seq]
s:1041 [binder, in mathcomp.algebra.ssralg]
s:1043 [binder, in mathcomp.ssreflect.seq]
s:1045 [binder, in mathcomp.algebra.matrix]
s:1046 [binder, in mathcomp.algebra.ssralg]
s:1048 [binder, in mathcomp.algebra.matrix]
s:105 [binder, in mathcomp.ssreflect.seq]
s:1050 [binder, in mathcomp.ssreflect.seq]
s:1053 [binder, in mathcomp.ssreflect.seq]
s:1054 [binder, in mathcomp.algebra.ssralg]
s:1056 [binder, in mathcomp.ssreflect.seq]
s:1057 [binder, in mathcomp.ssreflect.seq]
s:1060 [binder, in mathcomp.ssreflect.seq]
s:1065 [binder, in mathcomp.algebra.ssralg]
s:1067 [binder, in mathcomp.ssreflect.seq]
s:1068 [binder, in mathcomp.ssreflect.seq]
s:1069 [binder, in mathcomp.ssreflect.seq]
s:107 [binder, in mathcomp.ssreflect.seq]
s:1071 [binder, in mathcomp.algebra.ssralg]
s:1075 [binder, in mathcomp.ssreflect.seq]
s:108 [binder, in mathcomp.fingroup.perm]
s:108 [binder, in mathcomp.ssreflect.finset]
S:108 [binder, in mathcomp.fingroup.morphism]
s:1081 [binder, in mathcomp.algebra.ssralg]
s:1085 [binder, in mathcomp.ssreflect.seq]
s:1086 [binder, in mathcomp.algebra.ssralg]
s:1088 [binder, in mathcomp.ssreflect.seq]
s:109 [binder, in mathcomp.fingroup.perm]
s:109 [binder, in mathcomp.ssreflect.seq]
S:109 [binder, in mathcomp.fingroup.action]
S:109 [binder, in mathcomp.character.classfun]
s:109 [binder, in mathcomp.ssreflect.path]
s:1091 [binder, in mathcomp.algebra.ssralg]
s:1094 [binder, in mathcomp.ssreflect.seq]
s:1099 [binder, in mathcomp.ssreflect.seq]
s:11 [binder, in mathcomp.solvable.jordanholder]
S:110 [binder, in mathcomp.fingroup.action]
S:110 [binder, in mathcomp.fingroup.morphism]
s:1102 [binder, in mathcomp.algebra.ssralg]
s:1104 [binder, in mathcomp.ssreflect.seq]
s:1108 [binder, in mathcomp.ssreflect.seq]
s:111 [binder, in mathcomp.ssreflect.seq]
S:111 [binder, in mathcomp.fingroup.action]
s:1110 [binder, in mathcomp.ssreflect.seq]
s:1112 [binder, in mathcomp.ssreflect.seq]
s:1115 [binder, in mathcomp.ssreflect.seq]
s:1118 [binder, in mathcomp.ssreflect.seq]
s:112 [binder, in mathcomp.ssreflect.seq]
S:112 [binder, in mathcomp.fingroup.morphism]
s:1122 [binder, in mathcomp.ssreflect.seq]
s:1128 [binder, in mathcomp.ssreflect.seq]
s:1132 [binder, in mathcomp.ssreflect.seq]
s:1133 [binder, in mathcomp.ssreflect.seq]
s:1134 [binder, in mathcomp.ssreflect.seq]
s:1135 [binder, in mathcomp.ssreflect.seq]
s:1137 [binder, in mathcomp.ssreflect.seq]
s:1138 [binder, in mathcomp.ssreflect.seq]
s:1139 [binder, in mathcomp.ssreflect.seq]
s:1140 [binder, in mathcomp.ssreflect.seq]
s:1142 [binder, in mathcomp.ssreflect.seq]
s:1143 [binder, in mathcomp.ssreflect.seq]
s:1144 [binder, in mathcomp.ssreflect.seq]
s:1145 [binder, in mathcomp.ssreflect.seq]
s:1147 [binder, in mathcomp.ssreflect.seq]
s:1149 [binder, in mathcomp.ssreflect.seq]
s:1156 [binder, in mathcomp.ssreflect.seq]
s:116 [binder, in mathcomp.algebra.matrix]
S:116 [binder, in mathcomp.fingroup.action]
s:1160 [binder, in mathcomp.ssreflect.seq]
s:1160 [binder, in mathcomp.algebra.poly]
s:1164 [binder, in mathcomp.ssreflect.seq]
s:1165 [binder, in mathcomp.ssreflect.seq]
s:1165 [binder, in mathcomp.ssreflect.ssrnat]
s:1167 [binder, in mathcomp.ssreflect.seq]
s:1168 [binder, in mathcomp.ssreflect.seq]
s:117 [binder, in mathcomp.ssreflect.seq]
S:117 [binder, in mathcomp.fingroup.action]
s:117 [binder, in mathcomp.ssreflect.path]
s:1170 [binder, in mathcomp.ssreflect.seq]
s:1172 [binder, in mathcomp.ssreflect.seq]
s:1172 [binder, in mathcomp.algebra.poly]
s:1175 [binder, in mathcomp.ssreflect.seq]
s:1177 [binder, in mathcomp.ssreflect.seq]
s:1179 [binder, in mathcomp.ssreflect.seq]
s:118 [binder, in mathcomp.algebra.matrix]
S:118 [binder, in mathcomp.fingroup.action]
s:1181 [binder, in mathcomp.ssreflect.seq]
s:1183 [binder, in mathcomp.ssreflect.seq]
s:1186 [binder, in mathcomp.ssreflect.seq]
s:1186 [binder, in mathcomp.ssreflect.ssrnat]
s:1187 [binder, in mathcomp.ssreflect.seq]
s:1188 [binder, in mathcomp.ssreflect.seq]
s:1189 [binder, in mathcomp.ssreflect.seq]
s:119 [binder, in mathcomp.algebra.interval]
s:1190 [binder, in mathcomp.ssreflect.seq]
s:1191 [binder, in mathcomp.ssreflect.seq]
s:1193 [binder, in mathcomp.ssreflect.seq]
s:1194 [binder, in mathcomp.algebra.ssralg]
s:1195 [binder, in mathcomp.ssreflect.seq]
S:12 [binder, in mathcomp.character.vcharacter]
s:12 [binder, in mathcomp.ssreflect.seq]
s:120 [binder, in mathcomp.fingroup.perm]
s:1200 [binder, in mathcomp.algebra.ssralg]
s:1206 [binder, in mathcomp.ssreflect.seq]
s:1209 [binder, in mathcomp.ssreflect.seq]
S:121 [binder, in mathcomp.fingroup.action]
s:121 [binder, in mathcomp.ssreflect.path]
s:1214 [binder, in mathcomp.ssreflect.seq]
s:1216 [binder, in mathcomp.ssreflect.seq]
S:122 [binder, in mathcomp.fingroup.action]
s:123 [binder, in mathcomp.fingroup.perm]
s:123 [binder, in mathcomp.ssreflect.seq]
S:123 [binder, in mathcomp.fingroup.action]
s:123 [binder, in mathcomp.ssreflect.path]
s:123 [binder, in mathcomp.field.algnum]
s:1231 [binder, in mathcomp.ssreflect.seq]
s:1232 [binder, in mathcomp.ssreflect.seq]
s:1235 [binder, in mathcomp.ssreflect.seq]
s:124 [binder, in mathcomp.ssreflect.seq]
s:124 [binder, in mathcomp.ssreflect.path]
s:1246 [binder, in mathcomp.ssreflect.seq]
S:125 [binder, in mathcomp.fingroup.action]
s:1253 [binder, in mathcomp.ssreflect.order]
s:1254 [binder, in mathcomp.ssreflect.order]
s:1258 [binder, in mathcomp.ssreflect.order]
s:1259 [binder, in mathcomp.ssreflect.order]
s:126 [binder, in mathcomp.ssreflect.seq]
s:126 [binder, in mathcomp.ssreflect.path]
s:1261 [binder, in mathcomp.ssreflect.seq]
s:1262 [binder, in mathcomp.ssreflect.order]
s:1263 [binder, in mathcomp.ssreflect.seq]
s:1267 [binder, in mathcomp.ssreflect.seq]
S:127 [binder, in mathcomp.fingroup.action]
s:1271 [binder, in mathcomp.ssreflect.seq]
s:1271 [binder, in mathcomp.ssreflect.order]
S:1271 [binder, in mathcomp.algebra.mxalgebra]
s:1272 [binder, in mathcomp.ssreflect.seq]
S:1274 [binder, in mathcomp.algebra.mxalgebra]
s:1275 [binder, in mathcomp.ssreflect.seq]
s:1278 [binder, in mathcomp.ssreflect.seq]
s:128 [binder, in mathcomp.ssreflect.path]
s:128 [binder, in mathcomp.solvable.burnside_app]
s:1283 [binder, in mathcomp.algebra.poly]
s:1285 [binder, in mathcomp.ssreflect.seq]
s:1286 [binder, in mathcomp.algebra.ssrnum]
s:1287 [binder, in mathcomp.ssreflect.seq]
s:1287 [binder, in mathcomp.algebra.ssrnum]
s:1289 [binder, in mathcomp.ssreflect.seq]
s:1290 [binder, in mathcomp.ssreflect.seq]
s:1291 [binder, in mathcomp.ssreflect.seq]
s:1295 [binder, in mathcomp.ssreflect.seq]
S:1295 [binder, in mathcomp.algebra.mxalgebra]
s:13 [binder, in mathcomp.ssreflect.choice]
s:13 [binder, in mathcomp.ssreflect.finfun]
s:13 [binder, in mathcomp.solvable.jordanholder]
S:130 [binder, in mathcomp.fingroup.action]
s:130 [binder, in mathcomp.ssreflect.path]
S:1301 [binder, in mathcomp.algebra.mxalgebra]
s:1304 [binder, in mathcomp.ssreflect.seq]
S:1304 [binder, in mathcomp.algebra.mxalgebra]
S:1306 [binder, in mathcomp.algebra.ssralg]
S:1307 [binder, in mathcomp.algebra.mxalgebra]
s:1309 [binder, in mathcomp.ssreflect.seq]
s:131 [binder, in mathcomp.fingroup.perm]
s:1315 [binder, in mathcomp.ssreflect.seq]
S:1316 [binder, in mathcomp.ssreflect.seq]
s:1316 [binder, in mathcomp.algebra.poly]
S:132 [binder, in mathcomp.fingroup.action]
s:132 [binder, in mathcomp.solvable.burnside_app]
s:1320 [binder, in mathcomp.ssreflect.seq]
s:1323 [binder, in mathcomp.ssreflect.seq]
s:1328 [binder, in mathcomp.ssreflect.seq]
s:1328 [binder, in mathcomp.ssreflect.bigop]
s:1329 [binder, in mathcomp.ssreflect.bigop]
s:133 [binder, in mathcomp.fingroup.perm]
s:133 [binder, in mathcomp.ssreflect.seq]
s:133 [binder, in mathcomp.field.algebraics_fundamentals]
s:133 [binder, in mathcomp.ssreflect.path]
s:1330 [binder, in mathcomp.ssreflect.bigop]
s:1331 [binder, in mathcomp.ssreflect.bigop]
s:1332 [binder, in mathcomp.ssreflect.seq]
s:1332 [binder, in mathcomp.ssreflect.bigop]
s:1333 [binder, in mathcomp.ssreflect.seq]
s:1335 [binder, in mathcomp.ssreflect.seq]
s:1336 [binder, in mathcomp.ssreflect.seq]
s:1339 [binder, in mathcomp.ssreflect.seq]
s:134 [binder, in mathcomp.ssreflect.seq]
S:134 [binder, in mathcomp.algebra.ring_quotient]
S:134 [binder, in mathcomp.fingroup.action]
s:134 [binder, in mathcomp.solvable.burnside_app]
s:1345 [binder, in mathcomp.ssreflect.seq]
s:135 [binder, in mathcomp.ssreflect.seq]
s:1354 [binder, in mathcomp.ssreflect.seq]
s:1357 [binder, in mathcomp.ssreflect.seq]
s:1359 [binder, in mathcomp.ssreflect.seq]
s:136 [binder, in mathcomp.fingroup.perm]
s:136 [binder, in mathcomp.ssreflect.path]
s:1360 [binder, in mathcomp.ssreflect.seq]
s:1365 [binder, in mathcomp.ssreflect.seq]
S:1367 [binder, in mathcomp.algebra.ssralg]
s:1369 [binder, in mathcomp.ssreflect.seq]
S:137 [binder, in mathcomp.character.character]
s:1371 [binder, in mathcomp.ssreflect.seq]
s:138 [binder, in mathcomp.fingroup.perm]
S:138 [binder, in mathcomp.algebra.ring_quotient]
s:138 [binder, in mathcomp.ssreflect.path]
S:1381 [binder, in mathcomp.algebra.ssralg]
S:139 [binder, in mathcomp.algebra.archimedean]
s:14 [binder, in mathcomp.fingroup.perm]
s:14 [binder, in mathcomp.ssreflect.seq]
s:140 [binder, in mathcomp.fingroup.perm]
s:140 [binder, in mathcomp.ssreflect.seq]
s:1406 [binder, in mathcomp.algebra.matrix]
s:1409 [binder, in mathcomp.algebra.matrix]
s:141 [binder, in mathcomp.fingroup.perm]
S:141 [binder, in mathcomp.fingroup.action]
s:1414 [binder, in mathcomp.ssreflect.order]
s:1416 [binder, in mathcomp.ssreflect.order]
s:142 [binder, in mathcomp.field.algebraics_fundamentals]
S:142 [binder, in mathcomp.algebra.ring_quotient]
S:142 [binder, in mathcomp.fingroup.morphism]
s:1420 [binder, in mathcomp.ssreflect.seq]
s:1421 [binder, in mathcomp.ssreflect.seq]
s:1426 [binder, in mathcomp.ssreflect.seq]
s:1427 [binder, in mathcomp.ssreflect.seq]
s:143 [binder, in mathcomp.ssreflect.seq]
s:1431 [binder, in mathcomp.ssreflect.seq]
s:144 [binder, in mathcomp.fingroup.perm]
s:1441 [binder, in mathcomp.ssreflect.seq]
s:1451 [binder, in mathcomp.ssreflect.seq]
s:146 [binder, in mathcomp.fingroup.perm]
s:146 [binder, in mathcomp.algebra.matrix]
S:146 [binder, in mathcomp.fingroup.action]
s:146 [binder, in mathcomp.ssreflect.path]
s:1462 [binder, in mathcomp.ssreflect.seq]
s:1464 [binder, in mathcomp.ssreflect.seq]
s:1469 [binder, in mathcomp.ssreflect.seq]
s:147 [binder, in mathcomp.ssreflect.seq]
s:147 [binder, in mathcomp.field.algebraics_fundamentals]
S:147 [binder, in mathcomp.algebra.ring_quotient]
s:1476 [binder, in mathcomp.ssreflect.seq]
s:1479 [binder, in mathcomp.ssreflect.seq]
s:148 [binder, in mathcomp.fingroup.perm]
s:1483 [binder, in mathcomp.ssreflect.seq]
s:1485 [binder, in mathcomp.ssreflect.seq]
s:1486 [binder, in mathcomp.ssreflect.seq]
s:1487 [binder, in mathcomp.ssreflect.seq]
S:149 [binder, in mathcomp.algebra.ring_quotient]
s:149 [binder, in mathcomp.algebra.matrix]
s:1491 [binder, in mathcomp.ssreflect.seq]
s:1495 [binder, in mathcomp.ssreflect.seq]
s:15 [binder, in mathcomp.solvable.finmodule]
s:15 [binder, in mathcomp.solvable.extremal]
s:150 [binder, in mathcomp.fingroup.perm]
S:150 [binder, in mathcomp.fingroup.morphism]
s:1502 [binder, in mathcomp.ssreflect.seq]
s:1506 [binder, in mathcomp.ssreflect.seq]
S:151 [binder, in mathcomp.algebra.ring_quotient]
s:1513 [binder, in mathcomp.ssreflect.seq]
s:152 [binder, in mathcomp.fingroup.perm]
s:152 [binder, in mathcomp.algebra.matrix]
s:1528 [binder, in mathcomp.ssreflect.seq]
s:153 [binder, in mathcomp.ssreflect.path]
s:1530 [binder, in mathcomp.algebra.ssrnum]
s:1532 [binder, in mathcomp.ssreflect.seq]
s:1533 [binder, in mathcomp.algebra.ssrnum]
s:1534 [binder, in mathcomp.ssreflect.bigop]
s:1536 [binder, in mathcomp.ssreflect.seq]
s:1538 [binder, in mathcomp.algebra.ssralg]
s:154 [binder, in mathcomp.fingroup.perm]
S:154 [binder, in mathcomp.fingroup.morphism]
s:154 [binder, in mathcomp.solvable.burnside_app]
s:1540 [binder, in mathcomp.ssreflect.seq]
s:1542 [binder, in mathcomp.algebra.ssralg]
s:1545 [binder, in mathcomp.ssreflect.seq]
s:155 [binder, in mathcomp.ssreflect.seq]
s:155 [binder, in mathcomp.field.separable]
s:1552 [binder, in mathcomp.ssreflect.seq]
s:1555 [binder, in mathcomp.ssreflect.seq]
s:1557 [binder, in mathcomp.algebra.ssralg]
S:156 [binder, in mathcomp.algebra.ring_quotient]
s:156 [binder, in mathcomp.ssreflect.path]
s:1565 [binder, in mathcomp.ssreflect.seq]
s:157 [binder, in mathcomp.fingroup.perm]
S:157 [binder, in mathcomp.solvable.frobenius]
s:1570 [binder, in mathcomp.ssreflect.seq]
s:1575 [binder, in mathcomp.ssreflect.seq]
s:1576 [binder, in mathcomp.ssreflect.seq]
s:1578 [binder, in mathcomp.ssreflect.seq]
s:1580 [binder, in mathcomp.ssreflect.seq]
s:1582 [binder, in mathcomp.ssreflect.seq]
s:1584 [binder, in mathcomp.ssreflect.seq]
S:159 [binder, in mathcomp.algebra.archimedean]
S:159 [binder, in mathcomp.algebra.ring_quotient]
s:159 [binder, in mathcomp.algebra.matrix]
s:1592 [binder, in mathcomp.ssreflect.seq]
s:1596 [binder, in mathcomp.ssreflect.seq]
s:1599 [binder, in mathcomp.ssreflect.seq]
S:16 [binder, in mathcomp.character.vcharacter]
s:16 [binder, in mathcomp.fingroup.perm]
s:16 [binder, in mathcomp.ssreflect.seq]
s:160 [binder, in mathcomp.fingroup.perm]
s:160 [binder, in mathcomp.ssreflect.seq]
s:160 [binder, in mathcomp.algebra.matrix]
s:1603 [binder, in mathcomp.ssreflect.seq]
s:1605 [binder, in mathcomp.ssreflect.seq]
S:161 [binder, in mathcomp.character.classfun]
s:1611 [binder, in mathcomp.ssreflect.seq]
s:1616 [binder, in mathcomp.ssreflect.seq]
S:162 [binder, in mathcomp.algebra.ring_quotient]
s:1625 [binder, in mathcomp.ssreflect.seq]
s:163 [binder, in mathcomp.fingroup.perm]
s:163 [binder, in mathcomp.ssreflect.seq]
S:1632 [binder, in mathcomp.ssreflect.seq]
S:164 [binder, in mathcomp.algebra.archimedean]
S:164 [binder, in mathcomp.character.classfun]
S:1641 [binder, in mathcomp.ssreflect.seq]
S:1647 [binder, in mathcomp.ssreflect.seq]
S:165 [binder, in mathcomp.character.classfun]
s:165 [binder, in mathcomp.ssreflect.path]
s:1654 [binder, in mathcomp.ssreflect.seq]
s:166 [binder, in mathcomp.ssreflect.path]
s:166 [binder, in mathcomp.solvable.gseries]
s:1660 [binder, in mathcomp.ssreflect.seq]
s:1666 [binder, in mathcomp.ssreflect.seq]
S:167 [binder, in mathcomp.algebra.ring_quotient]
s:167 [binder, in mathcomp.ssreflect.path]
s:167 [binder, in mathcomp.solvable.gseries]
s:168 [binder, in mathcomp.fingroup.perm]
s:1680 [binder, in mathcomp.ssreflect.seq]
s:1681 [binder, in mathcomp.algebra.matrix]
s:1686 [binder, in mathcomp.ssreflect.seq]
s:1687 [binder, in mathcomp.algebra.matrix]
s:1688 [binder, in mathcomp.ssreflect.seq]
s:169 [binder, in mathcomp.ssreflect.path]
s:1690 [binder, in mathcomp.ssreflect.seq]
s:1691 [binder, in mathcomp.ssreflect.seq]
s:1698 [binder, in mathcomp.algebra.matrix]
s:17 [binder, in mathcomp.solvable.jordanholder]
s:17 [binder, in mathcomp.ssreflect.ssrAC]
s:17 [binder, in mathcomp.solvable.burnside_app]
s:170 [binder, in mathcomp.ssreflect.seq]
S:170 [binder, in mathcomp.algebra.ring_quotient]
s:1704 [binder, in mathcomp.algebra.matrix]
s:1708 [binder, in mathcomp.algebra.matrix]
s:1709 [binder, in mathcomp.ssreflect.seq]
s:1710 [binder, in mathcomp.ssreflect.seq]
s:172 [binder, in mathcomp.fingroup.perm]
s:1721 [binder, in mathcomp.algebra.matrix]
s:1726 [binder, in mathcomp.algebra.matrix]
s:173 [binder, in mathcomp.fingroup.perm]
s:173 [binder, in mathcomp.ssreflect.seq]
s:173 [binder, in mathcomp.field.algnum]
s:1732 [binder, in mathcomp.algebra.matrix]
s:1736 [binder, in mathcomp.algebra.matrix]
s:1737 [binder, in mathcomp.algebra.matrix]
s:1738 [binder, in mathcomp.algebra.matrix]
s:174 [binder, in mathcomp.fingroup.perm]
s:174 [binder, in mathcomp.ssreflect.path]
S:1741 [binder, in mathcomp.ssreflect.seq]
s:1741 [binder, in mathcomp.algebra.matrix]
s:1743 [binder, in mathcomp.algebra.matrix]
S:1745 [binder, in mathcomp.ssreflect.seq]
s:1748 [binder, in mathcomp.ssreflect.seq]
S:175 [binder, in mathcomp.character.vcharacter]
S:175 [binder, in mathcomp.algebra.ring_quotient]
s:1753 [binder, in mathcomp.ssreflect.seq]
S:1756 [binder, in mathcomp.ssreflect.seq]
s:1759 [binder, in mathcomp.ssreflect.seq]
s:176 [binder, in mathcomp.ssreflect.seq]
s:1764 [binder, in mathcomp.ssreflect.seq]
s:1765 [binder, in mathcomp.ssreflect.seq]
s:1767 [binder, in mathcomp.ssreflect.seq]
s:177 [binder, in mathcomp.fingroup.perm]
s:1789 [binder, in mathcomp.ssreflect.seq]
s:179 [binder, in mathcomp.ssreflect.seq]
s:179 [binder, in mathcomp.ssreflect.path]
s:1790 [binder, in mathcomp.ssreflect.seq]
s:1791 [binder, in mathcomp.ssreflect.seq]
S:18 [binder, in mathcomp.character.vcharacter]
s:180 [binder, in mathcomp.field.algnum]
s:1805 [binder, in mathcomp.ssreflect.seq]
s:181 [binder, in mathcomp.ssreflect.tuple]
S:181 [binder, in mathcomp.fingroup.action]
s:1813 [binder, in mathcomp.ssreflect.seq]
s:1819 [binder, in mathcomp.ssreflect.seq]
s:182 [binder, in mathcomp.ssreflect.seq]
s:182 [binder, in mathcomp.field.algnum]
s:1820 [binder, in mathcomp.ssreflect.seq]
s:1821 [binder, in mathcomp.ssreflect.seq]
s:1846 [binder, in mathcomp.ssreflect.seq]
s:1849 [binder, in mathcomp.ssreflect.seq]
s:185 [binder, in mathcomp.ssreflect.seq]
s:185 [binder, in mathcomp.ssreflect.path]
s:185 [binder, in mathcomp.field.algnum]
s:1859 [binder, in mathcomp.ssreflect.seq]
s:186 [binder, in mathcomp.ssreflect.seq]
s:186 [binder, in mathcomp.field.algnum]
s:1860 [binder, in mathcomp.ssreflect.seq]
s:1864 [binder, in mathcomp.ssreflect.seq]
s:187 [binder, in mathcomp.ssreflect.seq]
s:1871 [binder, in mathcomp.ssreflect.seq]
s:1872 [binder, in mathcomp.ssreflect.seq]
s:1875 [binder, in mathcomp.ssreflect.seq]
s:188 [binder, in mathcomp.ssreflect.seq]
s:1886 [binder, in mathcomp.algebra.matrix]
s:1887 [binder, in mathcomp.algebra.matrix]
s:1888 [binder, in mathcomp.ssreflect.seq]
s:1888 [binder, in mathcomp.algebra.matrix]
s:189 [binder, in mathcomp.ssreflect.seq]
s:1890 [binder, in mathcomp.algebra.matrix]
s:1891 [binder, in mathcomp.algebra.matrix]
s:1894 [binder, in mathcomp.algebra.matrix]
s:1895 [binder, in mathcomp.algebra.matrix]
s:1899 [binder, in mathcomp.ssreflect.seq]
s:19 [binder, in mathcomp.fingroup.perm]
s:19 [binder, in mathcomp.ssreflect.ssrAC]
s:190 [binder, in mathcomp.ssreflect.seq]
s:190 [binder, in mathcomp.ssreflect.path]
s:1901 [binder, in mathcomp.ssreflect.seq]
s:1903 [binder, in mathcomp.ssreflect.seq]
s:1906 [binder, in mathcomp.ssreflect.seq]
s:191 [binder, in mathcomp.ssreflect.seq]
s:1915 [binder, in mathcomp.ssreflect.seq]
s:1918 [binder, in mathcomp.ssreflect.seq]
s:192 [binder, in mathcomp.ssreflect.seq]
s:1926 [binder, in mathcomp.algebra.ssralg]
s:193 [binder, in mathcomp.ssreflect.seq]
s:1932 [binder, in mathcomp.algebra.matrix]
s:1939 [binder, in mathcomp.algebra.ssralg]
s:1946 [binder, in mathcomp.algebra.ssralg]
s:1947 [binder, in mathcomp.algebra.ssralg]
s:1949 [binder, in mathcomp.ssreflect.seq]
s:195 [binder, in mathcomp.ssreflect.path]
s:1951 [binder, in mathcomp.ssreflect.seq]
s:1953 [binder, in mathcomp.ssreflect.seq]
s:1955 [binder, in mathcomp.ssreflect.seq]
S:196 [binder, in mathcomp.fingroup.morphism]
s:1960 [binder, in mathcomp.algebra.matrix]
s:1963 [binder, in mathcomp.ssreflect.seq]
s:1965 [binder, in mathcomp.ssreflect.seq]
s:1967 [binder, in mathcomp.ssreflect.seq]
s:1969 [binder, in mathcomp.ssreflect.seq]
s:197 [binder, in mathcomp.ssreflect.fintype]
s:1971 [binder, in mathcomp.ssreflect.seq]
S:198 [binder, in mathcomp.fingroup.morphism]
s:198 [binder, in mathcomp.ssreflect.fintype]
s:199 [binder, in mathcomp.algebra.ssrnum]
s:1994 [binder, in mathcomp.ssreflect.seq]
s:2 [binder, in mathcomp.solvable.burnside_app]
S:20 [binder, in mathcomp.character.vcharacter]
s:20 [binder, in mathcomp.fingroup.perm]
s:20 [binder, in mathcomp.solvable.jordanholder]
S:200 [binder, in mathcomp.fingroup.morphism]
s:2001 [binder, in mathcomp.ssreflect.seq]
s:201 [binder, in mathcomp.character.integral_char]
s:201 [binder, in mathcomp.ssreflect.path]
s:2016 [binder, in mathcomp.ssreflect.seq]
S:202 [binder, in mathcomp.character.integral_char]
s:203 [binder, in mathcomp.character.integral_char]
s:2031 [binder, in mathcomp.ssreflect.seq]
s:204 [binder, in mathcomp.character.integral_char]
s:2041 [binder, in mathcomp.ssreflect.seq]
S:2043 [binder, in mathcomp.algebra.ssralg]
S:2048 [binder, in mathcomp.algebra.ssralg]
s:205 [binder, in mathcomp.character.integral_char]
S:2053 [binder, in mathcomp.algebra.ssralg]
s:2056 [binder, in mathcomp.ssreflect.seq]
S:2058 [binder, in mathcomp.algebra.ssralg]
s:206 [binder, in mathcomp.character.integral_char]
s:206 [binder, in mathcomp.field.galois]
S:2063 [binder, in mathcomp.algebra.ssralg]
s:2064 [binder, in mathcomp.algebra.matrix]
s:2067 [binder, in mathcomp.algebra.matrix]
s:2069 [binder, in mathcomp.ssreflect.seq]
S:2069 [binder, in mathcomp.algebra.ssralg]
s:207 [binder, in mathcomp.character.integral_char]
S:2075 [binder, in mathcomp.algebra.ssralg]
S:2078 [binder, in mathcomp.algebra.ssralg]
s:208 [binder, in mathcomp.character.integral_char]
S:2081 [binder, in mathcomp.algebra.ssralg]
S:2084 [binder, in mathcomp.algebra.ssralg]
S:2087 [binder, in mathcomp.algebra.ssralg]
s:209 [binder, in mathcomp.algebra.ssrnum]
S:2090 [binder, in mathcomp.algebra.ssralg]
S:2093 [binder, in mathcomp.algebra.ssralg]
S:2096 [binder, in mathcomp.algebra.ssralg]
s:2099 [binder, in mathcomp.ssreflect.seq]
S:2099 [binder, in mathcomp.algebra.ssralg]
s:21 [binder, in mathcomp.fingroup.perm]
s:210 [binder, in mathcomp.ssreflect.path]
S:2102 [binder, in mathcomp.algebra.ssralg]
S:2105 [binder, in mathcomp.algebra.ssralg]
S:2109 [binder, in mathcomp.algebra.ssralg]
s:211 [binder, in mathcomp.ssreflect.path]
s:2113 [binder, in mathcomp.ssreflect.seq]
S:2113 [binder, in mathcomp.algebra.ssralg]
S:2116 [binder, in mathcomp.algebra.ssralg]
s:212 [binder, in mathcomp.ssreflect.seq]
S:2120 [binder, in mathcomp.algebra.ssralg]
S:2123 [binder, in mathcomp.algebra.ssralg]
s:2126 [binder, in mathcomp.ssreflect.seq]
S:2128 [binder, in mathcomp.algebra.ssralg]
s:213 [binder, in mathcomp.fingroup.perm]
s:213 [binder, in mathcomp.ssreflect.seq]
S:2132 [binder, in mathcomp.algebra.ssralg]
S:2136 [binder, in mathcomp.ssreflect.seq]
S:2137 [binder, in mathcomp.algebra.ssralg]
S:2141 [binder, in mathcomp.algebra.ssralg]
s:2142 [binder, in mathcomp.ssreflect.seq]
S:2146 [binder, in mathcomp.algebra.ssralg]
s:215 [binder, in mathcomp.character.integral_char]
s:215 [binder, in mathcomp.ssreflect.seq]
S:2150 [binder, in mathcomp.algebra.ssralg]
s:2153 [binder, in mathcomp.ssreflect.bigop]
S:2155 [binder, in mathcomp.algebra.ssralg]
s:2156 [binder, in mathcomp.ssreflect.seq]
S:2159 [binder, in mathcomp.algebra.ssralg]
s:216 [binder, in mathcomp.character.integral_char]
s:216 [binder, in mathcomp.field.galois]
s:216 [binder, in mathcomp.ssreflect.path]
s:2162 [binder, in mathcomp.ssreflect.seq]
S:2164 [binder, in mathcomp.algebra.ssralg]
S:2168 [binder, in mathcomp.algebra.ssralg]
s:217 [binder, in mathcomp.character.integral_char]
s:217 [binder, in mathcomp.ssreflect.path]
s:217 [binder, in mathcomp.algebra.ssrnum]
S:2173 [binder, in mathcomp.algebra.ssralg]
s:2174 [binder, in mathcomp.ssreflect.seq]
S:2177 [binder, in mathcomp.algebra.ssralg]
s:218 [binder, in mathcomp.character.integral_char]
s:218 [binder, in mathcomp.fingroup.perm]
s:218 [binder, in mathcomp.ssreflect.seq]
S:2182 [binder, in mathcomp.algebra.ssralg]
s:2186 [binder, in mathcomp.ssreflect.seq]
S:2187 [binder, in mathcomp.algebra.ssralg]
s:219 [binder, in mathcomp.character.integral_char]
s:219 [binder, in mathcomp.ssreflect.path]
S:2194 [binder, in mathcomp.algebra.ssralg]
s:2196 [binder, in mathcomp.ssreflect.seq]
s:2198 [binder, in mathcomp.ssreflect.bigop]
s:2199 [binder, in mathcomp.ssreflect.bigop]
S:22 [binder, in mathcomp.character.vcharacter]
s:22 [binder, in mathcomp.ssreflect.choice]
s:220 [binder, in mathcomp.character.integral_char]
S:2200 [binder, in mathcomp.algebra.ssralg]
s:2200 [binder, in mathcomp.ssreflect.bigop]
s:2201 [binder, in mathcomp.ssreflect.bigop]
s:2202 [binder, in mathcomp.ssreflect.bigop]
S:2207 [binder, in mathcomp.algebra.ssralg]
s:221 [binder, in mathcomp.character.integral_char]
s:221 [binder, in mathcomp.ssreflect.choice]
S:2212 [binder, in mathcomp.algebra.ssralg]
S:2217 [binder, in mathcomp.algebra.ssralg]
s:222 [binder, in mathcomp.character.integral_char]
s:222 [binder, in mathcomp.solvable.cyclic]
S:2222 [binder, in mathcomp.algebra.ssralg]
s:2228 [binder, in mathcomp.algebra.matrix]
s:2229 [binder, in mathcomp.algebra.matrix]
S:2229 [binder, in mathcomp.algebra.ssralg]
s:223 [binder, in mathcomp.character.integral_char]
s:2230 [binder, in mathcomp.algebra.matrix]
s:2236 [binder, in mathcomp.ssreflect.seq]
s:224 [binder, in mathcomp.character.integral_char]
s:224 [binder, in mathcomp.ssreflect.seq]
S:225 [binder, in mathcomp.field.algC]
s:2258 [binder, in mathcomp.ssreflect.seq]
s:2274 [binder, in mathcomp.ssreflect.seq]
S:2278 [binder, in mathcomp.algebra.ssralg]
S:228 [binder, in mathcomp.character.vcharacter]
s:228 [binder, in mathcomp.ssreflect.seq]
s:228 [binder, in mathcomp.ssreflect.path]
s:228 [binder, in mathcomp.solvable.cyclic]
S:2282 [binder, in mathcomp.algebra.ssralg]
S:2285 [binder, in mathcomp.algebra.ssralg]
S:2286 [binder, in mathcomp.algebra.ssralg]
S:229 [binder, in mathcomp.fingroup.action]
s:229 [binder, in mathcomp.ssreflect.path]
s:2290 [binder, in mathcomp.ssreflect.seq]
S:2291 [binder, in mathcomp.algebra.ssralg]
S:2294 [binder, in mathcomp.algebra.ssralg]
s:23 [binder, in mathcomp.fingroup.perm]
s:23 [binder, in mathcomp.ssreflect.seq]
s:230 [binder, in mathcomp.ssreflect.seq]
s:230 [binder, in mathcomp.solvable.cyclic]
s:2304 [binder, in mathcomp.ssreflect.seq]
s:231 [binder, in mathcomp.character.integral_char]
s:231 [binder, in mathcomp.ssreflect.seq]
s:231 [binder, in mathcomp.ssreflect.choice]
s:2318 [binder, in mathcomp.ssreflect.seq]
s:232 [binder, in mathcomp.character.integral_char]
s:233 [binder, in mathcomp.character.integral_char]
S:233 [binder, in mathcomp.fingroup.action]
s:233 [binder, in mathcomp.solvable.cyclic]
S:2331 [binder, in mathcomp.algebra.ssralg]
s:2332 [binder, in mathcomp.ssreflect.seq]
S:2334 [binder, in mathcomp.algebra.ssralg]
s:234 [binder, in mathcomp.character.integral_char]
s:234 [binder, in mathcomp.ssreflect.path]
S:2344 [binder, in mathcomp.algebra.ssralg]
S:2345 [binder, in mathcomp.ssreflect.seq]
s:2345 [binder, in mathcomp.algebra.matrix]
s:235 [binder, in mathcomp.character.integral_char]
S:235 [binder, in mathcomp.character.vcharacter]
S:235 [binder, in mathcomp.fingroup.action]
s:235 [binder, in mathcomp.ssreflect.path]
s:235 [binder, in mathcomp.solvable.cyclic]
s:2351 [binder, in mathcomp.ssreflect.seq]
S:2351 [binder, in mathcomp.algebra.ssralg]
s:2351 [binder, in mathcomp.ssreflect.bigop]
S:2355 [binder, in mathcomp.algebra.ssralg]
s:236 [binder, in mathcomp.character.integral_char]
s:236 [binder, in mathcomp.fingroup.perm]
S:2362 [binder, in mathcomp.algebra.ssralg]
s:2363 [binder, in mathcomp.algebra.matrix]
s:2364 [binder, in mathcomp.ssreflect.seq]
s:2366 [binder, in mathcomp.ssreflect.bigop]
s:2369 [binder, in mathcomp.algebra.matrix]
S:2369 [binder, in mathcomp.algebra.ssralg]
s:237 [binder, in mathcomp.character.integral_char]
s:2370 [binder, in mathcomp.algebra.matrix]
s:2371 [binder, in mathcomp.algebra.matrix]
s:2373 [binder, in mathcomp.ssreflect.seq]
s:2378 [binder, in mathcomp.algebra.matrix]
s:2378 [binder, in mathcomp.ssreflect.bigop]
s:2379 [binder, in mathcomp.algebra.matrix]
S:2379 [binder, in mathcomp.algebra.ssralg]
s:238 [binder, in mathcomp.character.integral_char]
s:238 [binder, in mathcomp.ssreflect.path]
s:238 [binder, in mathcomp.solvable.cyclic]
s:2380 [binder, in mathcomp.algebra.matrix]
s:2383 [binder, in mathcomp.ssreflect.seq]
S:2386 [binder, in mathcomp.algebra.ssralg]
s:239 [binder, in mathcomp.character.integral_char]
S:2390 [binder, in mathcomp.algebra.ssralg]
s:2391 [binder, in mathcomp.ssreflect.bigop]
S:2399 [binder, in mathcomp.algebra.ssralg]
s:24 [binder, in mathcomp.fingroup.perm]
s:24 [binder, in mathcomp.solvable.jordanholder]
s:24 [binder, in mathcomp.field.algnum]
s:240 [binder, in mathcomp.character.integral_char]
s:240 [binder, in mathcomp.ssreflect.tuple]
s:240 [binder, in mathcomp.solvable.cyclic]
s:2402 [binder, in mathcomp.ssreflect.bigop]
s:2404 [binder, in mathcomp.algebra.matrix]
s:2405 [binder, in mathcomp.algebra.matrix]
s:2406 [binder, in mathcomp.algebra.matrix]
S:2406 [binder, in mathcomp.algebra.ssralg]
s:241 [binder, in mathcomp.character.integral_char]
s:241 [binder, in mathcomp.fingroup.perm]
S:241 [binder, in mathcomp.solvable.maximal]
s:2411 [binder, in mathcomp.algebra.matrix]
s:2414 [binder, in mathcomp.algebra.matrix]
s:2416 [binder, in mathcomp.algebra.matrix]
s:2417 [binder, in mathcomp.algebra.matrix]
S:2417 [binder, in mathcomp.algebra.ssralg]
s:2417 [binder, in mathcomp.ssreflect.bigop]
s:242 [binder, in mathcomp.character.integral_char]
s:242 [binder, in mathcomp.ssreflect.path]
s:2420 [binder, in mathcomp.ssreflect.seq]
S:2424 [binder, in mathcomp.algebra.ssralg]
s:2426 [binder, in mathcomp.algebra.matrix]
s:2427 [binder, in mathcomp.algebra.matrix]
s:2428 [binder, in mathcomp.algebra.matrix]
S:2428 [binder, in mathcomp.algebra.ssralg]
s:2429 [binder, in mathcomp.ssreflect.bigop]
s:243 [binder, in mathcomp.ssreflect.tuple]
S:243 [binder, in mathcomp.fingroup.action]
S:2435 [binder, in mathcomp.algebra.ssralg]
S:244 [binder, in mathcomp.fingroup.action]
S:244 [binder, in mathcomp.solvable.maximal]
S:2442 [binder, in mathcomp.algebra.ssralg]
s:2443 [binder, in mathcomp.ssreflect.bigop]
s:245 [binder, in mathcomp.fingroup.perm]
s:245 [binder, in mathcomp.ssreflect.tuple]
S:2452 [binder, in mathcomp.algebra.ssralg]
S:2456 [binder, in mathcomp.algebra.ssralg]
S:2462 [binder, in mathcomp.algebra.ssralg]
S:2468 [binder, in mathcomp.algebra.ssralg]
S:247 [binder, in mathcomp.character.vcharacter]
S:2472 [binder, in mathcomp.algebra.ssralg]
S:2478 [binder, in mathcomp.ssreflect.seq]
S:2479 [binder, in mathcomp.algebra.ssralg]
S:2488 [binder, in mathcomp.ssreflect.seq]
S:2489 [binder, in mathcomp.algebra.ssralg]
s:249 [binder, in mathcomp.fingroup.perm]
s:249 [binder, in mathcomp.ssreflect.seq]
s:249 [binder, in mathcomp.ssreflect.fintype]
s:2490 [binder, in mathcomp.algebra.matrix]
S:2493 [binder, in mathcomp.algebra.ssralg]
S:2496 [binder, in mathcomp.ssreflect.seq]
S:2499 [binder, in mathcomp.algebra.ssralg]
s:25 [binder, in mathcomp.solvable.nilpotent]
s:250 [binder, in mathcomp.ssreflect.seq]
S:2504 [binder, in mathcomp.ssreflect.seq]
S:2506 [binder, in mathcomp.algebra.ssralg]
S:2508 [binder, in mathcomp.ssreflect.seq]
s:251 [binder, in mathcomp.ssreflect.seq]
s:251 [binder, in mathcomp.ssreflect.fintype]
s:2514 [binder, in mathcomp.algebra.matrix]
S:2515 [binder, in mathcomp.ssreflect.seq]
S:2515 [binder, in mathcomp.algebra.ssralg]
s:252 [binder, in mathcomp.fingroup.perm]
s:252 [binder, in mathcomp.ssreflect.seq]
S:2520 [binder, in mathcomp.algebra.ssralg]
S:2522 [binder, in mathcomp.ssreflect.seq]
S:2524 [binder, in mathcomp.algebra.ssralg]
s:253 [binder, in mathcomp.ssreflect.seq]
S:253 [binder, in mathcomp.fingroup.action]
S:253 [binder, in mathcomp.algebra.rat]
S:2531 [binder, in mathcomp.ssreflect.seq]
S:2533 [binder, in mathcomp.algebra.ssralg]
s:2535 [binder, in mathcomp.ssreflect.bigop]
S:2538 [binder, in mathcomp.ssreflect.seq]
s:254 [binder, in mathcomp.ssreflect.seq]
S:254 [binder, in mathcomp.fingroup.action]
S:2542 [binder, in mathcomp.ssreflect.seq]
s:255 [binder, in mathcomp.fingroup.perm]
S:255 [binder, in mathcomp.fingroup.action]
S:2550 [binder, in mathcomp.ssreflect.seq]
s:2552 [binder, in mathcomp.ssreflect.bigop]
S:2553 [binder, in mathcomp.algebra.ssralg]
S:2555 [binder, in mathcomp.ssreflect.seq]
S:2558 [binder, in mathcomp.algebra.ssralg]
S:256 [binder, in mathcomp.fingroup.action]
s:256 [binder, in mathcomp.ssreflect.fintype]
S:2560 [binder, in mathcomp.ssreflect.seq]
S:2565 [binder, in mathcomp.ssreflect.seq]
S:2566 [binder, in mathcomp.algebra.ssralg]
s:257 [binder, in mathcomp.ssreflect.seq]
S:2571 [binder, in mathcomp.ssreflect.seq]
S:2577 [binder, in mathcomp.ssreflect.seq]
S:2577 [binder, in mathcomp.algebra.ssralg]
s:258 [binder, in mathcomp.fingroup.perm]
s:258 [binder, in mathcomp.ssreflect.seq]
S:258 [binder, in mathcomp.fingroup.action]
s:258 [binder, in mathcomp.ssreflect.fintype]
S:2582 [binder, in mathcomp.algebra.ssralg]
s:259 [binder, in mathcomp.ssreflect.seq]
S:2590 [binder, in mathcomp.algebra.ssralg]
S:26 [binder, in mathcomp.character.vcharacter]
S:2600 [binder, in mathcomp.algebra.ssralg]
S:2604 [binder, in mathcomp.algebra.ssralg]
s:261 [binder, in mathcomp.ssreflect.path]
S:2611 [binder, in mathcomp.algebra.ssralg]
S:2614 [binder, in mathcomp.algebra.matrix]
s:262 [binder, in mathcomp.ssreflect.seq]
S:262 [binder, in mathcomp.ssreflect.eqtype]
S:2622 [binder, in mathcomp.algebra.matrix]
S:2624 [binder, in mathcomp.algebra.matrix]
S:2625 [binder, in mathcomp.algebra.ssralg]
S:2629 [binder, in mathcomp.algebra.ssralg]
s:263 [binder, in mathcomp.fingroup.perm]
S:2631 [binder, in mathcomp.algebra.matrix]
S:2633 [binder, in mathcomp.algebra.matrix]
S:2633 [binder, in mathcomp.algebra.ssralg]
S:2637 [binder, in mathcomp.algebra.matrix]
S:2639 [binder, in mathcomp.algebra.ssralg]
s:264 [binder, in mathcomp.ssreflect.seq]
s:264 [binder, in mathcomp.ssreflect.path]
s:264 [binder, in mathcomp.ssreflect.fintype]
s:2640 [binder, in mathcomp.ssreflect.seq]
S:2641 [binder, in mathcomp.algebra.matrix]
S:2645 [binder, in mathcomp.algebra.matrix]
S:2645 [binder, in mathcomp.algebra.ssralg]
S:2649 [binder, in mathcomp.algebra.ssralg]
S:2652 [binder, in mathcomp.algebra.matrix]
s:2653 [binder, in mathcomp.ssreflect.seq]
S:2654 [binder, in mathcomp.algebra.matrix]
S:2656 [binder, in mathcomp.algebra.matrix]
S:2658 [binder, in mathcomp.algebra.ssralg]
s:2659 [binder, in mathcomp.ssreflect.seq]
S:2659 [binder, in mathcomp.algebra.matrix]
S:2662 [binder, in mathcomp.algebra.matrix]
S:2664 [binder, in mathcomp.algebra.ssralg]
S:2665 [binder, in mathcomp.algebra.matrix]
s:2668 [binder, in mathcomp.ssreflect.seq]
s:2669 [binder, in mathcomp.ssreflect.seq]
s:267 [binder, in mathcomp.ssreflect.seq]
s:2671 [binder, in mathcomp.ssreflect.seq]
S:2671 [binder, in mathcomp.algebra.ssralg]
s:2672 [binder, in mathcomp.ssreflect.seq]
S:2674 [binder, in mathcomp.algebra.matrix]
s:2675 [binder, in mathcomp.ssreflect.seq]
S:2677 [binder, in mathcomp.algebra.ssralg]
s:268 [binder, in mathcomp.fingroup.perm]
s:268 [binder, in mathcomp.ssreflect.seq]
S:2684 [binder, in mathcomp.algebra.ssralg]
s:2685 [binder, in mathcomp.ssreflect.seq]
s:2689 [binder, in mathcomp.ssreflect.seq]
s:269 [binder, in mathcomp.ssreflect.seq]
S:2690 [binder, in mathcomp.algebra.ssralg]
S:2697 [binder, in mathcomp.algebra.ssralg]
s:2698 [binder, in mathcomp.ssreflect.seq]
S:27 [binder, in mathcomp.character.vcharacter]
s:27 [binder, in mathcomp.fingroup.perm]
s:27 [binder, in mathcomp.ssreflect.tuple]
S:270 [binder, in mathcomp.field.algnum]
s:2703 [binder, in mathcomp.ssreflect.seq]
S:2703 [binder, in mathcomp.algebra.ssralg]
s:2704 [binder, in mathcomp.ssreflect.seq]
s:271 [binder, in mathcomp.fingroup.perm]
s:271 [binder, in mathcomp.ssreflect.seq]
S:271 [binder, in mathcomp.field.algnum]
S:2710 [binder, in mathcomp.algebra.ssralg]
s:2713 [binder, in mathcomp.ssreflect.seq]
S:2717 [binder, in mathcomp.algebra.ssralg]
s:2720 [binder, in mathcomp.ssreflect.seq]
s:2723 [binder, in mathcomp.ssreflect.seq]
S:2726 [binder, in mathcomp.algebra.ssralg]
s:2728 [binder, in mathcomp.ssreflect.seq]
s:2729 [binder, in mathcomp.ssreflect.seq]
s:273 [binder, in mathcomp.ssreflect.path]
s:2732 [binder, in mathcomp.ssreflect.seq]
s:2733 [binder, in mathcomp.ssreflect.seq]
S:2734 [binder, in mathcomp.algebra.ssralg]
s:2739 [binder, in mathcomp.ssreflect.seq]
s:274 [binder, in mathcomp.ssreflect.seq]
S:274 [binder, in mathcomp.field.algC]
S:2743 [binder, in mathcomp.algebra.ssralg]
s:275 [binder, in mathcomp.ssreflect.seq]
S:2751 [binder, in mathcomp.algebra.ssralg]
s:2754 [binder, in mathcomp.ssreflect.seq]
s:2755 [binder, in mathcomp.ssreflect.seq]
s:2756 [binder, in mathcomp.ssreflect.seq]
S:276 [binder, in mathcomp.character.vcharacter]
s:276 [binder, in mathcomp.ssreflect.seq]
S:276 [binder, in mathcomp.fingroup.action]
S:2760 [binder, in mathcomp.algebra.ssralg]
S:2767 [binder, in mathcomp.algebra.ssralg]
s:277 [binder, in mathcomp.fingroup.perm]
S:2774 [binder, in mathcomp.algebra.ssralg]
s:278 [binder, in mathcomp.ssreflect.seq]
s:278 [binder, in mathcomp.ssreflect.path]
S:2780 [binder, in mathcomp.algebra.ssralg]
S:2787 [binder, in mathcomp.algebra.ssralg]
S:2793 [binder, in mathcomp.algebra.ssralg]
S:2800 [binder, in mathcomp.algebra.ssralg]
S:281 [binder, in mathcomp.character.vcharacter]
s:281 [binder, in mathcomp.ssreflect.seq]
s:282 [binder, in mathcomp.fingroup.perm]
S:282 [binder, in mathcomp.fingroup.action]
s:282 [binder, in mathcomp.ssreflect.path]
s:283 [binder, in mathcomp.ssreflect.path]
s:284 [binder, in mathcomp.ssreflect.seq]
s:285 [binder, in mathcomp.ssreflect.path]
s:286 [binder, in mathcomp.fingroup.perm]
s:286 [binder, in mathcomp.ssreflect.seq]
S:287 [binder, in mathcomp.fingroup.action]
s:288 [binder, in mathcomp.algebra.matrix]
S:29 [binder, in mathcomp.character.vcharacter]
s:29 [binder, in mathcomp.solvable.jordanholder]
s:29 [binder, in mathcomp.ssreflect.path]
s:29 [binder, in mathcomp.algebra.poly]
s:290 [binder, in mathcomp.ssreflect.seq]
s:290 [binder, in mathcomp.ssreflect.path]
s:291 [binder, in mathcomp.fingroup.perm]
S:291 [binder, in mathcomp.field.algnum]
s:292 [binder, in mathcomp.ssreflect.seq]
s:292 [binder, in mathcomp.algebra.matrix]
s:293 [binder, in mathcomp.ssreflect.seq]
s:295 [binder, in mathcomp.ssreflect.seq]
s:296 [binder, in mathcomp.ssreflect.tuple]
s:297 [binder, in mathcomp.ssreflect.seq]
s:298 [binder, in mathcomp.fingroup.perm]
S:298 [binder, in mathcomp.field.algC]
S:30 [binder, in mathcomp.algebra.archimedean]
s:30 [binder, in mathcomp.fingroup.perm]
s:300 [binder, in mathcomp.ssreflect.fintype]
s:304 [binder, in mathcomp.ssreflect.tuple]
s:305 [binder, in mathcomp.ssreflect.seq]
s:306 [binder, in mathcomp.ssreflect.tuple]
s:308 [binder, in mathcomp.fingroup.perm]
s:308 [binder, in mathcomp.ssreflect.tuple]
s:309 [binder, in mathcomp.ssreflect.tuple]
s:309 [binder, in mathcomp.ssreflect.seq]
s:31 [binder, in mathcomp.fingroup.perm]
s:31 [binder, in mathcomp.solvable.jordanholder]
s:31 [binder, in mathcomp.algebra.mxpoly]
s:31 [binder, in mathcomp.ssreflect.path]
s:31 [binder, in mathcomp.algebra.poly]
s:311 [binder, in mathcomp.ssreflect.tuple]
s:313 [binder, in mathcomp.ssreflect.tuple]
s:313 [binder, in mathcomp.ssreflect.seq]
s:314 [binder, in mathcomp.ssreflect.tuple]
S:314 [binder, in mathcomp.fingroup.action]
s:315 [binder, in mathcomp.ssreflect.seq]
s:316 [binder, in mathcomp.ssreflect.tuple]
s:316 [binder, in mathcomp.ssreflect.seq]
S:316 [binder, in mathcomp.fingroup.action]
s:318 [binder, in mathcomp.ssreflect.tuple]
s:318 [binder, in mathcomp.ssreflect.seq]
S:318 [binder, in mathcomp.fingroup.action]
s:319 [binder, in mathcomp.ssreflect.tuple]
S:32 [binder, in mathcomp.character.vcharacter]
s:32 [binder, in mathcomp.fingroup.perm]
s:32 [binder, in mathcomp.algebra.poly]
s:320 [binder, in mathcomp.ssreflect.tuple]
s:320 [binder, in mathcomp.ssreflect.seq]
s:321 [binder, in mathcomp.ssreflect.tuple]
S:321 [binder, in mathcomp.fingroup.action]
s:322 [binder, in mathcomp.ssreflect.tuple]
s:322 [binder, in mathcomp.ssreflect.seq]
s:323 [binder, in mathcomp.ssreflect.tuple]
s:323 [binder, in mathcomp.ssreflect.seq]
s:323 [binder, in mathcomp.algebra.ssralg]
s:324 [binder, in mathcomp.ssreflect.tuple]
s:324 [binder, in mathcomp.ssreflect.seq]
s:325 [binder, in mathcomp.ssreflect.tuple]
s:325 [binder, in mathcomp.ssreflect.seq]
s:326 [binder, in mathcomp.ssreflect.tuple]
s:327 [binder, in mathcomp.ssreflect.tuple]
S:327 [binder, in mathcomp.fingroup.action]
S:3283 [binder, in mathcomp.ssreflect.order]
s:329 [binder, in mathcomp.ssreflect.tuple]
S:3290 [binder, in mathcomp.ssreflect.order]
S:3297 [binder, in mathcomp.ssreflect.order]
S:330 [binder, in mathcomp.fingroup.action]
S:3304 [binder, in mathcomp.ssreflect.order]
s:331 [binder, in mathcomp.ssreflect.tuple]
S:3311 [binder, in mathcomp.ssreflect.order]
S:3315 [binder, in mathcomp.ssreflect.order]
S:3319 [binder, in mathcomp.ssreflect.order]
S:3323 [binder, in mathcomp.ssreflect.order]
S:3327 [binder, in mathcomp.ssreflect.order]
s:333 [binder, in mathcomp.ssreflect.seq]
S:3331 [binder, in mathcomp.ssreflect.order]
S:3335 [binder, in mathcomp.ssreflect.order]
S:3339 [binder, in mathcomp.ssreflect.order]
s:334 [binder, in mathcomp.ssreflect.tuple]
S:3343 [binder, in mathcomp.ssreflect.order]
s:335 [binder, in mathcomp.character.inertia]
S:3351 [binder, in mathcomp.ssreflect.order]
S:3357 [binder, in mathcomp.ssreflect.order]
s:336 [binder, in mathcomp.ssreflect.seq]
s:336 [binder, in mathcomp.character.inertia]
S:3367 [binder, in mathcomp.ssreflect.order]
s:337 [binder, in mathcomp.ssreflect.tuple]
S:3373 [binder, in mathcomp.ssreflect.order]
S:3376 [binder, in mathcomp.ssreflect.order]
S:3381 [binder, in mathcomp.ssreflect.order]
S:3382 [binder, in mathcomp.ssreflect.order]
s:339 [binder, in mathcomp.ssreflect.seq]
s:339 [binder, in mathcomp.character.inertia]
S:3393 [binder, in mathcomp.ssreflect.order]
S:3394 [binder, in mathcomp.ssreflect.order]
s:34 [binder, in mathcomp.ssreflect.seq]
s:340 [binder, in mathcomp.ssreflect.tuple]
S:3405 [binder, in mathcomp.ssreflect.order]
s:341 [binder, in mathcomp.algebra.ssralg]
s:342 [binder, in mathcomp.ssreflect.seq]
S:3420 [binder, in mathcomp.ssreflect.order]
S:3426 [binder, in mathcomp.ssreflect.order]
s:343 [binder, in mathcomp.ssreflect.tuple]
S:3435 [binder, in mathcomp.ssreflect.order]
S:3445 [binder, in mathcomp.ssreflect.order]
s:345 [binder, in mathcomp.ssreflect.tuple]
s:345 [binder, in mathcomp.ssreflect.seq]
S:3455 [binder, in mathcomp.ssreflect.order]
S:3460 [binder, in mathcomp.ssreflect.order]
S:347 [binder, in mathcomp.field.algC]
S:3475 [binder, in mathcomp.ssreflect.order]
s:348 [binder, in mathcomp.ssreflect.tuple]
s:348 [binder, in mathcomp.ssreflect.seq]
s:348 [binder, in mathcomp.character.inertia]
s:349 [binder, in mathcomp.ssreflect.fintype]
S:3490 [binder, in mathcomp.ssreflect.order]
S:3496 [binder, in mathcomp.ssreflect.order]
s:35 [binder, in mathcomp.fingroup.perm]
s:35 [binder, in mathcomp.solvable.jordanholder]
s:35 [binder, in mathcomp.ssreflect.path]
S:350 [binder, in mathcomp.field.algC]
s:350 [binder, in mathcomp.character.inertia]
S:3502 [binder, in mathcomp.ssreflect.order]
S:3508 [binder, in mathcomp.ssreflect.order]
s:351 [binder, in mathcomp.ssreflect.tuple]
s:351 [binder, in mathcomp.ssreflect.seq]
s:351 [binder, in mathcomp.character.inertia]
s:351 [binder, in mathcomp.ssreflect.fintype]
S:3514 [binder, in mathcomp.ssreflect.order]
s:352 [binder, in mathcomp.character.inertia]
S:3520 [binder, in mathcomp.ssreflect.order]
S:3526 [binder, in mathcomp.ssreflect.order]
s:353 [binder, in mathcomp.ssreflect.tuple]
s:353 [binder, in mathcomp.character.inertia]
S:3532 [binder, in mathcomp.ssreflect.order]
S:3538 [binder, in mathcomp.ssreflect.order]
s:354 [binder, in mathcomp.ssreflect.seq]
s:354 [binder, in mathcomp.character.inertia]
S:3544 [binder, in mathcomp.ssreflect.order]
S:3550 [binder, in mathcomp.ssreflect.order]
S:3556 [binder, in mathcomp.ssreflect.order]
s:356 [binder, in mathcomp.algebra.ssralg]
S:3562 [binder, in mathcomp.ssreflect.order]
S:3568 [binder, in mathcomp.ssreflect.order]
s:357 [binder, in mathcomp.ssreflect.seq]
S:3574 [binder, in mathcomp.ssreflect.order]
S:3580 [binder, in mathcomp.ssreflect.order]
S:3586 [binder, in mathcomp.ssreflect.order]
S:3591 [binder, in mathcomp.ssreflect.order]
S:3596 [binder, in mathcomp.ssreflect.order]
s:360 [binder, in mathcomp.ssreflect.seq]
S:3608 [binder, in mathcomp.ssreflect.order]
s:363 [binder, in mathcomp.ssreflect.seq]
S:3630 [binder, in mathcomp.ssreflect.order]
S:3642 [binder, in mathcomp.ssreflect.order]
S:3652 [binder, in mathcomp.ssreflect.order]
S:3663 [binder, in mathcomp.ssreflect.order]
S:3669 [binder, in mathcomp.ssreflect.order]
S:3675 [binder, in mathcomp.ssreflect.order]
s:368 [binder, in mathcomp.ssreflect.tuple]
S:3681 [binder, in mathcomp.ssreflect.order]
S:3687 [binder, in mathcomp.ssreflect.order]
S:3692 [binder, in mathcomp.ssreflect.order]
S:37 [binder, in mathcomp.character.vcharacter]
s:37 [binder, in mathcomp.ssreflect.path]
S:3703 [binder, in mathcomp.ssreflect.order]
s:371 [binder, in mathcomp.ssreflect.seq]
S:3716 [binder, in mathcomp.ssreflect.order]
S:3729 [binder, in mathcomp.ssreflect.order]
s:373 [binder, in mathcomp.ssreflect.seq]
S:3739 [binder, in mathcomp.ssreflect.order]
s:375 [binder, in mathcomp.ssreflect.div]
s:375 [binder, in mathcomp.ssreflect.seq]
S:3750 [binder, in mathcomp.ssreflect.order]
S:3756 [binder, in mathcomp.ssreflect.order]
s:376 [binder, in mathcomp.ssreflect.seq]
S:3762 [binder, in mathcomp.ssreflect.order]
S:3768 [binder, in mathcomp.ssreflect.order]
s:377 [binder, in mathcomp.ssreflect.seq]
S:3774 [binder, in mathcomp.ssreflect.order]
S:3779 [binder, in mathcomp.ssreflect.order]
s:379 [binder, in mathcomp.ssreflect.seq]
S:3790 [binder, in mathcomp.ssreflect.order]
s:38 [binder, in mathcomp.fingroup.perm]
s:38 [binder, in mathcomp.solvable.jordanholder]
s:38 [binder, in mathcomp.ssreflect.path]
S:38 [binder, in mathcomp.solvable.frobenius]
S:38 [binder, in mathcomp.algebra.polyXY]
s:380 [binder, in mathcomp.ssreflect.seq]
S:3803 [binder, in mathcomp.ssreflect.order]
s:381 [binder, in mathcomp.ssreflect.seq]
S:3816 [binder, in mathcomp.ssreflect.order]
S:3826 [binder, in mathcomp.ssreflect.order]
S:3832 [binder, in mathcomp.ssreflect.order]
S:3837 [binder, in mathcomp.ssreflect.order]
S:3849 [binder, in mathcomp.ssreflect.order]
S:385 [binder, in mathcomp.fingroup.action]
S:3859 [binder, in mathcomp.ssreflect.order]
s:386 [binder, in mathcomp.ssreflect.seq]
S:3873 [binder, in mathcomp.ssreflect.order]
S:388 [binder, in mathcomp.algebra.vector]
s:388 [binder, in mathcomp.algebra.poly]
S:3883 [binder, in mathcomp.ssreflect.order]
S:3889 [binder, in mathcomp.ssreflect.order]
s:389 [binder, in mathcomp.algebra.ssralg]
S:389 [binder, in mathcomp.algebra.vector]
S:3899 [binder, in mathcomp.ssreflect.order]
S:39 [binder, in mathcomp.character.vcharacter]
s:39 [binder, in mathcomp.ssreflect.seq]
s:39 [binder, in mathcomp.field.algnum]
S:3909 [binder, in mathcomp.ssreflect.order]
s:391 [binder, in mathcomp.ssreflect.seq]
S:3919 [binder, in mathcomp.ssreflect.order]
s:392 [binder, in mathcomp.ssreflect.seq]
S:3929 [binder, in mathcomp.ssreflect.order]
S:393 [binder, in mathcomp.fingroup.action]
S:3939 [binder, in mathcomp.ssreflect.order]
S:394 [binder, in mathcomp.algebra.vector]
s:395 [binder, in mathcomp.ssreflect.seq]
S:396 [binder, in mathcomp.algebra.vector]
s:398 [binder, in mathcomp.ssreflect.seq]
S:398 [binder, in mathcomp.fingroup.action]
s:4 [binder, in mathcomp.ssreflect.seq]
s:4 [binder, in mathcomp.solvable.extremal]
s:40 [binder, in mathcomp.solvable.jordanholder]
S:40 [binder, in mathcomp.fingroup.action]
s:40 [binder, in mathcomp.solvable.gseries]
s:401 [binder, in mathcomp.ssreflect.seq]
s:401 [binder, in mathcomp.ssreflect.finset]
s:402 [binder, in mathcomp.ssreflect.seq]
s:403 [binder, in mathcomp.ssreflect.seq]
s:404 [binder, in mathcomp.ssreflect.seq]
s:406 [binder, in mathcomp.ssreflect.seq]
s:406 [binder, in mathcomp.algebra.poly]
S:408 [binder, in mathcomp.fingroup.action]
s:409 [binder, in mathcomp.ssreflect.seq]
S:409 [binder, in mathcomp.algebra.vector]
s:41 [binder, in mathcomp.fingroup.perm]
s:41 [binder, in mathcomp.ssreflect.seq]
S:410 [binder, in mathcomp.algebra.vector]
s:411 [binder, in mathcomp.ssreflect.seq]
s:411 [binder, in mathcomp.ssreflect.path]
S:411 [binder, in mathcomp.algebra.vector]
S:412 [binder, in mathcomp.fingroup.action]
s:413 [binder, in mathcomp.ssreflect.seq]
S:413 [binder, in mathcomp.algebra.vector]
S:414 [binder, in mathcomp.algebra.vector]
s:415 [binder, in mathcomp.ssreflect.seq]
s:417 [binder, in mathcomp.ssreflect.seq]
S:417 [binder, in mathcomp.fingroup.action]
S:42 [binder, in mathcomp.fingroup.perm]
s:42 [binder, in mathcomp.solvable.jordanholder]
s:42 [binder, in mathcomp.fingroup.presentation]
S:420 [binder, in mathcomp.fingroup.action]
S:423 [binder, in mathcomp.algebra.mxpoly]
s:423 [binder, in mathcomp.character.inertia]
S:426 [binder, in mathcomp.ssreflect.seq]
S:426 [binder, in mathcomp.fingroup.action]
S:429 [binder, in mathcomp.fingroup.action]
s:43 [binder, in mathcomp.fingroup.perm]
s:43 [binder, in mathcomp.solvable.gseries]
s:431 [binder, in mathcomp.ssreflect.seq]
S:431 [binder, in mathcomp.fingroup.action]
s:433 [binder, in mathcomp.ssreflect.seq]
S:433 [binder, in mathcomp.fingroup.action]
s:433 [binder, in mathcomp.algebra.ssralg]
S:437 [binder, in mathcomp.fingroup.action]
s:439 [binder, in mathcomp.character.inertia]
S:44 [binder, in mathcomp.fingroup.perm]
s:44 [binder, in mathcomp.solvable.gseries]
S:440 [binder, in mathcomp.fingroup.action]
S:444 [binder, in mathcomp.fingroup.action]
s:4442 [binder, in mathcomp.ssreflect.order]
s:4443 [binder, in mathcomp.ssreflect.order]
s:4459 [binder, in mathcomp.ssreflect.order]
s:446 [binder, in mathcomp.ssreflect.seq]
S:449 [binder, in mathcomp.fingroup.action]
S:45 [binder, in mathcomp.fingroup.perm]
s:45 [binder, in mathcomp.field.algnum]
s:4515 [binder, in mathcomp.ssreflect.order]
s:4516 [binder, in mathcomp.ssreflect.order]
s:4517 [binder, in mathcomp.ssreflect.order]
s:4518 [binder, in mathcomp.ssreflect.order]
s:452 [binder, in mathcomp.ssreflect.seq]
s:453 [binder, in mathcomp.ssreflect.path]
s:458 [binder, in mathcomp.ssreflect.path]
s:46 [binder, in mathcomp.fingroup.perm]
s:46 [binder, in mathcomp.solvable.burnside_app]
s:461 [binder, in mathcomp.ssreflect.path]
s:466 [binder, in mathcomp.ssreflect.path]
s:467 [binder, in mathcomp.character.inertia]
S:469 [binder, in mathcomp.character.classfun]
s:47 [binder, in mathcomp.ssreflect.seq]
s:470 [binder, in mathcomp.algebra.mxpoly]
s:470 [binder, in mathcomp.ssreflect.order]
S:472 [binder, in mathcomp.character.classfun]
s:472 [binder, in mathcomp.ssreflect.order]
s:473 [binder, in mathcomp.algebra.intdiv]
s:473 [binder, in mathcomp.ssreflect.seq]
s:474 [binder, in mathcomp.ssreflect.seq]
s:474 [binder, in mathcomp.ssreflect.order]
s:476 [binder, in mathcomp.ssreflect.seq]
S:476 [binder, in mathcomp.fingroup.action]
s:476 [binder, in mathcomp.ssreflect.order]
s:4762 [binder, in mathcomp.ssreflect.order]
s:4765 [binder, in mathcomp.ssreflect.order]
s:4769 [binder, in mathcomp.ssreflect.order]
s:477 [binder, in mathcomp.ssreflect.seq]
S:477 [binder, in mathcomp.fingroup.action]
S:477 [binder, in mathcomp.character.classfun]
s:477 [binder, in mathcomp.ssreflect.order]
S:477 [binder, in mathcomp.character.mxrepresentation]
s:4773 [binder, in mathcomp.ssreflect.order]
s:4777 [binder, in mathcomp.ssreflect.order]
s:478 [binder, in mathcomp.character.inertia]
s:478 [binder, in mathcomp.ssreflect.order]
S:479 [binder, in mathcomp.fingroup.action]
S:479 [binder, in mathcomp.character.classfun]
S:48 [binder, in mathcomp.fingroup.perm]
s:480 [binder, in mathcomp.ssreflect.seq]
s:480 [binder, in mathcomp.ssreflect.order]
s:481 [binder, in mathcomp.algebra.intdiv]
s:482 [binder, in mathcomp.ssreflect.seq]
s:482 [binder, in mathcomp.ssreflect.order]
s:483 [binder, in mathcomp.ssreflect.order]
s:485 [binder, in mathcomp.character.inertia]
s:485 [binder, in mathcomp.ssreflect.order]
s:487 [binder, in mathcomp.ssreflect.order]
S:488 [binder, in mathcomp.character.classfun]
s:489 [binder, in mathcomp.ssreflect.seq]
s:489 [binder, in mathcomp.ssreflect.order]
S:49 [binder, in mathcomp.character.vcharacter]
s:49 [binder, in mathcomp.fingroup.perm]
s:49 [binder, in mathcomp.ssreflect.path]
s:491 [binder, in mathcomp.ssreflect.order]
s:4925 [binder, in mathcomp.ssreflect.order]
s:4926 [binder, in mathcomp.ssreflect.order]
s:4929 [binder, in mathcomp.ssreflect.order]
s:493 [binder, in mathcomp.ssreflect.path]
s:4931 [binder, in mathcomp.ssreflect.order]
s:494 [binder, in mathcomp.ssreflect.seq]
S:494 [binder, in mathcomp.fingroup.action]
s:494 [binder, in mathcomp.ssreflect.order]
S:495 [binder, in mathcomp.fingroup.action]
s:495 [binder, in mathcomp.ssreflect.path]
S:496 [binder, in mathcomp.character.classfun]
s:497 [binder, in mathcomp.ssreflect.order]
s:498 [binder, in mathcomp.character.inertia]
S:499 [binder, in mathcomp.character.mxrepresentation]
s:5 [binder, in mathcomp.solvable.extremal]
s:500 [binder, in mathcomp.ssreflect.order]
s:5006 [binder, in mathcomp.ssreflect.order]
s:503 [binder, in mathcomp.ssreflect.order]
s:505 [binder, in mathcomp.ssreflect.order]
S:507 [binder, in mathcomp.character.classfun]
s:51 [binder, in mathcomp.ssreflect.seq]
S:510 [binder, in mathcomp.character.classfun]
S:512 [binder, in mathcomp.character.classfun]
s:512 [binder, in mathcomp.ssreflect.order]
s:514 [binder, in mathcomp.ssreflect.seq]
S:514 [binder, in mathcomp.character.classfun]
s:515 [binder, in mathcomp.ssreflect.path]
s:517 [binder, in mathcomp.ssreflect.seq]
S:518 [binder, in mathcomp.character.classfun]
s:519 [binder, in mathcomp.ssreflect.seq]
s:519 [binder, in mathcomp.ssreflect.path]
s:519 [binder, in mathcomp.ssreflect.order]
s:52 [binder, in mathcomp.ssreflect.path]
s:520 [binder, in mathcomp.ssreflect.seq]
S:520 [binder, in mathcomp.character.classfun]
s:521 [binder, in mathcomp.ssreflect.seq]
s:523 [binder, in mathcomp.ssreflect.seq]
S:523 [binder, in mathcomp.fingroup.action]
S:523 [binder, in mathcomp.character.classfun]
S:524 [binder, in mathcomp.character.classfun]
s:525 [binder, in mathcomp.ssreflect.seq]
S:526 [binder, in mathcomp.fingroup.action]
S:526 [binder, in mathcomp.character.classfun]
s:526 [binder, in mathcomp.ssreflect.order]
s:527 [binder, in mathcomp.ssreflect.seq]
S:527 [binder, in mathcomp.character.classfun]
s:528 [binder, in mathcomp.ssreflect.path]
s:529 [binder, in mathcomp.ssreflect.seq]
S:529 [binder, in mathcomp.character.classfun]
s:529 [binder, in mathcomp.ssreflect.path]
s:53 [binder, in mathcomp.fingroup.perm]
s:53 [binder, in mathcomp.solvable.extremal]
s:530 [binder, in mathcomp.ssreflect.path]
S:531 [binder, in mathcomp.character.classfun]
S:533 [binder, in mathcomp.character.classfun]
s:534 [binder, in mathcomp.ssreflect.seq]
S:534 [binder, in mathcomp.character.classfun]
S:535 [binder, in mathcomp.character.classfun]
S:537 [binder, in mathcomp.ssreflect.ssrnat]
s:538 [binder, in mathcomp.ssreflect.seq]
s:54 [binder, in mathcomp.field.algnum]
s:541 [binder, in mathcomp.ssreflect.seq]
s:541 [binder, in mathcomp.character.character]
S:542 [binder, in mathcomp.character.classfun]
s:542 [binder, in mathcomp.ssreflect.path]
s:542 [binder, in mathcomp.ssreflect.order]
s:544 [binder, in mathcomp.ssreflect.seq]
S:545 [binder, in mathcomp.fingroup.action]
S:546 [binder, in mathcomp.character.classfun]
s:547 [binder, in mathcomp.ssreflect.seq]
s:548 [binder, in mathcomp.ssreflect.order]
s:55 [binder, in mathcomp.ssreflect.path]
s:55 [binder, in mathcomp.field.algnum]
s:55 [binder, in mathcomp.solvable.extremal]
s:550 [binder, in mathcomp.ssreflect.seq]
S:550 [binder, in mathcomp.fingroup.action]
S:551 [binder, in mathcomp.fingroup.action]
S:552 [binder, in mathcomp.algebra.poly]
S:553 [binder, in mathcomp.fingroup.action]
s:553 [binder, in mathcomp.ssreflect.path]
s:553 [binder, in mathcomp.ssreflect.order]
S:554 [binder, in mathcomp.algebra.poly]
s:556 [binder, in mathcomp.ssreflect.path]
s:556 [binder, in mathcomp.ssreflect.order]
s:557 [binder, in mathcomp.ssreflect.path]
S:558 [binder, in mathcomp.algebra.poly]
S:559 [binder, in mathcomp.algebra.poly]
s:56 [binder, in mathcomp.fingroup.perm]
S:56 [binder, in mathcomp.solvable.jordanholder]
s:561 [binder, in mathcomp.ssreflect.order]
s:564 [binder, in mathcomp.ssreflect.seq]
s:564 [binder, in mathcomp.ssreflect.order]
s:565 [binder, in mathcomp.ssreflect.seq]
s:566 [binder, in mathcomp.ssreflect.seq]
s:566 [binder, in mathcomp.ssreflect.order]
s:567 [binder, in mathcomp.ssreflect.seq]
s:568 [binder, in mathcomp.ssreflect.seq]
s:569 [binder, in mathcomp.ssreflect.order]
S:57 [binder, in mathcomp.fingroup.perm]
S:57 [binder, in mathcomp.fingroup.action]
s:57 [binder, in mathcomp.field.algnum]
S:570 [binder, in mathcomp.character.classfun]
s:573 [binder, in mathcomp.ssreflect.order]
S:574 [binder, in mathcomp.character.classfun]
S:575 [binder, in mathcomp.fingroup.action]
s:576 [binder, in mathcomp.ssreflect.seq]
S:576 [binder, in mathcomp.fingroup.action]
s:577 [binder, in mathcomp.ssreflect.seq]
s:577 [binder, in mathcomp.ssreflect.path]
s:577 [binder, in mathcomp.ssreflect.order]
s:578 [binder, in mathcomp.ssreflect.seq]
s:579 [binder, in mathcomp.ssreflect.order]
S:58 [binder, in mathcomp.character.vcharacter]
s:580 [binder, in mathcomp.ssreflect.order]
s:581 [binder, in mathcomp.ssreflect.seq]
s:583 [binder, in mathcomp.ssreflect.seq]
s:583 [binder, in mathcomp.ssreflect.path]
s:59 [binder, in mathcomp.ssreflect.seq]
s:59 [binder, in mathcomp.ssreflect.ssrAC]
s:59 [binder, in mathcomp.solvable.gseries]
s:590 [binder, in mathcomp.ssreflect.path]
s:594 [binder, in mathcomp.ssreflect.seq]
s:595 [binder, in mathcomp.fingroup.action]
s:596 [binder, in mathcomp.ssreflect.seq]
s:596 [binder, in mathcomp.ssreflect.path]
s:6 [binder, in mathcomp.ssreflect.finfun]
s:6 [binder, in mathcomp.solvable.extremal]
s:60 [binder, in mathcomp.ssreflect.tuple]
s:60 [binder, in mathcomp.field.algnum]
s:60 [binder, in mathcomp.solvable.gseries]
s:600 [binder, in mathcomp.ssreflect.seq]
s:603 [binder, in mathcomp.ssreflect.path]
s:608 [binder, in mathcomp.ssreflect.seq]
s:608 [binder, in mathcomp.ssreflect.path]
S:61 [binder, in mathcomp.fingroup.perm]
S:61 [binder, in mathcomp.fingroup.action]
s:61 [binder, in mathcomp.field.algnum]
s:610 [binder, in mathcomp.ssreflect.seq]
s:612 [binder, in mathcomp.ssreflect.seq]
s:613 [binder, in mathcomp.ssreflect.seq]
s:615 [binder, in mathcomp.ssreflect.seq]
s:615 [binder, in mathcomp.ssreflect.path]
s:616 [binder, in mathcomp.ssreflect.seq]
s:616 [binder, in mathcomp.algebra.mxalgebra]
s:623 [binder, in mathcomp.ssreflect.path]
s:624 [binder, in mathcomp.ssreflect.seq]
s:626 [binder, in mathcomp.ssreflect.seq]
s:626 [binder, in mathcomp.ssreflect.path]
s:629 [binder, in mathcomp.ssreflect.seq]
S:63 [binder, in mathcomp.fingroup.perm]
s:63 [binder, in mathcomp.ssreflect.ssrAC]
s:63 [binder, in mathcomp.ssreflect.path]
s:630 [binder, in mathcomp.ssreflect.seq]
s:631 [binder, in mathcomp.ssreflect.seq]
s:632 [binder, in mathcomp.ssreflect.seq]
s:633 [binder, in mathcomp.ssreflect.seq]
s:634 [binder, in mathcomp.ssreflect.path]
s:635 [binder, in mathcomp.ssreflect.seq]
s:636 [binder, in mathcomp.ssreflect.seq]
S:636 [binder, in mathcomp.fingroup.action]
s:636 [binder, in mathcomp.ssreflect.path]
s:637 [binder, in mathcomp.ssreflect.seq]
s:638 [binder, in mathcomp.ssreflect.path]
S:639 [binder, in mathcomp.fingroup.action]
s:639 [binder, in mathcomp.ssreflect.path]
s:64 [binder, in mathcomp.ssreflect.seq]
s:64 [binder, in mathcomp.ssreflect.path]
s:640 [binder, in mathcomp.ssreflect.seq]
S:642 [binder, in mathcomp.fingroup.action]
s:643 [binder, in mathcomp.ssreflect.seq]
s:645 [binder, in mathcomp.ssreflect.path]
s:645 [binder, in mathcomp.character.mxrepresentation]
s:646 [binder, in mathcomp.ssreflect.fintype]
s:647 [binder, in mathcomp.ssreflect.seq]
s:647 [binder, in mathcomp.ssreflect.path]
s:648 [binder, in mathcomp.ssreflect.path]
s:649 [binder, in mathcomp.ssreflect.seq]
s:649 [binder, in mathcomp.ssreflect.fintype]
S:65 [binder, in mathcomp.fingroup.action]
s:65 [binder, in mathcomp.ssreflect.path]
s:651 [binder, in mathcomp.ssreflect.seq]
s:653 [binder, in mathcomp.ssreflect.seq]
s:653 [binder, in mathcomp.ssreflect.path]
s:657 [binder, in mathcomp.ssreflect.path]
s:658 [binder, in mathcomp.ssreflect.seq]
s:66 [binder, in mathcomp.ssreflect.seq]
s:661 [binder, in mathcomp.ssreflect.seq]
s:664 [binder, in mathcomp.ssreflect.seq]
S:664 [binder, in mathcomp.fingroup.action]
s:666 [binder, in mathcomp.ssreflect.seq]
s:668 [binder, in mathcomp.ssreflect.seq]
s:670 [binder, in mathcomp.ssreflect.seq]
s:672 [binder, in mathcomp.ssreflect.seq]
s:673 [binder, in mathcomp.ssreflect.seq]
s:675 [binder, in mathcomp.ssreflect.path]
s:676 [binder, in mathcomp.ssreflect.seq]
s:679 [binder, in mathcomp.ssreflect.seq]
S:68 [binder, in mathcomp.character.vcharacter]
S:68 [binder, in mathcomp.fingroup.perm]
s:680 [binder, in mathcomp.ssreflect.seq]
s:683 [binder, in mathcomp.ssreflect.seq]
s:686 [binder, in mathcomp.ssreflect.path]
s:688 [binder, in mathcomp.ssreflect.seq]
s:69 [binder, in mathcomp.ssreflect.seq]
s:692 [binder, in mathcomp.ssreflect.seq]
s:7 [binder, in mathcomp.ssreflect.seq]
S:7 [binder, in mathcomp.solvable.sylow]
S:70 [binder, in mathcomp.fingroup.action]
S:705 [binder, in mathcomp.fingroup.action]
S:706 [binder, in mathcomp.fingroup.action]
S:709 [binder, in mathcomp.fingroup.action]
s:71 [binder, in mathcomp.ssreflect.path]
S:714 [binder, in mathcomp.fingroup.action]
S:716 [binder, in mathcomp.fingroup.action]
s:72 [binder, in mathcomp.ssreflect.path]
S:720 [binder, in mathcomp.algebra.mxpoly]
s:727 [binder, in mathcomp.ssreflect.seq]
s:73 [binder, in mathcomp.ssreflect.seq]
S:73 [binder, in mathcomp.fingroup.action]
s:73 [binder, in mathcomp.ssreflect.path]
s:730 [binder, in mathcomp.ssreflect.seq]
s:736 [binder, in mathcomp.ssreflect.seq]
s:739 [binder, in mathcomp.ssreflect.seq]
s:739 [binder, in mathcomp.algebra.poly]
s:741 [binder, in mathcomp.ssreflect.seq]
s:748 [binder, in mathcomp.ssreflect.seq]
s:753 [binder, in mathcomp.ssreflect.seq]
s:755 [binder, in mathcomp.algebra.poly]
s:756 [binder, in mathcomp.algebra.ssrint]
s:759 [binder, in mathcomp.ssreflect.seq]
s:763 [binder, in mathcomp.ssreflect.fintype]
s:764 [binder, in mathcomp.ssreflect.seq]
s:764 [binder, in mathcomp.ssreflect.fintype]
s:769 [binder, in mathcomp.ssreflect.seq]
S:77 [binder, in mathcomp.character.vcharacter]
s:77 [binder, in mathcomp.ssreflect.seq]
s:773 [binder, in mathcomp.algebra.ssrint]
s:774 [binder, in mathcomp.ssreflect.seq]
s:774 [binder, in mathcomp.algebra.ssrint]
s:779 [binder, in mathcomp.ssreflect.seq]
s:78 [binder, in mathcomp.algebra.matrix]
S:783 [binder, in mathcomp.fingroup.action]
s:784 [binder, in mathcomp.ssreflect.seq]
S:784 [binder, in mathcomp.fingroup.action]
s:795 [binder, in mathcomp.ssreflect.seq]
s:8 [binder, in mathcomp.ssreflect.seq]
s:8 [binder, in mathcomp.solvable.jordanholder]
s:80 [binder, in mathcomp.ssreflect.seq]
s:805 [binder, in mathcomp.ssreflect.seq]
s:81 [binder, in mathcomp.ssreflect.seq]
s:81 [binder, in mathcomp.ssreflect.path]
S:81 [binder, in mathcomp.fingroup.morphism]
s:812 [binder, in mathcomp.ssreflect.seq]
s:82 [binder, in mathcomp.algebra.matrix]
S:82 [binder, in mathcomp.fingroup.action]
s:826 [binder, in mathcomp.ssreflect.order]
s:834 [binder, in mathcomp.ssreflect.seq]
s:837 [binder, in mathcomp.algebra.matrix]
s:838 [binder, in mathcomp.algebra.matrix]
s:839 [binder, in mathcomp.ssreflect.order]
s:84 [binder, in mathcomp.ssreflect.seq]
s:84 [binder, in mathcomp.ssreflect.path]
s:846 [binder, in mathcomp.ssreflect.seq]
S:846 [binder, in mathcomp.algebra.ssrint]
S:85 [binder, in mathcomp.character.vcharacter]
S:85 [binder, in mathcomp.fingroup.action]
s:85 [binder, in mathcomp.ssreflect.path]
S:850 [binder, in mathcomp.algebra.ssrint]
s:852 [binder, in mathcomp.algebra.poly]
S:854 [binder, in mathcomp.algebra.ssrint]
S:858 [binder, in mathcomp.algebra.ssrint]
S:862 [binder, in mathcomp.algebra.matrix]
S:862 [binder, in mathcomp.algebra.ssrint]
s:866 [binder, in mathcomp.algebra.poly]
s:87 [binder, in mathcomp.ssreflect.ssrAC]
s:87 [binder, in mathcomp.ssreflect.path]
s:873 [binder, in mathcomp.ssreflect.seq]
s:875 [binder, in mathcomp.ssreflect.seq]
s:877 [binder, in mathcomp.ssreflect.seq]
s:878 [binder, in mathcomp.ssreflect.seq]
s:88 [binder, in mathcomp.solvable.jordanholder]
s:88 [binder, in mathcomp.algebra.mxpoly]
S:88 [binder, in mathcomp.fingroup.action]
s:88 [binder, in mathcomp.ssreflect.path]
s:88 [binder, in mathcomp.solvable.extremal]
s:883 [binder, in mathcomp.ssreflect.seq]
S:884 [binder, in mathcomp.algebra.matrix]
s:888 [binder, in mathcomp.ssreflect.seq]
s:89 [binder, in mathcomp.ssreflect.seq]
s:89 [binder, in mathcomp.algebra.mxpoly]
S:89 [binder, in mathcomp.character.mxabelem]
s:89 [binder, in mathcomp.solvable.extremal]
s:890 [binder, in mathcomp.ssreflect.seq]
s:9 [binder, in mathcomp.ssreflect.seq]
s:9 [binder, in mathcomp.ssreflect.finfun]
s:90 [binder, in mathcomp.algebra.mxpoly]
s:907 [binder, in mathcomp.algebra.matrix]
s:908 [binder, in mathcomp.algebra.matrix]
s:91 [binder, in mathcomp.algebra.mxpoly]
s:91 [binder, in mathcomp.ssreflect.path]
s:92 [binder, in mathcomp.solvable.jordanholder]
s:92 [binder, in mathcomp.algebra.mxpoly]
s:920 [binder, in mathcomp.ssreflect.seq]
S:925 [binder, in mathcomp.algebra.ssralg]
s:93 [binder, in mathcomp.algebra.mxpoly]
s:93 [binder, in mathcomp.ssreflect.path]
S:932 [binder, in mathcomp.algebra.ssralg]
S:937 [binder, in mathcomp.character.mxrepresentation]
S:939 [binder, in mathcomp.algebra.ssralg]
s:94 [binder, in mathcomp.field.algebraics_fundamentals]
s:94 [binder, in mathcomp.algebra.mxpoly]
S:94 [binder, in mathcomp.fingroup.morphism]
s:941 [binder, in mathcomp.ssreflect.seq]
S:941 [binder, in mathcomp.algebra.matrix]
s:942 [binder, in mathcomp.ssreflect.seq]
s:946 [binder, in mathcomp.ssreflect.seq]
s:948 [binder, in mathcomp.ssreflect.seq]
s:949 [binder, in mathcomp.ssreflect.seq]
s:95 [binder, in mathcomp.ssreflect.seq]
s:95 [binder, in mathcomp.algebra.mxpoly]
s:95 [binder, in mathcomp.ssreflect.ssrAC]
s:950 [binder, in mathcomp.ssreflect.seq]
s:951 [binder, in mathcomp.ssreflect.seq]
s:953 [binder, in mathcomp.ssreflect.seq]
s:954 [binder, in mathcomp.ssreflect.seq]
s:956 [binder, in mathcomp.ssreflect.seq]
s:957 [binder, in mathcomp.ssreflect.seq]
s:96 [binder, in mathcomp.solvable.jordanholder]
s:96 [binder, in mathcomp.algebra.mxpoly]
s:96 [binder, in mathcomp.ssreflect.path]
s:961 [binder, in mathcomp.ssreflect.seq]
s:963 [binder, in mathcomp.ssreflect.seq]
s:966 [binder, in mathcomp.ssreflect.seq]
s:968 [binder, in mathcomp.ssreflect.seq]
s:969 [binder, in mathcomp.ssreflect.seq]
s:976 [binder, in mathcomp.ssreflect.seq]
s:979 [binder, in mathcomp.ssreflect.seq]
s:982 [binder, in mathcomp.ssreflect.seq]
s:985 [binder, in mathcomp.ssreflect.seq]
s:988 [binder, in mathcomp.ssreflect.seq]
s:99 [binder, in mathcomp.solvable.jordanholder]
s:99 [binder, in mathcomp.ssreflect.path]
s:991 [binder, in mathcomp.ssreflect.seq]
s:995 [binder, in mathcomp.ssreflect.seq]
S:996 [binder, in mathcomp.character.mxrepresentation]
s:999 [binder, in mathcomp.ssreflect.seq]
| 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 | (76754 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 | (1892 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 | (49588 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 | (305 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 | (4034 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 | (94 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 | (14802 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 | (222 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 | (9 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 | (131 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 | (43 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 | (1392 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 | (1140 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 | (3066 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) |