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 | (24947 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 | (1496 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 | (216 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 | (3586 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 | (84 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 | (11878 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 | (389 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 | (49 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 | (119 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 | (272 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 | (1128 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 | (701 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 | (4837 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 | (192 entries) |

## Z

Zchar [section, in mathcomp.character.vcharacter]Zchar [definition, in mathcomp.character.vcharacter]

zcharD1 [lemma, in mathcomp.character.vcharacter]

zcharD1E [lemma, in mathcomp.character.vcharacter]

zcharW [lemma, in mathcomp.character.vcharacter]

zchar_small_norm [lemma, in mathcomp.character.vcharacter]

zchar_filter [lemma, in mathcomp.character.vcharacter]

zchar_subseq [lemma, in mathcomp.character.vcharacter]

zchar_subset [lemma, in mathcomp.character.vcharacter]

zchar_sub_irr [lemma, in mathcomp.character.vcharacter]

zchar_trans_on [lemma, in mathcomp.character.vcharacter]

zchar_trans [lemma, in mathcomp.character.vcharacter]

zchar_span [lemma, in mathcomp.character.vcharacter]

zchar_expansion [lemma, in mathcomp.character.vcharacter]

zchar_tuple_expansion [lemma, in mathcomp.character.vcharacter]

zchar_nth_expansion [lemma, in mathcomp.character.vcharacter]

zchar_onG [lemma, in mathcomp.character.vcharacter]

zchar_onS [lemma, in mathcomp.character.vcharacter]

zchar_on [lemma, in mathcomp.character.vcharacter]

zchar_split [lemma, in mathcomp.character.vcharacter]

Zchar_zmodPred [definition, in mathcomp.character.vcharacter]

Zchar_addrPred [definition, in mathcomp.character.vcharacter]

Zchar_opprPred [definition, in mathcomp.character.vcharacter]

Zchar_zmod [lemma, in mathcomp.character.vcharacter]

Zchar_keyed [definition, in mathcomp.character.vcharacter]

Zchar_key [lemma, in mathcomp.character.vcharacter]

Zchar.G [variable, in mathcomp.character.vcharacter]

Zchar.gT [variable, in mathcomp.character.vcharacter]

zchinese [definition, in mathcomp.algebra.intdiv]

zchinese_mod [lemma, in mathcomp.algebra.intdiv]

zchinese_modr [lemma, in mathcomp.algebra.intdiv]

zchinese_modl [lemma, in mathcomp.algebra.intdiv]

zchinese_remainder [lemma, in mathcomp.algebra.intdiv]

zcontents [definition, in mathcomp.algebra.intdiv]

zcontentsM [lemma, in mathcomp.algebra.intdiv]

zcontentsZ [lemma, in mathcomp.algebra.intdiv]

zcontents_primitive [lemma, in mathcomp.algebra.intdiv]

zcontents_monic [lemma, in mathcomp.algebra.intdiv]

zcontents_eq0 [lemma, in mathcomp.algebra.intdiv]

zcontents0 [lemma, in mathcomp.algebra.intdiv]

zeroq [definition, in mathcomp.algebra.rat]

zero_lfunE [lemma, in mathcomp.algebra.vector]

zero_lfun [definition, in mathcomp.algebra.vector]

Zgroup [definition, in mathcomp.solvable.sylow]

ZgroupS [lemma, in mathcomp.solvable.sylow]

Zgroups [section, in mathcomp.solvable.sylow]

Zgroups.D [variable, in mathcomp.solvable.sylow]

Zgroups.f [variable, in mathcomp.solvable.sylow]

Zgroups.gT [variable, in mathcomp.solvable.sylow]

Zgroups.rT [variable, in mathcomp.solvable.sylow]

ZintLmod [section, in mathcomp.algebra.ssrint]

ZintLmod.M [variable, in mathcomp.algebra.ssrint]

_ ^z (type_scope) [notation, in mathcomp.algebra.ssrint]

ZintNeg [constructor, in mathcomp.algebra.ssrint]

ZintNull [constructor, in mathcomp.algebra.ssrint]

ZintPos [constructor, in mathcomp.algebra.ssrint]

zip [definition, in mathcomp.ssreflect.seq]

Zip [section, in mathcomp.ssreflect.seq]

zip_tuple [definition, in mathcomp.ssreflect.tuple]

zip_tupleP [lemma, in mathcomp.ssreflect.tuple]

zip_rcons [lemma, in mathcomp.ssreflect.seq]

zip_cat [lemma, in mathcomp.ssreflect.seq]

zip_unzip [lemma, in mathcomp.ssreflect.seq]

Zip.S [variable, in mathcomp.ssreflect.seq]

Zip.T [variable, in mathcomp.ssreflect.seq]

Zisometry_inj [lemma, in mathcomp.character.vcharacter]

Zisometry_of_iso [lemma, in mathcomp.character.vcharacter]

Zisometry_of_cfnorm [lemma, in mathcomp.character.vcharacter]

zmodp [library]

ZmodQuot [section, in mathcomp.algebra.ring_quotient]

ZmodQuotClass [constructor, in mathcomp.algebra.ring_quotient]

ZmodQuotMixin [abbreviation, in mathcomp.algebra.ring_quotient]

ZmodQuotMixinPack [constructor, in mathcomp.algebra.ring_quotient]

ZmodQuotMixin_pack [definition, in mathcomp.algebra.ring_quotient]

ZmodQuotType [abbreviation, in mathcomp.algebra.ring_quotient]

zmodQuotType [record, in mathcomp.algebra.ring_quotient]

ZmodQuotTypePack [constructor, in mathcomp.algebra.ring_quotient]

ZmodQuotType_clone [definition, in mathcomp.algebra.ring_quotient]

ZmodQuotType_pack [definition, in mathcomp.algebra.ring_quotient]

zmodQuotType_eqQuotType [definition, in mathcomp.algebra.ring_quotient]

zmodQuotType_quotType [definition, in mathcomp.algebra.ring_quotient]

zmodQuotType_zmodType [definition, in mathcomp.algebra.ring_quotient]

zmodQuotType_choiceType [definition, in mathcomp.algebra.ring_quotient]

zmodQuotType_eqType [definition, in mathcomp.algebra.ring_quotient]

ZmodQuot.addT [variable, in mathcomp.algebra.ring_quotient]

ZmodQuot.eqT [variable, in mathcomp.algebra.ring_quotient]

ZmodQuot.oppT [variable, in mathcomp.algebra.ring_quotient]

ZmodQuot.T [variable, in mathcomp.algebra.ring_quotient]

ZmodQuot.zeroT [variable, in mathcomp.algebra.ring_quotient]

zmodule [definition, in mathcomp.algebra.ssrint]

zmod_quot_mixinP [lemma, in mathcomp.algebra.ring_quotient]

zmod_eq_quot_class [definition, in mathcomp.algebra.ring_quotient]

zmod_quot_class [definition, in mathcomp.algebra.ring_quotient]

zmod_quot_sort [projection, in mathcomp.algebra.ring_quotient]

zmod_quot_mixin [projection, in mathcomp.algebra.ring_quotient]

zmod_quot_zmod_class [projection, in mathcomp.algebra.ring_quotient]

zmod_quot_quot_class [projection, in mathcomp.algebra.ring_quotient]

zmod_quot_class_of [record, in mathcomp.algebra.ring_quotient]

zmod_eq_quot_mixin [projection, in mathcomp.algebra.ring_quotient]

zmod_quot_mixin_of [record, in mathcomp.algebra.ring_quotient]

Znat [definition, in mathcomp.algebra.ssrint]

ZnatP [lemma, in mathcomp.algebra.ssrint]

ZnatPred [section, in mathcomp.algebra.ssrint]

Znat_semiringPred [definition, in mathcomp.algebra.ssrint]

Znat_mulrPred [definition, in mathcomp.algebra.ssrint]

Znat_addrPred [definition, in mathcomp.algebra.ssrint]

Znat_semiring_closed [lemma, in mathcomp.algebra.ssrint]

Znat_def [lemma, in mathcomp.algebra.ssrint]

Znat_keyd [definition, in mathcomp.algebra.ssrint]

Znat_key [lemma, in mathcomp.algebra.ssrint]

Zp [definition, in mathcomp.algebra.zmodp]

ZpDef [section, in mathcomp.algebra.zmodp]

ZpDef.p' [variable, in mathcomp.algebra.zmodp]

Zpm [definition, in mathcomp.solvable.cyclic]

ZpmM [lemma, in mathcomp.solvable.cyclic]

Zpm_morphism [definition, in mathcomp.solvable.cyclic]

zpolyEprim [lemma, in mathcomp.algebra.intdiv]

ZpolyScale [section, in mathcomp.algebra.intdiv]

zprimitive [definition, in mathcomp.algebra.intdiv]

zprimitiveM [lemma, in mathcomp.algebra.intdiv]

zprimitiveZ [lemma, in mathcomp.algebra.intdiv]

zprimitive_irr [lemma, in mathcomp.algebra.intdiv]

zprimitive_min [lemma, in mathcomp.algebra.intdiv]

zprimitive_monic [lemma, in mathcomp.algebra.intdiv]

zprimitive_id [lemma, in mathcomp.algebra.intdiv]

zprimitive_eq0 [lemma, in mathcomp.algebra.intdiv]

zprimitive0 [lemma, in mathcomp.algebra.intdiv]

ZpRing [section, in mathcomp.algebra.zmodp]

ZpRing.p' [variable, in mathcomp.algebra.zmodp]

Zp_countComUnitRingType [definition, in mathcomp.field.countalg]

Zp_countUnitRingType [definition, in mathcomp.field.countalg]

Zp_countComRingType [definition, in mathcomp.field.countalg]

Zp_countRingType [definition, in mathcomp.field.countalg]

Zp_countZmodType [definition, in mathcomp.field.countalg]

Zp_group [definition, in mathcomp.algebra.zmodp]

Zp_group_set [lemma, in mathcomp.algebra.zmodp]

Zp_nat_mod [lemma, in mathcomp.algebra.zmodp]

Zp_cast [lemma, in mathcomp.algebra.zmodp]

Zp_trunc [definition, in mathcomp.algebra.zmodp]

Zp_nat [lemma, in mathcomp.algebra.zmodp]

Zp_finComUnitRingType [definition, in mathcomp.algebra.zmodp]

Zp_comUnitRingType [definition, in mathcomp.algebra.zmodp]

Zp_finUnitRingType [definition, in mathcomp.algebra.zmodp]

Zp_unitRingType [definition, in mathcomp.algebra.zmodp]

Zp_unitRingMixin [definition, in mathcomp.algebra.zmodp]

Zp_finComRingType [definition, in mathcomp.algebra.zmodp]

Zp_comRingType [definition, in mathcomp.algebra.zmodp]

Zp_finRingType [definition, in mathcomp.algebra.zmodp]

Zp_ringType [definition, in mathcomp.algebra.zmodp]

Zp_ringMixin [definition, in mathcomp.algebra.zmodp]

Zp_nontrivial [lemma, in mathcomp.algebra.zmodp]

Zp_cycle [lemma, in mathcomp.algebra.zmodp]

Zp_expg [lemma, in mathcomp.algebra.zmodp]

Zp_abelian [lemma, in mathcomp.algebra.zmodp]

Zp_mulgC [lemma, in mathcomp.algebra.zmodp]

Zp_mulrn [lemma, in mathcomp.algebra.zmodp]

Zp_inv_out [lemma, in mathcomp.algebra.zmodp]

Zp_intro_unit [lemma, in mathcomp.algebra.zmodp]

Zp_mulzV [lemma, in mathcomp.algebra.zmodp]

Zp_mulVz [lemma, in mathcomp.algebra.zmodp]

Zp_mul_addl [lemma, in mathcomp.algebra.zmodp]

Zp_mul_addr [lemma, in mathcomp.algebra.zmodp]

Zp_mulA [lemma, in mathcomp.algebra.zmodp]

Zp_mulz1 [lemma, in mathcomp.algebra.zmodp]

Zp_mulC [lemma, in mathcomp.algebra.zmodp]

Zp_mul1z [lemma, in mathcomp.algebra.zmodp]

Zp_finGroupType [definition, in mathcomp.algebra.zmodp]

Zp_baseFinGroupType [definition, in mathcomp.algebra.zmodp]

Zp_finZmodType [definition, in mathcomp.algebra.zmodp]

Zp_zmodType [definition, in mathcomp.algebra.zmodp]

Zp_zmodMixin [definition, in mathcomp.algebra.zmodp]

Zp_addC [lemma, in mathcomp.algebra.zmodp]

Zp_addA [lemma, in mathcomp.algebra.zmodp]

Zp_addNz [lemma, in mathcomp.algebra.zmodp]

Zp_add0z [lemma, in mathcomp.algebra.zmodp]

Zp_inv [definition, in mathcomp.algebra.zmodp]

Zp_mul [definition, in mathcomp.algebra.zmodp]

Zp_add [definition, in mathcomp.algebra.zmodp]

Zp_opp [definition, in mathcomp.algebra.zmodp]

Zp_unit_isog [lemma, in mathcomp.solvable.cyclic]

Zp_unit_isom [lemma, in mathcomp.solvable.cyclic]

Zp_unit_morphism [definition, in mathcomp.solvable.cyclic]

Zp_unitmM [lemma, in mathcomp.solvable.cyclic]

Zp_unitm [definition, in mathcomp.solvable.cyclic]

Zp_isog [lemma, in mathcomp.solvable.cyclic]

Zp_isom [lemma, in mathcomp.solvable.cyclic]

Zp0 [definition, in mathcomp.algebra.zmodp]

Zp1 [definition, in mathcomp.algebra.zmodp]

Zp1_expgz [lemma, in mathcomp.algebra.zmodp]

ZtoC [abbreviation, in mathcomp.field.algC]

ZtoC [abbreviation, in mathcomp.field.cyclotomic]

ZtoC [abbreviation, in mathcomp.field.algnum]

ZtoQ [abbreviation, in mathcomp.field.algC]

ZtoQ [abbreviation, in mathcomp.field.cyclotomic]

ZtoQ [abbreviation, in mathcomp.field.algnum]

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 | (24947 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 | (1496 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 | (216 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 | (3586 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 | (84 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 | (11878 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 | (389 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 | (49 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 | (119 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 | (272 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 | (1128 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 | (701 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 | (4837 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 | (192 entries) |