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) |