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)

N

nandP [lemma, in ssrbool]
nary_congruence [lemma, in ssreflect]
nary_congruence_statement [definition, in ssreflect]
Nat [module, in choice]
NatConst [section, in bigops]
NatConst.A [variable, in bigops]
NatConst.I [variable, in bigops]
natnseq0P [lemma, in seq]
NatPreds [section, in prime]
NatPreds.n [variable, in prime]
NatPreds.pi [variable, in prime]
NatTrec [module, in ssrnat]
natTrecE [abbreviation, in ssrnat]
NatTrec.add [definition, in ssrnat]
NatTrec.addE [lemma, in ssrnat]
NatTrec.add_mul [definition, in ssrnat]
NatTrec.add_mulE [lemma, in ssrnat]
NatTrec.double [definition, in ssrnat]
NatTrec.doubleE [lemma, in ssrnat]
NatTrec.doublen [abbreviation, in ssrnat]
NatTrec.exp [definition, in ssrnat]
NatTrec.expE [lemma, in ssrnat]
NatTrec.mul [definition, in ssrnat]
NatTrec.mulE [lemma, in ssrnat]
NatTrec.mul_exp [definition, in ssrnat]
NatTrec.mul_expE [lemma, in ssrnat]
NatTrec.odd [definition, in ssrnat]
NatTrec.oddE [lemma, in ssrnat]
NatTrec.oddn [abbreviation, in ssrnat]
NatTrec.trecE [definition, in ssrnat]
nat_AGM2 [lemma, in ssrnat]
nat_Cauchy [lemma, in ssrnat]
nat_choiceMixin [definition, in choice]
nat_choiceType [definition, in choice]
nat_countMixin [definition, in choice]
nat_countType [definition, in choice]
nat_eqMixin [definition, in ssrnat]
nat_eqType [definition, in ssrnat]
nat_irrelevance [lemma, in ssrnat]
nat_of_addn_gt0 [lemma, in ssrnat]
nat_of_add_bin [lemma, in ssrnat]
nat_of_bin [definition, in ssrnat]
nat_of_binK [lemma, in ssrnat]
nat_of_bool [definition, in ssrnat]
nat_of_exp_bin [lemma, in ssrnat]
nat_of_mul_bin [lemma, in ssrnat]
nat_of_ord [definition, in fintype]
nat_of_pos [definition, in ssrnat]
nat_of_succ_gt0 [lemma, in ssrnat]
nat_pickleK [lemma, in choice]
nat_power_theory [lemma, in ssrnat]
nat_pred [definition, in prime]
nat_pred_of_nat [definition, in prime]
nat_pred_pred [definition, in prime]
nat_semi_morph [lemma, in ssrnat]
nat_semi_ring [lemma, in ssrnat]
ncons [definition, in seq]
nconsK [lemma, in seq]
ncycles_mul_tperm [lemma, in perm]
negbF [lemma, in ssrbool]
negbFE [lemma, in ssrbool]
negbK [lemma, in ssrbool]
negbLR [lemma, in ssrbool]
negbNE [lemma, in ssrbool]
negbRL [lemma, in ssrbool]
negbT [lemma, in ssrbool]
negbTE [lemma, in ssrbool]
negb_add [lemma, in eqtype]
negb_and [lemma, in ssrbool]
negb_eqb [lemma, in eqtype]
negb_exists [lemma, in fintype]
negb_forall [lemma, in fintype]
negb_imply [lemma, in ssrbool]
negb_inj [lemma, in ssrbool]
negb_or [lemma, in ssrbool]
negn [definition, in prime]
negnK [lemma, in prime]
negP [lemma, in ssrbool]
negPf [lemma, in ssrbool]
negPn [lemma, in ssrbool]
neq0_lt0n [lemma, in ssrnat]
neq_bump [lemma, in fintype]
neq_lift [lemma, in fintype]
neq_ltn [lemma, in ssrnat]
nesym [definition, in ssrfun]
NewType [definition, in eqtype]
next [definition, in paths]
next_at [definition, in paths]
next_cycle [lemma, in paths]
next_map [lemma, in paths]
next_nth [lemma, in paths]
next_prev [lemma, in paths]
next_rev [lemma, in paths]
next_rot [lemma, in paths]
next_rotr [lemma, in paths]
nil [abbreviation, in seq]
Nil [constructor, in seq]
nil_tuple [definition, in tuple]
nn [abbreviation, in charpoly]
nNH [definition, in normal]
nonzero_poly1 [lemma, in poly]
Nopick [constructor, in fintype]
normal [definition, in groups]
normal [library]
normalG [lemma, in groups]
normalised [definition, in groups]
normaliser [definition, in groups]
Normaliser [section, in groups]
Normaliser.gT [variable, in groups]
Normaliser.norm_trans [section, in groups]
Normaliser.norm_trans.A [variable, in groups]
Normaliser.norm_trans.B [variable, in groups]
Normaliser.norm_trans.C [variable, in groups]
Normaliser.norm_trans.nBA [variable, in groups]
Normaliser.norm_trans.nCA [variable, in groups]
normaliser_group [definition, in groups]
normalM [lemma, in groups]
normalP [lemma, in groups]
normalS [lemma, in groups]
normalSG [lemma, in groups]
normal1 [lemma, in groups]
normal_cosetpre [lemma, in normal]
normal_norm [lemma, in groups]
normal_refl [lemma, in groups]
normal_sub [lemma, in groups]
normal_subnorm [lemma, in groups]
normC [lemma, in groups]
normG [lemma, in groups]
normJ [lemma, in groups]
normP [lemma, in groups]
normsG [lemma, in groups]
normsI [lemma, in groups]
normsM [lemma, in groups]
normsP [lemma, in groups]
normsR [lemma, in groups]
norms1 [lemma, in groups]
norms_cent [lemma, in groups]
norms_gen [lemma, in groups]
norms_mulgen [lemma, in groups]
norms_norm [lemma, in groups]
norm1 [lemma, in groups]
norm_class [lemma, in groups]
norm_conj_autE [lemma, in automorphism]
norm_conj_dom [lemma, in automorphism]
norm_gen [lemma, in groups]
norm_mulgenEl [lemma, in groups]
norm_mulgenEr [lemma, in groups]
norm_rlcoset [lemma, in groups]
norP [lemma, in ssrbool]
not_false_is_true [lemma, in ssrbool]
not_locked_false_eq_true [lemma, in ssreflect]
nseq [definition, in seq]
NseqthTheory [section, in seq]
NseqthTheory.T [variable, in seq]
nseq_tuple [definition, in tuple]
nseq_tupleP [lemma, in tuple]
nth [abbreviation, in seq]
nth [definition, in seq]
nthP [lemma, in seq]
nth0 [lemma, in seq]
nth_behead [lemma, in seq]
nth_cat [lemma, in seq]
nth_default [lemma, in seq]
nth_drop [lemma, in seq]
nth_enum_ord [lemma, in fintype]
nth_enum_rank [lemma, in fintype]
nth_fgraph_ord [lemma, in finfun]
nth_find [lemma, in seq]
nth_incr_nth [lemma, in seq]
nth_index [lemma, in seq]
nth_iota [lemma, in seq]
nth_last [lemma, in seq]
nth_map [lemma, in seq]
nth_mkseq [lemma, in seq]
nth_ncons [lemma, in seq]
nth_nil [lemma, in seq]
nth_nseq [lemma, in seq]
nth_ord_enum [lemma, in fintype]
nth_pairmap [lemma, in seq]
nth_rcons [lemma, in seq]
nth_rev [lemma, in seq]
nth_scanl [lemma, in seq]
nth_set_nth [lemma, in seq]
nth_take [lemma, in seq]
nth_traject [lemma, in paths]
nth_uniq [lemma, in seq]
null_mx [definition, in matrix]
Num [constructor, in ssrnat]
number [record, in ssrnat]
NumberInterpretation [section, in ssrnat]
NumberInterpretation.Trec [section, in ssrnat]
number_eqMixin [definition, in ssrnat]
number_eqType [definition, in ssrnat]
number_subType [definition, in ssrnat]
NumFactor [definition, in prime]
n_comp [definition, in connect]
n_compC [lemma, in connect]
n_comp_closure2 [lemma, in connect]
n_comp_connect [lemma, in connect]



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)