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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |

## S

sameP [lemma, in ssrbool]same_connect [lemma, in connect]

same_connect_r [lemma, in connect]

same_connect_rev [lemma, in connect]

same_count1 [definition, in seq]

same_cover_at [lemma, in finset]

same_fconnect1 [lemma, in connect]

same_fconnect1_r [lemma, in connect]

same_fconnect_finv [lemma, in connect]

scalar_mx [definition, in matrix]

scalar_mx0 [lemma, in matrix]

scalar_mx_add [lemma, in matrix]

scalar_mx_comm [lemma, in matrix]

scalar_mx_mul [lemma, in matrix]

scalar_mx_opp [lemma, in matrix]

scalemx [definition, in matrix]

scalemxA [lemma, in matrix]

scalemxAl [lemma, in matrix]

scalemxAr [lemma, in matrix]

scalemxN [lemma, in matrix]

scalemx0 [lemma, in matrix]

scalemx_add [lemma, in matrix]

scalemx_addl [lemma, in matrix]

scalemx_addr [lemma, in matrix]

scalemx_block [lemma, in matrix]

scalemx_paste [lemma, in matrix]

scalemx_subl [lemma, in matrix]

scalemx_subr [lemma, in matrix]

scaleNmx [lemma, in matrix]

scale0mx [lemma, in matrix]

scale1mx [lemma, in matrix]

scalp [definition, in poly]

scalp_id [lemma, in poly]

scalp_spec [lemma, in poly]

Scan [section, in seq]

scanl [definition, in seq]

scanlK [lemma, in seq]

scanl_tuple [definition, in tuple]

scanl_tupleP [lemma, in tuple]

Scan.f [variable, in seq]

Scan.g [variable, in seq]

Scan.T1 [variable, in seq]

Scan.T2 [variable, in seq]

Scan.x1 [variable, in seq]

Scan.x2 [variable, in seq]

SecondIsomorphism [section, in normal]

SecondIsomorphism.gT [variable, in normal]

SecondIsomorphism.H [variable, in normal]

SecondIsomorphism.K [variable, in normal]

SecondIsomorphism.nKH [variable, in normal]

second_isog [lemma, in normal]

second_isom [lemma, in normal]

self_inverse [definition, in ssrfun]

seq [inductive, in seq]

seq [library]

SeqFinType [section, in fintype]

SeqFinType.s [variable, in fintype]

SeqFinType.T [variable, in fintype]

seqn [definition, in seq]

seqn_rec [definition, in seq]

seqn_type [definition, in seq]

SeqSub [constructor, in fintype]

SeqTuple [section, in tuple]

SeqTuple.n [variable, in tuple]

SeqTuple.rT [variable, in tuple]

SeqTuple.T [variable, in tuple]

Sequences [section, in seq]

Sequences.n0 [variable, in seq]

Sequences.SeqFind [section, in seq]

Sequences.SeqFind.a [variable, in seq]

Sequences.T [variable, in seq]

Sequences.x0 [variable, in seq]

Seq2 [module, in choice]

seq2_of [definition, in choice]

seq2_ofK [lemma, in choice]

seq_choiceMixin [definition, in choice]

seq_choiceType [definition, in choice]

seq_countMixin [definition, in choice]

seq_countType [definition, in choice]

seq_eqMixin [definition, in seq]

seq_eqType [definition, in seq]

seq_factor [lemma, in poly]

seq_mul_polyX [lemma, in poly]

seq_of_opt [definition, in choice]

seq_of_optK [lemma, in choice]

seq_polyXn [lemma, in poly]

seq_poly0 [lemma, in poly]

seq_predType [definition, in seq]

seq_sub [record, in fintype]

seq_sub_choiceMixin [definition, in fintype]

seq_sub_choiceType [definition, in fintype]

seq_sub_countMixin [definition, in fintype]

seq_sub_countType [definition, in fintype]

seq_sub_enum [definition, in fintype]

seq_sub_eqMixin [definition, in fintype]

seq_sub_eqType [definition, in fintype]

seq_sub_finMixin [definition, in fintype]

seq_sub_finType [definition, in fintype]

seq_sub_pickle [definition, in fintype]

seq_sub_pickleK [lemma, in fintype]

seq_sub_subCountType [definition, in fintype]

seq_sub_subFinType [definition, in fintype]

seq_sub_subType [definition, in fintype]

seq_sub_unpickle [definition, in fintype]

setC [definition, in finset]

setCD [lemma, in finset]

setCI [lemma, in finset]

setCK [lemma, in finset]

setCP [lemma, in finset]

setCS [lemma, in finset]

setCT [lemma, in finset]

setCU [lemma, in finset]

setC0 [lemma, in finset]

setC11 [lemma, in finset]

setC_bigcap [lemma, in finset]

setC_bigcup [lemma, in finset]

setC_inj [lemma, in finset]

setD [definition, in finset]

setDDl [lemma, in finset]

setDDr [lemma, in finset]

setDE [lemma, in finset]

SetDef [module, in finset]

SetDefSig [module, in finset]

SetDefSig.finset [axiom, in finset]

SetDefSig.finsetE [axiom, in finset]

SetDefSig.pred_of_set [axiom, in finset]

SetDefSig.pred_of_setE [axiom, in finset]

SetDef.finset [definition, in finset]

SetDef.finsetE [lemma, in finset]

SetDef.pred_of_set [definition, in finset]

SetDef.pred_of_setE [lemma, in finset]

setDeq0 [lemma, in finset]

setDidPl [lemma, in finset]

setDIl [lemma, in finset]

setDIr [lemma, in finset]

setDP [lemma, in finset]

setDS [lemma, in finset]

setDSS [lemma, in finset]

setDT [lemma, in finset]

setDUl [lemma, in finset]

setDUr [lemma, in finset]

setDv [lemma, in finset]

setD0 [lemma, in finset]

setD1K [lemma, in finset]

setD1P [lemma, in finset]

setD11 [lemma, in finset]

setI [definition, in finset]

setIA [lemma, in finset]

setIAC [lemma, in finset]

setIC [lemma, in finset]

setICA [lemma, in finset]

setICr [lemma, in finset]

setIdP [lemma, in finset]

setIid [lemma, in finset]

setIidPl [lemma, in finset]

setIidPr [lemma, in finset]

setIIl [lemma, in finset]

setIIr [lemma, in finset]

setIK [lemma, in finset]

setIP [lemma, in finset]

setIS [lemma, in finset]

setISS [lemma, in finset]

setIT [lemma, in finset]

setIUl [lemma, in finset]

setIUr [lemma, in finset]

setI0 [lemma, in finset]

setI_addoid [definition, in finset]

setI_comoid [definition, in finset]

setI_group [definition, in groups]

setI_monoid [definition, in finset]

setI_muloid [definition, in finset]

setKI [lemma, in finset]

setKU [lemma, in finset]

SetMulDef [section, in groups]

SetMulDef.gT [variable, in groups]

setOps [section, in finset]

setOpsAlgebra [section, in finset]

setOpsAlgebra.T [variable, in finset]

setOpsDefs [section, in finset]

setOpsDefs.T [variable, in finset]

setOps.T [variable, in finset]

setP [lemma, in finset]

setSD [lemma, in finset]

setSI [lemma, in finset]

setSU [lemma, in finset]

setT [definition, in finset]

setTD [lemma, in finset]

setTI [lemma, in finset]

setTU [lemma, in finset]

SetType [section, in finset]

SetType.T [variable, in finset]

setT_group [definition, in groups]

setU [definition, in finset]

setUA [lemma, in finset]

setUAC [lemma, in finset]

setUC [lemma, in finset]

setUCA [lemma, in finset]

setUCr [lemma, in finset]

setUid [lemma, in finset]

setUidPl [lemma, in finset]

setUidPr [lemma, in finset]

setUIl [lemma, in finset]

setUIr [lemma, in finset]

setUK [lemma, in finset]

setUP [lemma, in finset]

setUS [lemma, in finset]

setUSS [lemma, in finset]

setUT [lemma, in finset]

setUUl [lemma, in finset]

setUUr [lemma, in finset]

setU0 [lemma, in finset]

setU1K [lemma, in finset]

setU1P [lemma, in finset]

setU1r [lemma, in finset]

setU11 [lemma, in finset]

setU_addoid [definition, in finset]

setU_comoid [definition, in finset]

setU_monoid [definition, in finset]

setU_muloid [definition, in finset]

setX [definition, in finset]

setXP [lemma, in finset]

setXS [lemma, in finset]

set0 [definition, in finset]

set0D [lemma, in finset]

set0I [lemma, in finset]

set0Pn [lemma, in finset]

set0U [lemma, in finset]

set1 [definition, in finset]

set1gE [lemma, in groups]

set1gP [lemma, in groups]

set1P [lemma, in finset]

set1Ul [lemma, in finset]

set1Ur [lemma, in finset]

set11 [lemma, in finset]

set1_group [definition, in groups]

set2P [lemma, in finset]

set21 [lemma, in finset]

set22 [lemma, in finset]

set_choiceMixin [definition, in finset]

set_choiceType [definition, in finset]

set_cons [lemma, in finset]

set_countMixin [definition, in finset]

set_countType [definition, in finset]

set_eqMixin [definition, in finset]

set_eqType [definition, in finset]

set_finMixin [definition, in finset]

set_finType [definition, in finset]

set_invg [definition, in groups]

set_invgK [lemma, in groups]

set_invgM [lemma, in groups]

set_mulg [definition, in groups]

set_mulgA [lemma, in groups]

set_mul1g [lemma, in groups]

set_nth [definition, in seq]

set_nth_default [lemma, in seq]

set_nth_nil [lemma, in seq]

set_of [definition, in finset]

set_of_choiceType [definition, in finset]

set_of_coset [projection, in normal]

set_of_countType [definition, in finset]

set_of_eqType [definition, in finset]

set_of_finType [definition, in finset]

set_of_subCountType [definition, in finset]

set_of_subFinType [definition, in finset]

set_of_subType [definition, in finset]

set_partition_big [lemma, in finset]

set_predType [definition, in finset]

set_set_nth [lemma, in seq]

set_subCountType [definition, in finset]

set_subFinType [definition, in finset]

set_subType [definition, in finset]

set_type [inductive, in finset]

set_0Vmem [lemma, in finset]

sfT [definition, in fintype]

sgval [definition, in groups]

sgvalEdom [lemma, in morphisms]

sgvalK [lemma, in groups]

sgvalM [lemma, in groups]

sgvalmK [lemma, in morphisms]

sgval_morphism [definition, in morphisms]

sgval_sub [lemma, in morphisms]

shape [definition, in seq]

shorten [definition, in paths]

shortenP [lemma, in paths]

ShortenSpec [constructor, in paths]

shorten_spec [inductive, in paths]

sieve [definition, in seq]

Sieve [section, in seq]

Sieve.n0 [variable, in seq]

Sieve.T [variable, in seq]

sieve0 [lemma, in seq]

sieve1 [lemma, in seq]

sieve_cat [lemma, in seq]

sieve_cons [lemma, in seq]

sieve_false [lemma, in seq]

sieve_rot [lemma, in seq]

sieve_true [lemma, in seq]

sieve_uniq [lemma, in seq]

SigEqType [section, in eqtype]

SigEqType.P [variable, in eqtype]

SigEqType.T [variable, in eqtype]

SigProj [section, in eqtype]

SigProj.P [variable, in eqtype]

SigProj.Q [variable, in eqtype]

SigProj.T [variable, in eqtype]

sig_choiceMixin [definition, in choice]

sig_choiceType [definition, in choice]

sig_countMixin [definition, in choice]

sig_countType [definition, in choice]

sig_eqMixin [definition, in eqtype]

sig_eqType [definition, in eqtype]

sig_finMixin [definition, in fintype]

sig_finType [definition, in fintype]

sig_subCountType [definition, in choice]

sig_subFinType [definition, in fintype]

sig_subType [definition, in eqtype]

simp [abbreviation, in matrix]

simp [abbreviation, in poly]

SimplFun [constructor, in ssrfun]

SimplFun [section, in ssrfun]

SimplFunDelta [definition, in ssrfun]

SimplFun.aT [variable, in ssrfun]

SimplFun.rT [variable, in ssrfun]

SimplPred [definition, in ssrbool]

simplPredType [definition, in ssrbool]

SimplRel [definition, in ssrbool]

simpl_fun [inductive, in ssrfun]

simpl_mem [section, in ssrbool]

simpl_mem.pT [variable, in ssrbool]

simpl_mem.T [variable, in ssrbool]

simpl_pred [definition, in ssrbool]

simpl_predE [lemma, in ssrbool]

simpl_rel [definition, in ssrbool]

size [definition, in seq]

size0nil [lemma, in seq]

size1_polyC [lemma, in poly]

size1_zip [lemma, in seq]

size2_zip [lemma, in seq]

size_add [lemma, in poly]

size_addl [lemma, in poly]

size_behead [lemma, in seq]

size_belast [lemma, in seq]

size_cat [lemma, in seq]

size_drop [lemma, in seq]

size_dvdp [lemma, in poly]

size_enum_ord [lemma, in fintype]

size_eqp [lemma, in poly]

size_eq0 [lemma, in seq]

size_exp [lemma, in poly]

size_flatten [lemma, in seq]

size_incr_nth [lemma, in seq]

size_iota [lemma, in seq]

size_map [lemma, in seq]

size_merge [lemma, in paths]

size_mkseq [lemma, in seq]

size_monic_mul [lemma, in poly]

size_mul [lemma, in poly]

size_mul_id [lemma, in poly]

size_mul_monic [lemma, in poly]

size_ncons [lemma, in seq]

size_nseq [lemma, in seq]

size_opp [lemma, in poly]

size_orbit [lemma, in connect]

size_pairmap [lemma, in seq]

size_pmap [lemma, in seq]

size_pmap_sub [lemma, in seq]

size_Poly [lemma, in poly]

size_poly [lemma, in poly]

size_polyC [lemma, in poly]

size_polyC_mul [lemma, in poly]

size_polyX [lemma, in poly]

size_polyXn [lemma, in poly]

size_poly0 [lemma, in poly]

size_poly1 [lemma, in poly]

size_poly_cons [lemma, in poly]

size_poly_eq [lemma, in poly]

size_poly_eq0 [lemma, in poly]

size_proper_mul [lemma, in poly]

size_rcons [lemma, in seq]

size_rev [lemma, in seq]

size_rot [lemma, in seq]

size_rotr [lemma, in seq]

size_scanl [lemma, in seq]

size_set_nth [lemma, in seq]

size_sieve [lemma, in seq]

size_sort [lemma, in paths]

size_sum [lemma, in poly]

size_take [lemma, in seq]

size_takel [lemma, in seq]

size_traject [lemma, in paths]

size_tuple [lemma, in tuple]

size_undup [lemma, in seq]

Slicing [section, in matrix]

Slicing.Block [section, in matrix]

Slicing.Block.CutBlock [section, in matrix]

Slicing.Block.CutBlock.A [variable, in matrix]

Slicing.Block.m1 [variable, in matrix]

Slicing.Block.m2 [variable, in matrix]

Slicing.Block.n1 [variable, in matrix]

Slicing.Block.n2 [variable, in matrix]

Slicing.Block.PasteBlock [section, in matrix]

Slicing.Block.PasteBlock.All [variable, in matrix]

Slicing.Block.PasteBlock.Alr [variable, in matrix]

Slicing.Block.PasteBlock.Aul [variable, in matrix]

Slicing.Block.PasteBlock.Aur [variable, in matrix]

Slicing.CutPaste [section, in matrix]

Slicing.CutPaste.m [variable, in matrix]

Slicing.CutPaste.n1 [variable, in matrix]

Slicing.CutPaste.n2 [variable, in matrix]

Slicing.R [variable, in matrix]

Slicing.TrBlock [section, in matrix]

Slicing.TrBlock.m1 [variable, in matrix]

Slicing.TrBlock.m2 [variable, in matrix]

Slicing.TrBlock.n1 [variable, in matrix]

Slicing.TrBlock.n2 [variable, in matrix]

Slicing.TrBlock.TrCut [section, in matrix]

Slicing.TrBlock.TrCut.A [variable, in matrix]

SmulProp [section, in groups]

SmulProp.gT [variable, in groups]

some [abbreviation, in ssrfun]

SomeChoiceTypes [section, in choice]

SomeChoiceTypes.P [variable, in choice]

SomeChoiceTypes.T [variable, in choice]

sort [definition, in paths]

sorted [definition, in paths]

sorted_divisors [lemma, in prime]

sorted_divisors_ltn [lemma, in prime]

sorted_filter [lemma, in paths]

sorted_iota [lemma, in paths]

sorted_ltn_iota [lemma, in paths]

sorted_ltn_uniq_leq [lemma, in paths]

sorted_merge [lemma, in paths]

sorted_primes [lemma, in prime]

sorted_sort [lemma, in paths]

sorted_uniq [lemma, in paths]

SortSeq [section, in paths]

SortSeq.leT [variable, in paths]

SortSeq.leT_total [variable, in paths]

SortSeq.T [variable, in paths]

SortSeq.Transitive [section, in paths]

SortSeq.Transitive.leT_tr [variable, in paths]

sort_of_simpl_pred [definition, in ssrbool]

sort_uniq [lemma, in paths]

split [definition, in fintype]

Split [constructor, in paths]

split [inductive, in paths]

SplitHi [constructor, in fintype]

splitK [lemma, in fintype]

Splitl [constructor, in paths]

splitl [inductive, in paths]

SplitLo [constructor, in fintype]

splitP [lemma, in paths]

splitP [lemma, in fintype]

splitPl [lemma, in paths]

splitPr [lemma, in paths]

splitP2r [lemma, in paths]

Splitr [constructor, in paths]

splitr [inductive, in paths]

split1 [lemma, in matrix]

split2r [inductive, in paths]

Split2r [constructor, in paths]

split_spec [inductive, in fintype]

split_subproof [lemma, in fintype]

sqrn_add [lemma, in ssrnat]

sqrn_add_sub [lemma, in ssrnat]

sqrn_gt0 [lemma, in ssrnat]

sqrn_inj [lemma, in ssrnat]

sqrn_sub [lemma, in ssrnat]

ssetI [definition, in finset]

ssralg [library]

ssrbool [library]

ssreflect [library]

ssrfun [library]

ssrnat [library]

SsrSyntax [module, in ssreflect]

ssr_have [definition, in ssreflect]

ssr_suff [definition, in ssreflect]

ssr_wlog [definition, in ssreflect]

ssval [projection, in fintype]

ssvalP [projection, in fintype]

sT [abbreviation, in groups]

sT [abbreviation, in groups]

sT [abbreviation, in finset]

sT [abbreviation, in groups]

sT [abbreviation, in groups]

sT [abbreviation, in groups]

strict_adjunction [lemma, in connect]

Sub [projection, in eqtype]

subBaseFinGroupType [definition, in groups]

subCountType [record, in choice]

SubCountType [constructor, in choice]

SubCountType [section, in choice]

SubCountType.P [variable, in choice]

SubCountType.T [variable, in choice]

SubCountType_for [definition, in choice]

subCount_sort [projection, in choice]

subDset [lemma, in finset]

subEproper [lemma, in finset]

SubEqMixin [definition, in eqtype]

SubEqType [section, in eqtype]

SubEqType.P [variable, in eqtype]

SubEqType.sT [variable, in eqtype]

SubEqType.T [variable, in eqtype]

subFinGroupMixin [definition, in groups]

subFinGroupType [definition, in groups]

SubFinMixin [definition, in fintype]

SubFinMixin_for [definition, in fintype]

subFinType [record, in fintype]

SubFinType [section, in fintype]

SubFinType [constructor, in fintype]

SubFinType.P [variable, in fintype]

SubFinType.T [variable, in fintype]

subFinType_finType [definition, in fintype]

subFinType_for [definition, in fintype]

subFin_sort [projection, in fintype]

subg [definition, in groups]

Subg [constructor, in groups]

subgEdom [lemma, in morphisms]

subgK [lemma, in groups]

subgM [lemma, in groups]

subgmK [lemma, in morphisms]

subgP [lemma, in groups]

subG1 [lemma, in groups]

subg_choiceMixin [definition, in groups]

subg_choiceType [definition, in groups]

subg_countMixin [definition, in groups]

subg_countType [definition, in groups]

subg_default [lemma, in groups]

subg_eqMixin [definition, in groups]

subg_eqType [definition, in groups]

subg_finMixin [definition, in groups]

subg_finType [definition, in groups]

subg_inj [lemma, in groups]

subg_inv [definition, in groups]

subg_invP [lemma, in groups]

subg_morphism [definition, in morphisms]

subg_mul [definition, in groups]

subg_mulP [lemma, in groups]

subg_of [inductive, in groups]

subg_one [definition, in groups]

subg_oneP [lemma, in groups]

subg_subCountType [definition, in groups]

subg_subFinType [definition, in groups]

subg_subType [definition, in groups]

subIset [lemma, in finset]

SubK [lemma, in eqtype]

subKn [lemma, in ssrnat]

SubMorphism [section, in morphisms]

SubMorphism.G [variable, in morphisms]

SubMorphism.gT [variable, in morphisms]

submxK [lemma, in matrix]

subn [definition, in ssrnat]

subnE [lemma, in ssrnat]

subnK [lemma, in ssrnat]

subnKC [lemma, in ssrnat]

subnn [lemma, in ssrnat]

subn0 [lemma, in ssrnat]

subn1 [lemma, in ssrnat]

subn_add2l [lemma, in ssrnat]

subn_add2r [lemma, in ssrnat]

subn_eq0 [lemma, in ssrnat]

subn_gt0 [lemma, in ssrnat]

subn_if_gt [lemma, in ssrnat]

subn_rec [definition, in ssrnat]

subn_sqr [lemma, in ssrnat]

subn_sub [lemma, in ssrnat]

subn_subA [lemma, in ssrnat]

subon1 [lemma, in ssrbool]

subon1l [lemma, in ssrbool]

subon2 [lemma, in ssrbool]

subon_bij [lemma, in ssrbool]

SubP [lemma, in eqtype]

subpred [definition, in ssrbool]

subrel [definition, in ssrbool]

subrelUl [lemma, in ssrbool]

subrelUr [lemma, in ssrbool]

subsetD [lemma, in finset]

SubsetDef [module, in fintype]

SubsetDefSig [module, in fintype]

SubsetDefSig.subset [axiom, in fintype]

SubsetDefSig.subsetEdef [axiom, in fintype]

SubsetDef.subset [definition, in fintype]

SubsetDef.subsetEdef [definition, in fintype]

subsetDl [lemma, in finset]

subsetDr [lemma, in finset]

subsetD1 [lemma, in finset]

subsetE [lemma, in fintype]

subsetI [lemma, in finset]

subsetIl [lemma, in finset]

subsetIr [lemma, in finset]

subsetP [lemma, in fintype]

subsetPn [lemma, in fintype]

subsets_disjoint [lemma, in finset]

subsetT [lemma, in finset]

subsetU [lemma, in finset]

subsetUl [lemma, in finset]

subsetUr [lemma, in finset]

subset0 [lemma, in finset]

subset1 [lemma, in finset]

subset_all [lemma, in fintype]

subset_cardP [lemma, in fintype]

subset_closure [lemma, in connect]

subset_def [abbreviation, in fintype]

subset_dfs [lemma, in connect]

subset_disjoint [lemma, in fintype]

subset_eqP [lemma, in fintype]

subset_gen [lemma, in groups]

subset_leqif_card [lemma, in fintype]

subset_leq_card [lemma, in fintype]

subset_predT [lemma, in fintype]

subset_pred1 [lemma, in fintype]

subset_trans [lemma, in fintype]

subset_type [abbreviation, in fintype]

subset_unlock [definition, in fintype]

subSnn [lemma, in ssrnat]

SubSpec [constructor, in eqtype]

subSS [lemma, in ssrnat]

subTset [lemma, in finset]

SubType [constructor, in eqtype]

subType [record, in eqtype]

SubType [section, in eqtype]

SubType.P [variable, in eqtype]

SubType.sT [variable, in eqtype]

SubType.T [variable, in eqtype]

subUset [lemma, in finset]

subxx [lemma, in fintype]

subxx_hint [lemma, in fintype]

sub0n [lemma, in ssrnat]

sub0set [lemma, in finset]

sub1G [lemma, in groups]

sub1set [lemma, in finset]

sub_choiceMixin [definition, in choice]

sub_choiceType [definition, in choice]

sub_conjg [lemma, in groups]

sub_conjgV [lemma, in groups]

sub_cosetpre [lemma, in normal]

sub_cosetpre_quo [lemma, in normal]

sub_countMixin [definition, in choice]

sub_countType [definition, in choice]

sub_enum [definition, in fintype]

sub_enum_uniq [lemma, in fintype]

sub_eqMixin [definition, in eqtype]

sub_eqType [definition, in eqtype]

sub_gen [lemma, in groups]

sub_in1 [lemma, in ssrbool]

sub_in11 [lemma, in ssrbool]

sub_in111 [lemma, in ssrbool]

sub_in12 [lemma, in ssrbool]

sub_in2 [lemma, in ssrbool]

sub_in21 [lemma, in ssrbool]

sub_in3 [lemma, in ssrbool]

sub_in_bij [lemma, in ssrbool]

sub_in_partn [lemma, in prime]

sub_in_pnat [lemma, in prime]

sub_isog [lemma, in morphisms]

sub_isom [lemma, in morphisms]

sub_mem [definition, in ssrbool]

sub_morphim_pre [lemma, in morphisms]

sub_morphpre_im [lemma, in morphisms]

sub_morphpre_injm [lemma, in morphisms]

sub_ordK [lemma, in fintype]

sub_path [lemma, in paths]

sub_proper_trans [lemma, in fintype]

sub_quotient_pre [lemma, in normal]

sub_sort [projection, in eqtype]

Sub_spec [inductive, in eqtype]

sub_sub_minn [lemma, in ssrnat]

succn [abbreviation, in ssrnat]

succnK [lemma, in ssrnat]

succn_inj [lemma, in ssrnat]

SumEqType [section, in eqtype]

SumEqType.T1 [variable, in eqtype]

SumEqType.T2 [variable, in eqtype]

SumFinType [section, in fintype]

SumFinType.T1 [variable, in fintype]

SumFinType.T2 [variable, in fintype]

summand [definition, in choice]

summxE [lemma, in matrix]

sumn [definition, in seq]

sumn_cat [lemma, in seq]

sumn_nseq [lemma, in seq]

SumTag [section, in choice]

SumTag.sT [variable, in choice]

SumTag.sT_sort [variable, in choice]

SumTag.T1 [variable, in choice]

SumTag.T2 [variable, in choice]

sum1dep_card [lemma, in finset]

sum1_card [lemma, in bigops]

sum_choiceMixin [definition, in choice]

sum_choiceType [definition, in choice]

sum_countMixin [definition, in choice]

sum_countType [definition, in choice]

sum_enum [definition, in fintype]

sum_enum_uniq [lemma, in fintype]

sum_eq [definition, in eqtype]

sum_eqE [lemma, in eqtype]

sum_eqMixin [definition, in eqtype]

sum_eqP [lemma, in eqtype]

sum_eqType [definition, in eqtype]

sum_finMixin [definition, in fintype]

sum_finType [definition, in fintype]

sum_nat_const [lemma, in bigops]

sum_nat_const_nat [lemma, in bigops]

sum_nat_dep_const [lemma, in finset]

sum_ncycle_phi [lemma, in cyclic]

sum_of_tag [definition, in choice]

sum_of_tagK [lemma, in choice]

sum_phi_dvd [lemma, in cyclic]

support [definition, in finfun]

sval [abbreviation, in eqtype]

svalP [lemma, in eqtype]

symmetric [definition, in ssrbool]

symmetric_from_pre [lemma, in ssrbool]

s2val [definition, in eqtype]

s2valP [lemma, in eqtype]

s2valP' [lemma, in eqtype]

S_pos_nat [definition, in ssrnat]

Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |