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

## D

DecFieldMixin [abbreviation, in ssralg]DecFieldType [abbreviation, in ssralg]

decFieldType [abbreviation, in ssralg]

DecidableField [module, in ssralg]

decP [definition, in ssrbool]

decPcases [lemma, in ssrbool]

Def [section, in finfun]

Def [section, in tuple]

Def.aT [variable, in finfun]

Def.n [variable, in tuple]

Def.rT [variable, in finfun]

Def.T [variable, in tuple]

delta_mx [definition, in matrix]

dependentReturnType [definition, in ssreflect]

der1_subG [lemma, in groups]

determinant [definition, in matrix]

Determinant [section, in matrix]

Determinant.R [variable, in matrix]

determinant_multilinear [lemma, in matrix]

detM [lemma, in matrix]

det1 [lemma, in matrix]

det_invmx [lemma, in matrix]

det_lblock [lemma, in matrix]

det_mulmx [lemma, in matrix]

det_perm_mx [lemma, in matrix]

det_perm_mx_neq0 [lemma, in matrix]

det_scalar [lemma, in matrix]

det_scalar1 [lemma, in matrix]

det_scalemx [lemma, in matrix]

det_trmx [lemma, in matrix]

det_ublock [lemma, in matrix]

dfs [definition, in connect]

dfsP [lemma, in connect]

DfsPath [constructor, in connect]

dfs_path [inductive, in connect]

diff_root [definition, in poly]

dinjectiveb [definition, in fintype]

dinjectiveP [lemma, in fintype]

dinjectivePn [lemma, in fintype]

disjoint [definition, in fintype]

disjointEsetI [lemma, in finset]

disjoints_subset [lemma, in finset]

disjointU [lemma, in fintype]

disjointU1 [lemma, in fintype]

disjoint0 [lemma, in fintype]

disjoint1 [lemma, in fintype]

disjoint_cat [lemma, in fintype]

disjoint_cons [lemma, in fintype]

disjoint_has [lemma, in fintype]

disjoint_setI0 [lemma, in finset]

disjoint_subset [lemma, in fintype]

disjoint_sym [lemma, in fintype]

disjoint_trans [lemma, in fintype]

Distributivity [section, in bigops]

Distributivity.one [variable, in bigops]

Distributivity.plus [variable, in bigops]

Distributivity.R [variable, in bigops]

Distributivity.times [variable, in bigops]

Distributivity.zero [variable, in bigops]

div [library]

divgI [lemma, in groups]

divgS [lemma, in groups]

divg_index [lemma, in groups]

divisorn [lemma, in prime]

divisors [definition, in prime]

divisors_correct [lemma, in prime]

divisors_uniq [lemma, in prime]

divisor1 [lemma, in prime]

divn [definition, in div]

divnAC [lemma, in div]

divnK [lemma, in div]

divnn [lemma, in div]

divn0 [lemma, in div]

divn1 [lemma, in div]

divn2 [lemma, in div]

divn_addl [lemma, in div]

divn_addl_mul [lemma, in div]

divn_addr [lemma, in div]

divn_divl [lemma, in div]

divn_divr [lemma, in div]

divn_eq [lemma, in div]

divn_gt0 [lemma, in div]

divn_mulA [lemma, in div]

divn_mulAC [lemma, in div]

divn_mulCA [lemma, in div]

divn_pmul2l [lemma, in div]

divn_pmul2r [lemma, in div]

divn_small [lemma, in div]

divp [definition, in poly]

divp1 [lemma, in poly]

divp_mon_mull [lemma, in poly]

divp_mon_spec [lemma, in poly]

divp_mull [lemma, in poly]

divp_size [lemma, in poly]

divp_spec [lemma, in poly]

div0n [lemma, in div]

div0p [lemma, in poly]

div_ring_mul_group_cyclic [lemma, in cyclic]

dom [definition, in morphisms]

dom_ker [lemma, in morphisms]

dotmx_paste [lemma, in matrix]

double [definition, in ssrnat]

doubleE [lemma, in ssrnat]

doubleK [lemma, in ssrnat]

doubleS [lemma, in ssrnat]

double0 [lemma, in ssrnat]

double_add [lemma, in ssrnat]

double_eq0 [lemma, in ssrnat]

double_gt0 [lemma, in ssrnat]

double_inj [definition, in ssrnat]

double_mull [lemma, in ssrnat]

double_mulr [lemma, in ssrnat]

double_rec [definition, in ssrnat]

double_sub [lemma, in ssrnat]

dpair [definition, in perm]

drop [definition, in seq]

drop0 [lemma, in seq]

drop1 [lemma, in seq]

drop_behead [lemma, in seq]

drop_cat [lemma, in seq]

drop_cons [lemma, in seq]

drop_nth [lemma, in seq]

drop_oversize [lemma, in seq]

drop_rcons [lemma, in seq]

drop_size [lemma, in seq]

drop_size_cat [lemma, in seq]

drop_tuple [definition, in tuple]

drop_tupleP [lemma, in tuple]

dvdn [definition, in div]

dvdnn [lemma, in div]

dvdnP [lemma, in div]

dvdn0 [lemma, in div]

dvdn1 [lemma, in div]

dvdn2 [lemma, in div]

dvdn_add [lemma, in div]

dvdn_addl [lemma, in div]

dvdn_addr [lemma, in div]

dvdn_add_eq [lemma, in div]

dvdn_divisors [lemma, in prime]

dvdn_eq [lemma, in div]

dvdn_exp [lemma, in div]

dvdn_gcd [lemma, in div]

dvdn_gcdl [lemma, in div]

dvdn_gcdr [lemma, in div]

dvdn_gt0 [lemma, in div]

dvdn_indexg [lemma, in groups]

dvdn_lcm [lemma, in div]

dvdn_lcml [lemma, in div]

dvdn_lcmr [lemma, in div]

dvdn_leq [lemma, in div]

dvdn_leq_log [lemma, in prime]

dvdn_morphim [lemma, in normal]

dvdn_mul [lemma, in div]

dvdn_mull [lemma, in div]

dvdn_mulr [lemma, in div]

dvdn_part [lemma, in prime]

dvdn_partP [lemma, in prime]

dvdn_pdiv [lemma, in prime]

dvdn_pfactor [lemma, in prime]

dvdn_pmul2l [lemma, in div]

dvdn_pmul2r [lemma, in div]

dvdn_prime2 [lemma, in prime]

dvdn_quotient [lemma, in normal]

dvdn_sub [lemma, in div]

dvdn_subl [lemma, in div]

dvdn_subr [lemma, in div]

dvdn_sum [lemma, in prime]

dvdn_trans [lemma, in div]

dvdp [definition, in poly]

dvdpp [lemma, in poly]

dvdpPc [lemma, in poly]

dvdpPm [lemma, in poly]

dvdp0 [lemma, in poly]

dvdp_add [lemma, in poly]

dvdp_addl [lemma, in poly]

dvdp_addr [lemma, in poly]

dvdp_add_eq [lemma, in poly]

dvdp_gcd [lemma, in poly]

dvdp_gcdl [lemma, in poly]

dvdp_gcdr [lemma, in poly]

dvdp_gcd2 [lemma, in poly]

dvdp_mod [lemma, in poly]

dvdp_mon_mull [lemma, in poly]

dvdp_mul [lemma, in poly]

dvdp_mull [lemma, in poly]

dvdp_mulr [lemma, in poly]

dvdp_sub [lemma, in poly]

dvdp_subl [lemma, in poly]

dvdp_subr [lemma, in poly]

dvdp_trans [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 | _ | (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) |