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

## 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_zmod [lemma, 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_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]

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_semiring_closed [lemma, in mathcomp.algebra.ssrint]

Znat_def [lemma, 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]

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