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 | (24263 entries) |
Notation 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 | (1399 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 | (226 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 | (3670 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 | (89 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 | (12297 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 | (383 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 | (45 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 | (114 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 | (279 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 | (1169 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 | (742 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 | (3657 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 | (193 entries) |
P (abbreviation)
p [in mathcomp.algebra.zmodp]p [in mathcomp.algebra.zmodp]
P [in mathcomp.ssreflect.finset]
perm [in mathcomp.fingroup.perm]
perms [in mathcomp.ssreflect.seq]
perm_def [in mathcomp.fingroup.perm]
perm_undup_count [in mathcomp.ssreflect.seq]
perm_eq_iotaP [in mathcomp.ssreflect.seq]
perm_eq_consP [in mathcomp.ssreflect.seq]
perm_eq_nilP [in mathcomp.ssreflect.seq]
perm_eq_small [in mathcomp.ssreflect.seq]
perm_eq_all [in mathcomp.ssreflect.seq]
perm_eq_flatten [in mathcomp.ssreflect.seq]
perm_eq_rev [in mathcomp.ssreflect.seq]
perm_eq_uniq [in mathcomp.ssreflect.seq]
perm_eq_mem [in mathcomp.ssreflect.seq]
perm_eq_size [in mathcomp.ssreflect.seq]
perm_eq_trans [in mathcomp.ssreflect.seq]
perm_eq_sym [in mathcomp.ssreflect.seq]
perm_eq_refl [in mathcomp.ssreflect.seq]
perm_eqlE [in mathcomp.ssreflect.seq]
perm_eqrP [in mathcomp.ssreflect.seq]
perm_eqlP [in mathcomp.ssreflect.seq]
perm_eqP [in mathcomp.ssreflect.seq]
perm_tseq [in mathcomp.ssreflect.seq]
perm_eqr [in mathcomp.ssreflect.seq]
perm_eql [in mathcomp.ssreflect.seq]
perm_eqr [in mathcomp.ssreflect.seq]
perm_eql [in mathcomp.ssreflect.seq]
pfamily [in mathcomp.ssreflect.finfun]
pffun_on [in mathcomp.ssreflect.finfun]
pFtoE [in mathcomp.algebra.polyXY]
PiConst [in mathcomp.ssreflect.generic_quotient]
piE [in mathcomp.ssreflect.generic_quotient]
PiEmbed [in mathcomp.ssreflect.generic_quotient]
PiMono1 [in mathcomp.ssreflect.generic_quotient]
PiMono2 [in mathcomp.ssreflect.generic_quotient]
PiMorph [in mathcomp.ssreflect.generic_quotient]
PiMorph1 [in mathcomp.ssreflect.generic_quotient]
PiMorph11 [in mathcomp.ssreflect.generic_quotient]
PiMorph2 [in mathcomp.ssreflect.generic_quotient]
pprod [in mathcomp.fingroup.gproduct]
pprod [in mathcomp.fingroup.gproduct]
pQtoC [in mathcomp.field.algC]
pQtoC [in mathcomp.field.cyclotomic]
pQtoC [in mathcomp.field.algnum]
predn [in mathcomp.ssreflect.ssrnat]
predOfType [in mathcomp.ssreflect.finset]
pred_of_set [in mathcomp.ssreflect.finset]
pred_of_set_def [in mathcomp.ssreflect.finset]
pT [in mathcomp.fingroup.perm]
Px [in mathcomp.field.galois]
pZtoC [in mathcomp.field.algC]
pZtoC [in mathcomp.field.cyclotomic]
pZtoC [in mathcomp.field.algnum]
pZtoQ [in mathcomp.field.algC]
pZtoQ [in mathcomp.algebra.intdiv]
pZtoQ [in mathcomp.field.cyclotomic]
pZtoQ [in mathcomp.field.algnum]
p_A [in mathcomp.algebra.mxpoly]
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 | (24263 entries) |
Notation 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 | (1399 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 | (226 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 | (3670 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 | (89 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 | (12297 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 | (383 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 | (45 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 | (114 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 | (279 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 | (1169 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 | (742 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 | (3657 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 | (193 entries) |