Z (Global Index)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
Z
Zchar [def, in mathcomp.group_representation.vcharacter]zchar_expansion [prf, in mathcomp.group_representation.vcharacter]
zchar_filter [prf, in mathcomp.group_representation.vcharacter]
zchar_nth_expansion [prf, in mathcomp.group_representation.vcharacter]
zchar_on [prf, in mathcomp.group_representation.vcharacter]
zchar_onG [prf, in mathcomp.group_representation.vcharacter]
zchar_onS [prf, in mathcomp.group_representation.vcharacter]
zchar_small_norm [prf, in mathcomp.group_representation.vcharacter]
zchar_span [prf, in mathcomp.group_representation.vcharacter]
zchar_split [prf, in mathcomp.group_representation.vcharacter]
zchar_sub_irr [prf, in mathcomp.group_representation.vcharacter]
zchar_subseq [prf, in mathcomp.group_representation.vcharacter]
zchar_subset [prf, in mathcomp.group_representation.vcharacter]
zchar_trans [prf, in mathcomp.group_representation.vcharacter]
zchar_trans_on [prf, in mathcomp.group_representation.vcharacter]
zchar_tuple_expansion [prf, in mathcomp.group_representation.vcharacter]
Zchar_zmod [prf, in mathcomp.group_representation.vcharacter]
zcharD1 [prf, in mathcomp.group_representation.vcharacter]
zcharD1E [prf, in mathcomp.group_representation.vcharacter]
zcharW [prf, in mathcomp.group_representation.vcharacter]
zchinese [def, in mathcomp.algebra.intdiv]
zchinese_mod [prf, in mathcomp.algebra.intdiv]
zchinese_modl [prf, in mathcomp.algebra.intdiv]
zchinese_modr [prf, in mathcomp.algebra.intdiv]
zchinese_remainder [prf, in mathcomp.algebra.intdiv]
zcontents [def, in mathcomp.algebra.intdiv]
zcontents0 [prf, in mathcomp.algebra.intdiv]
zcontents_eq0 [prf, in mathcomp.algebra.intdiv]
zcontents_monic [prf, in mathcomp.algebra.intdiv]
zcontents_primitive [prf, in mathcomp.algebra.intdiv]
zcontentsM [prf, in mathcomp.algebra.intdiv]
zcontentsZ [prf, in mathcomp.algebra.intdiv]
zero_lfun [def, in mathcomp.algebra.vector]
zero_lfunE [prf, in mathcomp.algebra.vector]
zeroq [def, in mathcomp.algebra.rat]
Zgroup [def, in mathcomp.solvable.sylow]
ZgroupS [prf, in mathcomp.solvable.sylow]
Zint [def, in mathcomp.algebra.binnums]
Zint0 [prf, in mathcomp.algebra.binnums]
Zint_double [prf, in mathcomp.algebra.binnums]
Zint_eq [prf, in mathcomp.algebra.binnums]
Zint_int_of_Z [prf, in mathcomp.algebra.binnums]
Zint_le [prf, in mathcomp.algebra.binnums]
Zint_neg [prf, in mathcomp.algebra.binnums]
Zint_pos [prf, in mathcomp.algebra.binnums]
Zint_pos_sub [prf, in mathcomp.algebra.binnums]
Zint_pow_pos [prf, in mathcomp.algebra.binnums]
Zint_pred_double [prf, in mathcomp.algebra.binnums]
Zint_spec [ind, in mathcomp.algebra.binnums]
Zint_spec_false [constr, in mathcomp.algebra.binnums]
Zint_spec_Z0 [constr, in mathcomp.algebra.binnums]
Zint_spec_Zneg [constr, in mathcomp.algebra.binnums]
Zint_spec_Zpos [constr, in mathcomp.algebra.binnums]
Zint_succ_double [prf, in mathcomp.algebra.binnums]
ZintB [prf, in mathcomp.algebra.binnums]
ZintD [prf, in mathcomp.algebra.binnums]
ZintE [def, in mathcomp.algebra.binnums]
ZintM [prf, in mathcomp.algebra.binnums]
ZintN [prf, in mathcomp.algebra.binnums]
ZintNeg [constr, in mathcomp.algebra.ssrint]
ZintNull [constr, in mathcomp.algebra.ssrint]
ZintP [prf, in mathcomp.algebra.binnums]
ZintPos [constr, in mathcomp.algebra.ssrint]
zip [def, in mathcomp.boot.seq]
zip_cat [prf, in mathcomp.boot.seq]
zip_map [prf, in mathcomp.boot.seq]
zip_rcons [prf, in mathcomp.boot.seq]
zip_tuple [def, in mathcomp.boot.tuple]
zip_tupleP [prf, in mathcomp.boot.tuple]
zip_uniql [prf, in mathcomp.boot.seq]
zip_uniqr [prf, in mathcomp.boot.seq]
zip_unzip [prf, in mathcomp.boot.seq]
Zisometry_inj [prf, in mathcomp.group_representation.vcharacter]
Zisometry_of_cfnorm [prf, in mathcomp.group_representation.vcharacter]
Zisometry_of_iso [prf, in mathcomp.group_representation.vcharacter]
zmodp [file, in mathcomp.algebra.zmodp]
ZmodQuotient [abbrev, in mathcomp.algebra.ring_quotient]
ZmodQuotient [mod, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Algebra_hasAdd_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Algebra_hasOpp_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Algebra_hasZero_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.axioms_ [rec, in mathcomp.algebra.ring_quotient]
ZmodQuotient.choice_hasChoice_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.class [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.clone [abbrev, in mathcomp.algebra.ring_quotient]
ZmodQuotient.copy [abbrev, in mathcomp.algebra.ring_quotient]
ZmodQuotient.eqtype_hasDecEq_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports [mod, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_AddMagma_and_generic_quotient_EqQuotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_AddMagma_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_AddSemigroup_and_generic_quotient_EqQuotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_AddSemigroup_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_AddUMagma_and_generic_quotient_EqQuotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_AddUMagma_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_BaseAddMagma_and_generic_quotient_EqQuotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_BaseAddMagma_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_BaseAddUMagma_and_generic_quotient_EqQuotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_BaseAddUMagma_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_BaseZmodule_and_generic_quotient_EqQuotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_BaseZmodule_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_ChoiceBaseAddMagma_and_generic_quotient_EqQuotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_ChoiceBaseAddMagma_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_ChoiceBaseAddUMagma_and_generic_quotient_EqQuotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_ChoiceBaseAddUMagma_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_Algebra_Nmodule_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_choice_Choice_and_generic_quotient_EqQuotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_choice_Choice_and_generic_quotient_Quotient [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_generic_quotient_EqQuotient_and_Algebra_Nmodule [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_generic_quotient_EqQuotient_and_Algebra_Zmodule [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.join_ring_quotient_ZmodQuotient_between_generic_quotient_Quotient_and_Algebra_Zmodule [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.Exports.zmodQuotType [abbrev, in mathcomp.algebra.ring_quotient]
ZmodQuotient.generic_quotient_isEqQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.generic_quotient_isQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.on [abbrev, in mathcomp.algebra.ring_quotient]
ZmodQuotient.on_ [abbrev, in mathcomp.algebra.ring_quotient]
ZmodQuotient.pack_ [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.phant_clone [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.phant_on_ [def, in mathcomp.algebra.ring_quotient]
ZmodQuotient.ring_quotient_isZmodQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.sort [proj, in mathcomp.algebra.ring_quotient]
ZmodQuotient.type [rec, in mathcomp.algebra.ring_quotient]
ZmodQuotientElpiOperations [mod, in mathcomp.algebra.ring_quotient]
zmodule [def, in mathcomp.algebra.ssrint]
Zp [def, in mathcomp.algebra.zmodp]
Zp0 [def, in mathcomp.boot.fintype]
Zp1 [def, in mathcomp.boot.fintype]
Zp1 [abbrev, in mathcomp.algebra.zmodp]
Zp1_expgz [prf, in mathcomp.algebra.zmodp]
Zp_abelian [prf, in mathcomp.algebra.zmodp]
Zp_add [def, in mathcomp.boot.fintype]
Zp_add0z [prf, in mathcomp.boot.fintype]
Zp_addA [prf, in mathcomp.boot.fintype]
Zp_addC [prf, in mathcomp.boot.fintype]
Zp_addNz [prf, in mathcomp.boot.fintype]
Zp_cast [prf, in mathcomp.algebra.zmodp]
Zp_cycle [prf, in mathcomp.algebra.zmodp]
Zp_expg [prf, in mathcomp.algebra.zmodp]
Zp_group [def, in mathcomp.algebra.zmodp]
Zp_group_set [prf, in mathcomp.algebra.zmodp]
Zp_intro_unit [prf, in mathcomp.algebra.zmodp]
Zp_inv [def, in mathcomp.boot.fintype]
Zp_inv_out [prf, in mathcomp.boot.fintype]
Zp_isog [prf, in mathcomp.solvable.cyclic]
Zp_isom [prf, in mathcomp.solvable.cyclic]
Zp_mul [def, in mathcomp.boot.fintype]
Zp_mul1z [prf, in mathcomp.algebra.zmodp]
Zp_mul_addl [prf, in mathcomp.boot.fintype]
Zp_mul_addr [prf, in mathcomp.boot.fintype]
Zp_mulA [prf, in mathcomp.boot.fintype]
Zp_mulC [prf, in mathcomp.boot.fintype]
Zp_mulgC [prf, in mathcomp.algebra.zmodp]
Zp_mulrn [prf, in mathcomp.algebra.zmodp]
Zp_mulVz [prf, in mathcomp.algebra.zmodp]
Zp_mulz1 [prf, in mathcomp.algebra.zmodp]
Zp_mulzV [prf, in mathcomp.algebra.zmodp]
Zp_nat [prf, in mathcomp.algebra.zmodp]
Zp_nat_mod [prf, in mathcomp.algebra.zmodp]
Zp_nontrivial [prf, in mathcomp.algebra.zmodp]
Zp_opp [def, in mathcomp.boot.fintype]
Zp_trunc [def, in mathcomp.algebra.zmodp]
Zp_unit_isog [prf, in mathcomp.solvable.cyclic]
Zp_unit_isom [prf, in mathcomp.solvable.cyclic]
Zp_unit_morphism [def, in mathcomp.solvable.cyclic]
Zp_unitm [def, in mathcomp.solvable.cyclic]
Zp_unitmM [prf, in mathcomp.solvable.cyclic]
Zpm [def, in mathcomp.solvable.cyclic]
Zpm_morphism [def, in mathcomp.solvable.cyclic]
ZpmM [prf, in mathcomp.solvable.cyclic]
zpolyEprim [prf, in mathcomp.algebra.intdiv]
zprimitive [def, in mathcomp.algebra.intdiv]
zprimitive0 [prf, in mathcomp.algebra.intdiv]
zprimitive_eq0 [prf, in mathcomp.algebra.intdiv]
zprimitive_id [prf, in mathcomp.algebra.intdiv]
zprimitive_irr [prf, in mathcomp.algebra.intdiv]
zprimitive_min [prf, in mathcomp.algebra.intdiv]
zprimitive_monic [prf, in mathcomp.algebra.intdiv]
zprimitiveM [prf, in mathcomp.algebra.intdiv]
zprimitiveZ [prf, in mathcomp.algebra.intdiv]
ZtoC [abbrev, in mathcomp.field.cyclotomic]
ZtoC [abbrev, in mathcomp.field.algnum]
ZtoC [abbrev, in mathcomp.field.algC]
ZtoQ [abbrev, in mathcomp.field.cyclotomic]
ZtoQ [abbrev, in mathcomp.field.algnum]
ZtoQ [abbrev, in mathcomp.field.algC]