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

## P (definition)

pairmap [in seq]pairmap_tuple [in tuple]

pair_eq [in eqtype]

pair_of_tag [in choice]

partition [in finset]

partn [in prime]

pastemx [in matrix]

path [in paths]

pcancel [in ssrfun]

PcanChoiceMixin [in choice]

PcanCountMixin [in choice]

PcanEqMixin [in eqtype]

PcanFinMixin [in fintype]

pcomp [in ssrfun]

pcycle [in perm]

pcycles [in perm]

pdiv [in prime]

PermDef.fun_of_perm [in perm]

PermDef.perm [in perm]

perm_baseFinGroupType [in perm]

perm_choiceMixin [in perm]

perm_choiceType [in perm]

perm_countMixin [in perm]

perm_countType [in perm]

perm_eq [in seq]

perm_eqMixin [in perm]

perm_eqType [in perm]

perm_finGroupType [in perm]

perm_finMixin [in perm]

perm_finType [in perm]

perm_for_choiceType [in perm]

perm_for_countType [in perm]

perm_for_eqType [in perm]

perm_for_finType [in perm]

perm_for_subCountType [in perm]

perm_for_subFinType [in perm]

perm_for_subType [in perm]

perm_in [in automorphism]

perm_inv [in perm]

perm_mul [in perm]

perm_mx [in matrix]

perm_of [in perm]

perm_of_baseFinGroupMixin [in perm]

perm_of_baseFinGroupType [in perm]

perm_of_finGroupType [in perm]

perm_on [in perm]

perm_one [in perm]

perm_subCountType [in perm]

perm_subFinType [in perm]

perm_subType [in perm]

perm_unlock [in perm]

pfactor [in prime]

pfamily [in finfun]

pffun_on [in finfun]

phi [in charpoly]

phi [in prime]

pick [in fintype]

pickle [in choice]

pickle_inv [in choice]

pi_of [in prime]

pmap [in seq]

pnat [in prime]

Poly [in poly]

polyC [in poly]

polynomial_choiceMixin [in poly]

polynomial_choiceType [in poly]

polynomial_comRingType [in poly]

polynomial_comUnitRingType [in poly]

polynomial_eqMixin [in poly]

polynomial_eqType [in poly]

polynomial_idomainType [in poly]

polynomial_ringType [in poly]

polynomial_subType [in poly]

polynomial_unitRingType [in poly]

polynomial_zmodType [in poly]

polyX [in poly]

poly_choiceType [in poly]

poly_comRingType [in poly]

poly_comUnitRingType [in poly]

poly_cons [in poly]

poly_eqType [in poly]

poly_idomainType [in poly]

poly_inv [in poly]

poly_of [in poly]

poly_ringMixin [in poly]

poly_ringType [in poly]

poly_subType [in poly]

poly_unit [in poly]

poly_unitRingMixin [in poly]

poly_unitRingType [in poly]

poly_zmodMixin [in poly]

poly_zmodType [in poly]

pop_succn [in ssrnat]

pos_nat_choiceMixin [in choice]

pos_nat_choiceType [in choice]

pos_nat_countMixin [in choice]

pos_nat_countType [in choice]

pos_nat_eqMixin [in ssrnat]

pos_nat_eqType [in ssrnat]

pos_nat_subCountType [in choice]

pos_nat_subType [in ssrnat]

pos_of_nat [in ssrnat]

powerset [in finfun]

pred [in ssrbool]

predArgType [in ssrbool]

predC [in ssrbool]

predC1 [in eqtype]

predD [in ssrbool]

predD1 [in eqtype]

predI [in ssrbool]

predn [in ssrnat]

predPredType [in ssrbool]

predT [in ssrbool]

predU [in ssrbool]

predU1 [in eqtype]

predX [in eqtype]

pred0 [in ssrbool]

pred0b [in fintype]

pred1 [in eqtype]

pred2 [in eqtype]

pred3 [in eqtype]

pred4 [in eqtype]

pred_of_argType [in ssrbool]

pred_of_eq_seq [in seq]

pred_of_mem [in ssrbool]

pred_of_mem_pred [in ssrbool]

pred_of_set_unlock [in finset]

pred_of_simpl [in ssrbool]

preim [in ssrbool]

preimset [in finset]

preim_at [in finset]

preim_partition [in finset]

preim_seq [in fintype]

prev [in paths]

prev_at [in paths]

pre_symmetric [in ssrbool]

prime [in prime]

primes [in prime]

prime_decomp [in prime]

prime_decomp_rec [in prime]

prime_pos_nat [in prime]

prod_choiceMixin [in choice]

prod_choiceType [in choice]

prod_countMixin [in choice]

prod_countType [in choice]

prod_enum [in fintype]

prod_eqMixin [in eqtype]

prod_eqType [in eqtype]

prod_finMixin [in fintype]

prod_finType [in fintype]

proper [in fintype]

prop_in1 [in ssrbool]

prop_in11 [in ssrbool]

prop_in111 [in ssrbool]

prop_in12 [in ssrbool]

prop_in2 [in ssrbool]

prop_in21 [in ssrbool]

prop_in3 [in ssrbool]

prop_on1 [in ssrbool]

prop_on2 [in ssrbool]

protect_term [in ssreflect]

pval [in perm]

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