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 (14626 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 (165 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 (112 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 (7292 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 (761 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 (250 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 (390 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 (84 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 (3144 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 (126 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 (28 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 (2221 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 (53 entries)

N

n [abbreviation, in mxpoly]
n [abbreviation, in matrix]
n [abbreviation, in matrix]
n [abbreviation, in mxabelem]
n [abbreviation, in mxrepresentation]
n [abbreviation, in mxabelem]
n [definition, in alt]
n [abbreviation, in matrix]
n [definition, in vector]
n [abbreviation, in mxpoly]
n [abbreviation, in mxrepresentation]
n [abbreviation, in fintype]
NactionDef [section, in primitive_action]
NactionDef.gT [variable, in primitive_action]
NactionDef.n [variable, in primitive_action]
NactionDef.sT [variable, in primitive_action]
NactionDef.to [variable, in primitive_action]
nandP [lemma, in ssrbool]
nary_congruence [lemma, in ssreflect]
nary_mxsum_proof [lemma, in mxalgebra]
nary_mxsum_expr [definition, in mxalgebra]
nary_congruence_statement [definition, in ssreflect]
nary_addv_proof [lemma, in vector]
nary_addv_expr [definition, in vector]
Nat [module, in choice]
NatConst [section, in bigop]
NatConst.A [variable, in bigop]
NatConst.I [variable, in bigop]
natnseq0P [lemma, in seq]
NatPreds [section, in prime]
NatPreds.n [variable, in prime]
NatPreds.pi [variable, in prime]
natr_negZp [lemma, in zmodp]
natr_Zp [lemma, in zmodp]
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_expE [lemma, in ssrnat]
NatTrec.mul_exp [definition, in ssrnat]
NatTrec.odd [definition, in ssrnat]
NatTrec.oddE [lemma, in ssrnat]
NatTrec.oddn [abbreviation, in ssrnat]
NatTrec.trecE [definition, in ssrnat]
nat_of_add_bin [lemma, in ssrnat]
nat_irrelevance [lemma, in ssrnat]
nat_power_theory [lemma, in ssrnat]
nat_of_succ_gt0 [lemma, in ssrnat]
nat_negb [lemma, in fintype]
nat_Cauchy [lemma, in ssrnat]
nat_semi_ring [lemma, in ssrnat]
nat_of_ord [definition, in fintype]
nat_of_bin [definition, in ssrnat]
nat_of_bool [definition, in ssrnat]
nat_eqType [definition, in ssrnat]
nat_eqMixin [definition, in ssrnat]
nat_pred_of_nat [definition, in prime]
nat_pred_pred [definition, in prime]
nat_of_exp_bin [lemma, in ssrnat]
nat_choiceMixin [definition, in choice]
nat_AGM2 [lemma, in ssrnat]
nat_countType [definition, in choice]
nat_choiceType [definition, in choice]
nat_of_addn_gt0 [lemma, in ssrnat]
nat_pickleK [lemma, in choice]
nat_of_binK [lemma, in ssrnat]
nat_countMixin [definition, in choice]
nat_of_mul_bin [lemma, in ssrnat]
nat_semi_morph [lemma, in ssrnat]
nat_of_pos [definition, in ssrnat]
nat_pred [definition, in prime]
ncons [definition, in seq]
nconsK [lemma, in seq]
ncprod [definition, in center]
ncprodS [lemma, in center]
ncprod0 [lemma, in center]
ncprod1 [lemma, in center]
ncycles_mul_tperm [lemma, in perm]
nderivn [definition, in poly]
nderivnC [lemma, in poly]
nderivnD [lemma, in poly]
nderivnMn [lemma, in poly]
nderivnMNn [lemma, in poly]
nderivnN [lemma, in poly]
nderivnXn [lemma, in poly]
nderivnZ [lemma, in poly]
nderivn_poly0 [lemma, in poly]
nderivn_amulX [lemma, in poly]
nderivn_linear [definition, in poly]
nderivn_def [lemma, in poly]
nderivn_linear_proof [lemma, in poly]
nderivn_map [lemma, in poly]
nderivn0 [lemma, in poly]
nderivn1 [lemma, in poly]
nderiv_taylor [lemma, in poly]
nderiv_taylor_wide [lemma, in poly]
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_eqb [lemma, in eqtype]
negb_exists_in [lemma, in fintype]
negb_forall [lemma, in fintype]
negb_inj [lemma, in ssrbool]
negb_add [lemma, in eqtype]
negb_exists [lemma, in fintype]
negb_and [lemma, in ssrbool]
negb_forall_in [lemma, in fintype]
negb_or [lemma, in ssrbool]
negb_imply [lemma, in ssrbool]
negn [definition, in prime]
negnK [lemma, in prime]
negP [lemma, in ssrbool]
negPf [lemma, in ssrbool]
negPn [lemma, in ssrbool]
nElem [definition, in abelian]
nElemI [lemma, in abelian]
nElemP [lemma, in abelian]
nElemS [lemma, in abelian]
nElem0 [lemma, in abelian]
nElem1P [lemma, in abelian]
neq_lift [lemma, in fintype]
neq_bump [lemma, in fintype]
neq_ltn [lemma, in ssrnat]
neq0_lt0n [lemma, in ssrnat]
nesym [definition, in ssrfun]
NewType [definition, in eqtype]
next [definition, in path]
next_rev [lemma, in path]
next_prev [lemma, in path]
next_rot [lemma, in path]
next_cycle [lemma, in path]
next_at [definition, in path]
next_nth [lemma, in path]
next_rotr [lemma, in path]
next_map [lemma, in path]
nfHfG [definition, in quotient]
nG [abbreviation, in mxrepresentation]
nG [abbreviation, in mxrepresentation]
nGA' [definition, in hall]
nHG [definition, in finmodule]
nHG [definition, in mxrepresentation]
nHG [definition, in quotient]
nHGs [definition, in mxrepresentation]
nHGs [definition, in mxrepresentation]
nil [abbreviation, in seq]
Nil [constructor, in seq]
nilp [definition, in seq]
nilP [lemma, in seq]
NilPGroups [section, in sylow]
NilPGroups.gT [variable, in sylow]
NilPGroups.p [variable, in sylow]
Nilpotent [section, in sylow]
nilpotent [definition, in nilpotent]
nilpotent [library]
NilpotentProps [section, in nilpotent]
NilpotentProps.gT [variable, in nilpotent]
nilpotentS [lemma, in nilpotent]
nilpotent_proper_norm [lemma, in nilpotent]
nilpotent_maxp_normal [lemma, in sylow]
nilpotent_class [lemma, in nilpotent]
nilpotent_Hall_pcore [lemma, in sylow]
nilpotent_sol [lemma, in nilpotent]
nilpotent_Fitting [lemma, in maximal]
nilpotent_sub_norm [lemma, in nilpotent]
nilpotent_pcore_Hall [lemma, in sylow]
nilpotent_pcoreC [lemma, in sylow]
nilpotent_subnormal [lemma, in nilpotent]
Nilpotent.gT [variable, in sylow]
nilpotent1 [lemma, in nilpotent]
nil_class_injm [lemma, in nilpotent]
nil_class_quotient_center [lemma, in nilpotent]
nil_tuple [definition, in tuple]
nil_comm_properl [lemma, in nilpotent]
nil_class_ucn [lemma, in nilpotent]
nil_Zgroup_cyclic [lemma, in sylow]
nil_class_morphim [lemma, in nilpotent]
nil_class0 [lemma, in nilpotent]
nil_comm_properr [lemma, in nilpotent]
nil_class2 [lemma, in sylow]
nil_class1 [lemma, in nilpotent]
nil_class3 [lemma, in sylow]
nil_class [definition, in nilpotent]
nil_class_pgroup [lemma, in sylow]
nNH [definition, in quotient]
nonconform_mx [lemma, in matrix]
nontrivial_gacent_pgroup [lemma, in sylow]
nonzero_poly1 [lemma, in poly]
Nopick [constructor, in fintype]
normal [definition, in fingroup]
normalG [lemma, in fingroup]
normalGI [lemma, in fingroup]
normalGY [lemma, in fingroup]
NormalHall [section, in pgroup]
NormalHall.gT [variable, in pgroup]
NormalHall.pi [variable, in pgroup]
normalI [lemma, in fingroup]
normalised [definition, in fingroup]
Normaliser [section, in fingroup]
normaliser [definition, in fingroup]
normaliser_group [definition, in fingroup]
Normaliser.gT [variable, in fingroup]
Normaliser.norm_trans.nBA [variable, in fingroup]
Normaliser.norm_trans [section, in fingroup]
Normaliser.norm_trans.nCA [variable, in fingroup]
Normaliser.norm_trans.A [variable, in fingroup]
Normaliser.norm_trans.B [variable, in fingroup]
Normaliser.norm_trans.C [variable, in fingroup]
Normaliser.norm_trans.D [variable, in fingroup]
Normaliser.SubAbelian [section, in fingroup]
Normaliser.SubAbelian.A [variable, in fingroup]
Normaliser.SubAbelian.B [variable, in fingroup]
Normaliser.SubAbelian.C [variable, in fingroup]
Normaliser.SubAbelian.cAA [variable, in fingroup]
normalJ [lemma, in fingroup]
normalM [lemma, in fingroup]
normalP [lemma, in fingroup]
normalS [lemma, in fingroup]
normalSG [lemma, in fingroup]
normalYG [lemma, in fingroup]
normal_subnorm [lemma, in fingroup]
normal_norm [lemma, in fingroup]
normal_sub_max_pgroup [lemma, in pgroup]
normal_rfix_mx_module [lemma, in mxrepresentation]
normal_sylowP [lemma, in sylow]
normal_refl [lemma, in fingroup]
normal_rank1_structure [lemma, in extremal]
normal_Hall_pcore [lemma, in pgroup]
normal_max_pgroup_Hall [lemma, in pgroup]
normal_cosetpre [lemma, in quotient]
normal_subnormal [lemma, in gseries]
normal_sub [lemma, in fingroup]
normal_pgroup [lemma, in sylow]
normal1 [lemma, in fingroup]
normC [lemma, in fingroup]
normCs [lemma, in fingroup]
normD1 [lemma, in fingroup]
normG [lemma, in fingroup]
normJ [lemma, in fingroup]
normP [lemma, in fingroup]
normsD [lemma, in fingroup]
normsG [lemma, in fingroup]
normsGI [lemma, in fingroup]
normsI [lemma, in fingroup]
normsIG [lemma, in fingroup]
normsIs [lemma, in fingroup]
normsM [lemma, in fingroup]
normsP [lemma, in fingroup]
normsR [lemma, in fingroup]
normsRl [lemma, in commutator]
normsRr [lemma, in commutator]
normsU [lemma, in fingroup]
normsY [lemma, in fingroup]
norms_norm [lemma, in fingroup]
norms_bigcap [lemma, in fingroup]
norms_class_support [lemma, in fingroup]
norms_gen [lemma, in fingroup]
norms_cent [lemma, in fingroup]
norms_bigcup [lemma, in fingroup]
norms_cycle [lemma, in fingroup]
norms1 [lemma, in fingroup]
norm_sub_rstabs_rfix_mx [lemma, in mxrepresentation]
norm_sub_max_pgroup [lemma, in pgroup]
norm_joinEr [lemma, in fingroup]
norm_normalI [lemma, in fingroup]
norm_conj_norm [lemma, in fingroup]
norm_conj_cent [lemma, in hall]
norm_joinEl [lemma, in fingroup]
norm_conj_autE [lemma, in automorphism]
norm_gen [lemma, in fingroup]
norm_rlcoset [lemma, in fingroup]
norm1 [lemma, in fingroup]
norP [lemma, in ssrbool]
NotExtremal [constructor, in extremal]
notF [definition, in ssrbool]
not_isog_Dn_DnQ [lemma, in extraspecial]
not_false_is_true [lemma, in ssrbool]
not_simple_Alt_4 [lemma, in alt]
not_rsim_op0 [definition, in mxrepresentation]
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]
nth_set_nth [lemma, in seq]
nth_behead [lemma, in seq]
nth_fgraph_ord [lemma, in finfun]
nth_map [lemma, in seq]
nth_take [lemma, in seq]
nth_mkseq [lemma, in seq]
nth_traject [lemma, in path]
nth_last [lemma, in seq]
nth_rev [lemma, in seq]
nth_nseq [lemma, in seq]
nth_enum_ord [lemma, in fintype]
nth_iota [lemma, in seq]
nth_cat [lemma, in seq]
nth_default [lemma, in seq]
nth_find [lemma, in seq]
nth_rcons [lemma, in seq]
nth_scanl [lemma, in seq]
nth_enum_rank [lemma, in fintype]
nth_zip [lemma, in seq]
nth_pairmap [lemma, in seq]
nth_drop [lemma, in seq]
nth_uniq [lemma, in seq]
nth_index [lemma, in seq]
nth_incr_nth [lemma, in seq]
nth_zip_cond [lemma, in seq]
nth_ncons [lemma, in seq]
nth_nil [lemma, in seq]
nth_enum_rank_in [lemma, in fintype]
nth_ord_enum [lemma, in fintype]
nth0 [lemma, in seq]
ntransitive [definition, in primitive_action]
NTransitive [section, in primitive_action]
ntransitive_primitive [lemma, in primitive_action]
ntransitive_weak [lemma, in primitive_action]
NTransitive.A [variable, in primitive_action]
NTransitive.gT [variable, in primitive_action]
NTransitive.n [variable, in primitive_action]
NTransitive.S [variable, in primitive_action]
NTransitive.sT [variable, in primitive_action]
NTransitive.to [variable, in primitive_action]
ntransitive0 [lemma, in primitive_action]
ntransitive1 [lemma, in primitive_action]
NTransitveProp [section, in primitive_action]
NTransitveProp.G [variable, in primitive_action]
NTransitveProp.gT [variable, in primitive_action]
NTransitveProp.S [variable, in primitive_action]
NTransitveProp.sT [variable, in primitive_action]
NTransitveProp.to [variable, in primitive_action]
NTransitveProp1 [section, in primitive_action]
NTransitveProp1.G [variable, in primitive_action]
NTransitveProp1.gT [variable, in primitive_action]
NTransitveProp1.S [variable, in primitive_action]
NTransitveProp1.sT [variable, in primitive_action]
NTransitveProp1.to [variable, in primitive_action]
nt_prime_order [lemma, in cyclic]
nt_pnElem [lemma, in abelian]
nt_gen_prime [lemma, in cyclic]
Num [constructor, in ssrnat]
number [record, in ssrnat]
NumberInterpretation [section, in ssrnat]
NumberInterpretation.Trec [section, in ssrnat]
number_eqType [definition, in ssrnat]
number_subType [definition, in ssrnat]
number_eqMixin [definition, in ssrnat]
NumFactor [definition, in prime]
nZA [definition, in maximal]
nz_row_eq0 [lemma, in matrix]
nz_row_mxsimple [lemma, in mxrepresentation]
nz_row [definition, in matrix]
nz_u [definition, in mxrepresentation]
nz_row_sub [lemma, in mxalgebra]
nz_socle [lemma, in mxrepresentation]
n_compC [lemma, in fingraph]
n_act_action [definition, in primitive_action]
n_comp [definition, in fingraph]
n_comp_closure2 [lemma, in fingraph]
n_act_dtuple [lemma, in primitive_action]
n_ [abbreviation, in mxrepresentation]
n_act_add [lemma, in primitive_action]
n_act0 [lemma, in primitive_action]
n_gt0 [definition, in poly]
n_act_is_action [lemma, in primitive_action]
n_comp_connect [lemma, in fingraph]
n_ [definition, in finmodule]
n_act [definition, in primitive_action]
n' [abbreviation, in mxabelem]



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 (14626 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 (165 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 (112 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 (7292 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 (761 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 (250 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 (390 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 (84 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 (3144 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 (126 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 (28 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 (2221 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 (53 entries)