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

## D

d [abbreviation, in mxpoly]DecField [module, in finalg]

DecidableField [module, in ssralg]

DecideRed [section, in mxrepresentation]

DecideRed.Definitions [section, in mxrepresentation]

DecideRed.Definitions.F [variable, in mxrepresentation]

DecideRed.Definitions.G [variable, in mxrepresentation]

DecideRed.Definitions.gT [variable, in mxrepresentation]

DecideRed.Definitions.n [variable, in mxrepresentation]

DecideRed.Definitions.rG [variable, in mxrepresentation]

DecideRed.F [variable, in mxrepresentation]

DecideRed.G [variable, in mxrepresentation]

DecideRed.gT [variable, in mxrepresentation]

DecideRed.n [variable, in mxrepresentation]

DecideRed.rG [variable, in mxrepresentation]

decP [definition, in ssrbool]

decPcases [lemma, in ssrbool]

DecSocleType [lemma, in mxrepresentation]

dec_mxsimple_exists [lemma, in mxrepresentation]

dec_mx_reducible_semisimple [lemma, in mxrepresentation]

Def [section, in finfun]

Def [section, in tuple]

defG [definition, in abelian]

Definitions [section, in frobenius]

Definitions.FrobeniusAction [section, in frobenius]

Definitions.FrobeniusAction.G [variable, in frobenius]

Definitions.FrobeniusAction.H [variable, in frobenius]

Definitions.FrobeniusAction.S [variable, in frobenius]

Definitions.FrobeniusAction.sT [variable, in frobenius]

Definitions.FrobeniusAction.to [variable, in frobenius]

Definitions.gT [variable, in frobenius]

defQ [definition, in extremal]

Defs [section, in gproduct]

Defs [section, in maximal]

Defs [section, in center]

Defs.gT [variable, in maximal]

Defs.gT [variable, in center]

Defs.gT [variable, in gproduct]

defU [definition, in mxrepresentation]

def_p [definition, in extremal]

def_q [definition, in extremal]

def_r [definition, in extremal]

def_q [definition, in extremal]

def_pnElem [lemma, in abelian]

def_n [definition, in extremal]

Def.aT [variable, in finfun]

Def.n [variable, in tuple]

Def.rT [variable, in finfun]

Def.T [variable, in tuple]

def2 [definition, in extremal]

def2qr [definition, in extremal]

degree_mxminpoly_map [lemma, in mxpoly]

degree_irr1 [lemma, in mxrepresentation]

degree_mxminpoly [definition, in mxpoly]

degree_mxminpoly_proof [lemma, in mxpoly]

delta_mx [definition, in matrix]

delta_mx_rshift [lemma, in matrix]

delta_mx_ushift [lemma, in matrix]

delta_mx_dshift [lemma, in matrix]

delta_mx_lshift [lemma, in matrix]

dependentReturnType [definition, in ssreflect]

dergS [lemma, in commutator]

dergSn [lemma, in commutator]

derg0 [lemma, in commutator]

derg1 [lemma, in commutator]

derG1P [lemma, in commutator]

deriv [definition, in poly]

Deriv [section, in poly]

derivC [lemma, in poly]

DerivC [section, in poly]

derivCE [definition, in poly]

DerivC.R [variable, in poly]

derivD [lemma, in poly]

derivE [definition, in poly]

DerivedBasics [section, in commutator]

DerivedBasics.gT [variable, in commutator]

derivedP [lemma, in nilpotent]

derived_at_rec [definition, in commutator]

derived_at_group [definition, in commutator]

derived_at [definition, in commutator]

derivM [lemma, in poly]

derivMn [lemma, in poly]

derivMNn [lemma, in poly]

derivN [lemma, in poly]

derivn [definition, in poly]

derivnC [lemma, in poly]

derivnD [lemma, in poly]

derivnMn [lemma, in poly]

derivnMNn [lemma, in poly]

derivnN [lemma, in poly]

derivnS [lemma, in poly]

derivnXn [lemma, in poly]

derivnZ [lemma, in poly]

derivn_linear [definition, in poly]

derivn_map [lemma, in poly]

derivn_amulX [lemma, in poly]

derivn_poly0 [lemma, in poly]

derivn_linear_proof [lemma, in poly]

derivn0 [lemma, in poly]

derivn1 [lemma, in poly]

derivPn [lemma, in poly]

derivSn [lemma, in poly]

derivX [lemma, in poly]

derivXn [lemma, in poly]

derivZ [lemma, in poly]

deriv_linear [definition, in poly]

deriv_linear_proof [lemma, in poly]

deriv_amulX [lemma, in poly]

deriv_poly_comp [lemma, in poly]

deriv_map [lemma, in poly]

Deriv.R [variable, in poly]

deriv0 [lemma, in poly]

derJ [lemma, in commutator]

der_sub [lemma, in commutator]

der_subS [lemma, in commutator]

der_norm [lemma, in commutator]

der_normalS [lemma, in commutator]

der_abelian [lemma, in commutator]

der_normal [lemma, in commutator]

der_mgFun [definition, in commutator]

der_gFun [definition, in commutator]

der_igFun [definition, in commutator]

der_group_set [lemma, in commutator]

der_cprod [lemma, in nilpotent]

der_cont [lemma, in commutator]

der_char [lemma, in commutator]

der1_stab_Ohm1_SCN_series [lemma, in maximal]

der1_min [lemma, in commutator]

der1_joing_cycles [lemma, in commutator]

der1_subG [lemma, in fingroup]

der1_sub_rker [lemma, in mxrepresentation]

determinant [definition, in matrix]

determinant_multilinear [lemma, in matrix]

determinant_alternate [lemma, in matrix]

detM [lemma, in matrix]

detV [lemma, in matrix]

det_mulmx [lemma, in matrix]

det_inv [lemma, in matrix]

det_scalar1 [lemma, in matrix]

det_perm [lemma, in matrix]

det_map_mx [lemma, in matrix]

det_scalemx [lemma, in matrix]

det_diag [lemma, in matrix]

det_tr [lemma, in matrix]

det_ublock [lemma, in matrix]

det_scalar [lemma, in matrix]

det_lblock [lemma, in matrix]

det0 [lemma, in matrix]

det0P [lemma, in mxalgebra]

det1 [lemma, in matrix]

dfs [definition, in fingraph]

dfsP [lemma, in fingraph]

DfsPath [constructor, in fingraph]

dfs_path [inductive, in fingraph]

DgH [definition, in gproduct]

DgK [definition, in gproduct]

diagA [definition, in mxpoly]

diag_mx_comm [lemma, in matrix]

diag_mx_sum_delta [lemma, in matrix]

diag_const_mx [lemma, in matrix]

diag_mx [definition, in matrix]

diag_mx_is_linear [lemma, in matrix]

diag_mxC [lemma, in matrix]

diag_mx_linear [definition, in matrix]

diag_mx_additive [definition, in matrix]

diffmx [definition, in mxalgebra]

diffmxE [lemma, in mxalgebra]

diffmxSl [lemma, in mxalgebra]

diffmx_def [definition, in mxalgebra]

diffmx_key [lemma, in mxalgebra]

diffv [definition, in vector]

diffvSl [lemma, in vector]

diff_roots [definition, in poly]

Dihedral [constructor, in extremal]

dihedral_classP [lemma, in extremal]

dihedral_gtype [definition, in extremal]

dihedral2_structure [lemma, in extremal]

dimv [definition, in vector]

dimvf [lemma, in vector]

dimvS [lemma, in vector]

dimv_leqif_eq [lemma, in vector]

dimv_disjoint_sum [lemma, in vector]

dimv_compl [lemma, in vector]

dimv_sum_leqif [lemma, in vector]

dimv_cap_compl [lemma, in vector]

dimv_leqif_sup [lemma, in vector]

dimv_sum_cap [lemma, in vector]

dimv_eq0 [lemma, in vector]

dimv_leq_sum [lemma, in vector]

dimv_sumw_leqif [lemma, in vector]

dimv0 [lemma, in vector]

dim_injv [lemma, in vector]

dim_span [lemma, in vector]

dim_abelemE [lemma, in mxabelem]

dinjectiveb [definition, in fintype]

dinjectiveP [lemma, in fintype]

dinjectivePn [lemma, in fintype]

directv [abbreviation, in vector]

directv [abbreviation, in vector]

directvE [lemma, in vector]

directvEgeq [lemma, in vector]

directvP [lemma, in vector]

directv_sumP [lemma, in vector]

directv_sumE [lemma, in vector]

directv_sum_recP [definition, in vector]

directv_sum_unique [lemma, in vector]

directv_addP [lemma, in vector]

directv_def [definition, in vector]

directv_trivial [lemma, in vector]

directv_addE [lemma, in vector]

directv_add_unique [lemma, in vector]

direct_product [definition, in gproduct]

DirprodIsom [section, in gproduct]

DirprodIsom.gT [variable, in gproduct]

disjoint [definition, in fintype]

disjoints_subset [lemma, in finset]

disjointU [lemma, in fintype]

disjointU1 [lemma, in fintype]

disjoint_has [lemma, in fintype]

disjoint_subset [lemma, in fintype]

disjoint_cat [lemma, in fintype]

disjoint_setI0 [lemma, in finset]

disjoint_cons [lemma, in fintype]

disjoint_trans [lemma, in fintype]

disjoint_sym [lemma, in fintype]

disjoint0 [lemma, in fintype]

disjoint1 [lemma, in fintype]

distn [definition, in ssrnat]

DistnArg [constructor, in ssrnat]

distnC [lemma, in ssrnat]

distnEl [lemma, in ssrnat]

distnEr [lemma, in ssrnat]

distnn [lemma, in ssrnat]

distnS [lemma, in ssrnat]

distn_add2l [lemma, in ssrnat]

distn_eq1 [lemma, in ssrnat]

distn_arg [inductive, in ssrnat]

distn_add2r [lemma, in ssrnat]

distn_eq0 [lemma, in ssrnat]

distn0 [lemma, in ssrnat]

Distributivity [section, in bigop]

Distributivity.one [variable, in bigop]

Distributivity.plus [variable, in bigop]

Distributivity.R [variable, in bigop]

Distributivity.times [variable, in bigop]

Distributivity.zero [variable, in bigop]

distSn [lemma, in ssrnat]

dist0n [lemma, in ssrnat]

div [library]

divCp_spec [lemma, in poly]

divgI [lemma, in fingroup]

divgr [definition, in gproduct]

divgrMid [lemma, in gproduct]

divgrMl [lemma, in gproduct]

divgr_id [lemma, in gproduct]

divgr_eq [lemma, in gproduct]

divgS [lemma, in fingroup]

divg_normal [lemma, in quotient]

divg_index [lemma, in fingroup]

divisorn [lemma, in prime]

divisors [definition, in prime]

divisors_uniq [lemma, in prime]

divisors_correct [lemma, in prime]

divisor1 [lemma, in prime]

divn [definition, in div]

divnAC [lemma, in div]

divnK [lemma, in div]

divnn [lemma, in div]

divn_divr [lemma, in div]

divn_pmul2r [lemma, in div]

divn_divl [lemma, in div]

divn_addl_mul [lemma, in div]

divn_mulCA [lemma, in div]

divn_gt0 [lemma, in div]

divn_pmul2l [lemma, in div]

divn_mulA [lemma, in div]

divn_small [lemma, in div]

divn_eq [lemma, in div]

divn_addl [lemma, in div]

divn_mulAC [lemma, in div]

divn_addr [lemma, in div]

divn0 [lemma, in div]

divn1 [lemma, in div]

divn2 [lemma, in div]

divp [definition, in poly]

divp_mon_spec [lemma, in poly]

divp_mon_eq [lemma, in poly]

divp_spec [lemma, in poly]

divp_mull [lemma, in poly]

divp_size [lemma, in poly]

divp1 [lemma, in poly]

div_ring_mul_group_cyclic [lemma, in cyclic]

div0n [lemma, in div]

div0p [lemma, in poly]

dlsubmx [definition, in matrix]

DnQ_P [lemma, in extraspecial]

DnQ_pgroup [lemma, in extraspecial]

DnQ_extraspecial [lemma, in extraspecial]

dom [definition, in morphism]

dom [abbreviation, in action]

domG [definition, in automorphism]

domG [definition, in automorphism]

domP [lemma, in morphism]

dom_hom_mx_module [lemma, in mxrepresentation]

dom_qactJ [lemma, in action]

dom_hom_invmx [lemma, in mxrepresentation]

dom_hom_mx [definition, in mxrepresentation]

dom_ker [lemma, in morphism]

double [definition, in ssrnat]

doubleE [lemma, in ssrnat]

doubleK [lemma, in ssrnat]

doubleS [lemma, in ssrnat]

double_mulr [lemma, in ssrnat]

double_gt0 [lemma, in ssrnat]

double_inj [definition, in ssrnat]

double_add [lemma, in ssrnat]

double_rec [definition, in ssrnat]

double_mull [lemma, in ssrnat]

double_sub [lemma, in ssrnat]

double_eq0 [lemma, in ssrnat]

double0 [lemma, in ssrnat]

dp [definition, in mxpoly]

dpair [definition, in perm]

dprod [abbreviation, in gproduct]

dprod [abbreviation, in gproduct]

dprodA [lemma, in gproduct]

dprodC [lemma, in gproduct]

dprodE [lemma, in gproduct]

dprodEcprod [lemma, in gproduct]

dprodEsdprod [lemma, in gproduct]

dprodEY [lemma, in gproduct]

dprodg1 [lemma, in gproduct]

dprodm [definition, in gproduct]

dprodmE [lemma, in gproduct]

dprodmEl [lemma, in gproduct]

dprodmEr [lemma, in gproduct]

dprodm_morphism [definition, in gproduct]

dprodm_eqf [lemma, in gproduct]

dprodm_cprod [lemma, in gproduct]

dprodP [lemma, in gproduct]

dprodYP [lemma, in gproduct]

dprod_abelaw [definition, in gproduct]

dprod_law [definition, in gproduct]

dprod_exponent [lemma, in abelian]

dprod_modl [lemma, in gproduct]

dprod_card [lemma, in gproduct]

dprod_modr [lemma, in gproduct]

dprod_abelem [lemma, in abelian]

dprod_normal2 [lemma, in gproduct]

dprod_nil [lemma, in nilpotent]

dprod1g [lemma, in gproduct]

dq [definition, in mxpoly]

drop [definition, in seq]

drop_cat [lemma, in seq]

drop_size_cat [lemma, in seq]

drop_nth [lemma, in seq]

drop_size [lemma, in seq]

drop_cons [lemma, in seq]

drop_tuple [definition, in tuple]

drop_tupleP [lemma, in tuple]

drop_rcons [lemma, in seq]

drop_behead [lemma, in seq]

drop_oversize [lemma, in seq]

drop0 [lemma, in seq]

drop1 [lemma, in seq]

drsubmx [definition, in matrix]

dsubmx [definition, in matrix]

dsubmx_linear [definition, in matrix]

dsubmx_additive [definition, in matrix]

dtuple_on_subset [lemma, in primitive_action]

dtuple_on_add [lemma, in primitive_action]

dtuple_on [definition, in primitive_action]

dtuple_onP [lemma, in primitive_action]

dtuple_on_add_D1 [lemma, in primitive_action]

dvdMpP [lemma, in poly]

dvdn [definition, in div]

dvdnn [lemma, in div]

dvdnP [lemma, in div]

dvdn_lcml [lemma, in div]

dvdn_mulr [lemma, in div]

dvdn_gcd [lemma, in div]

dvdn_odd [lemma, in div]

dvdn_addr [lemma, in div]

dvdn_biglcmP [lemma, in bigop]

dvdn_pmul2r [lemma, in div]

dvdn_add_eq [lemma, in div]

dvdn_indexg [lemma, in fingroup]

dvdn_addl [lemma, in div]

dvdn_biggcdP [lemma, in bigop]

dvdn_leq_log [lemma, in prime]

dvdn_gcdl [lemma, in div]

dvdn_lcm_idl [lemma, in div]

dvdn_gcd_idr [lemma, in div]

dvdn_sum [lemma, in prime]

dvdn_cardMg [lemma, in fingroup]

dvdn_exp2r [lemma, in div]

dvdn_eq [lemma, in div]

dvdn_prime2 [lemma, in prime]

dvdn_exp2l [lemma, in div]

dvdn_lcm_idr [lemma, in div]

dvdn_morphim [lemma, in quotient]

dvdn_orbit [lemma, in action]

dvdn_Pexp2l [lemma, in div]

dvdn_gcd_idl [lemma, in div]

dvdn_lcmr [lemma, in div]

dvdn_gt0 [lemma, in div]

dvdn_mull [lemma, in div]

dvdn_sub [lemma, in div]

dvdn_exponent [lemma, in abelian]

dvdn_leq [lemma, in div]

dvdn_gcdr [lemma, in div]

dvdn_exp [lemma, in div]

dvdn_subr [lemma, in div]

dvdn_quotient [lemma, in quotient]

dvdn_pfactor [lemma, in prime]

dvdn_pmul2l [lemma, in div]

dvdn_mul [lemma, in div]

dvdn_part [lemma, in prime]

dvdn_prime_cyclic [lemma, in cyclic]

dvdn_lcm [lemma, in div]

dvdn_partP [lemma, in prime]

dvdn_pexp2r [lemma, in div]

dvdn_divisors [lemma, in prime]

dvdn_trans [lemma, in div]

dvdn_add [lemma, in div]

dvdn_subl [lemma, in div]

dvdn0 [lemma, in div]

dvdn1 [lemma, in div]

dvdn2 [lemma, in div]

dvdp [definition, in poly]

dvdpp [lemma, in poly]

dvdpP [lemma, in poly]

dvdpPc [lemma, in poly]

dvdp_add_eq [lemma, in poly]

dvdp_gcd [lemma, in poly]

dvdp_addl [lemma, in poly]

dvdp_sub [lemma, in poly]

dvdp_gcd2 [lemma, in poly]

dvdp_mulr [lemma, in poly]

dvdp_mod [lemma, in poly]

dvdp_mul [lemma, in poly]

dvdp_addr [lemma, in poly]

dvdp_gcdl [lemma, in poly]

dvdp_mull [lemma, in poly]

dvdp_map [lemma, in poly]

dvdp_subr [lemma, in poly]

dvdp_subl [lemma, in poly]

dvdp_gcdr [lemma, in poly]

dvdp_add [lemma, in poly]

dvdp_trans [lemma, in poly]

dvdp0 [lemma, in poly]

dvd0n [lemma, in div]

dvd1n [lemma, in div]

dvd1p [lemma, in poly]

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