E (Definitions)
| 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 |
E (Definitions)
eclassicType [def, in mathcomp.classical.boolp]ecubes [def, in mathcomp.solvable.burnside_app]
edist [def, in mathcomp.analysis.normedtype_theory.urysohn]
edist_inf [def, in mathcomp.analysis.normedtype_theory.urysohn]
edivn [def, in mathcomp.boot.div]
edivn_rec [def, in mathcomp.boot.div]
ednatmul [def, in mathcomp.reals.constructive_ereal]
egcdn [def, in mathcomp.boot.div]
egcdn_rec [def, in mathcomp.boot.div]
egcdz [def, in mathcomp.algebra.intdiv]
eigenpoly [def, in mathcomp.algebra.mxpoly]
eigenspace [def, in mathcomp.algebra.mxalgebra]
eigenvalue [def, in mathcomp.algebra.mxalgebra]
einfs [def, in mathcomp.analysis.sequences]
elebesgue_measure [def, in mathcomp.analysis.lebesgue_measure]
eltm [def, in mathcomp.solvable.cyclic]
eltm_morphism [def, in mathcomp.solvable.cyclic]
emeasurable [def, in mathcomp.analysis.measurable_realfun]
Empty.pack_ [def, in mathcomp.classical.classical_sets]
Empty.phant_clone [def, in mathcomp.classical.classical_sets]
Empty.phant_on_ [def, in mathcomp.classical.classical_sets]
empty_itv [def, in mathcomp.algebra.interval_inference]
emptyE [def, in mathcomp.classical.cardinality]
emptyE_subdef [def, in mathcomp.classical.cardinality]
enatmul [def, in mathcomp.reals.constructive_ereal]
enc_mod_rel_equiv_rel [def, in mathcomp.boot.generic_quotient]
encModEquivP [def, in mathcomp.boot.generic_quotient]
encModRelClass [def, in mathcomp.boot.generic_quotient]
encModRelE [def, in mathcomp.boot.generic_quotient]
encModRelP [def, in mathcomp.boot.generic_quotient]
encoded_equiv [def, in mathcomp.boot.generic_quotient]
encoded_equiv_equiv_rel [def, in mathcomp.boot.generic_quotient]
entourage [def, in mathcomp.analysis.topology_theory.uniform_structure]
entourage_ [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
entourage_filter [def, in mathcomp.analysis.topology_theory.uniform_structure]
entourage_set [def, in mathcomp.analysis.topology_theory.uniform_structure]
enum_extremal_groups [def, in mathcomp.solvable.extremal]
enum_fin [def, in mathcomp.finmap.finmap]
enum_finmem [def, in mathcomp.finmap.finmap]
enum_finpred [def, in mathcomp.finmap.finmap]
enum_mem [def, in mathcomp.boot.fintype]
enum_mset_unlock [def, in mathcomp.finmap.multiset]
enum_prob [def, in mathcomp.analysis.probability_theory.random_variable]
enum_rank [def, in mathcomp.boot.fintype]
enum_rank_in.body [def, in mathcomp.boot.fintype]
enum_rank_in.unlock [def, in mathcomp.boot.fintype]
enum_rank_in_unlock_subterm [def, in mathcomp.boot.fintype]
enum_subdef [def, in mathcomp.boot.fintype]
enum_tuple [def, in mathcomp.boot.tuple]
enum_val [def, in mathcomp.boot.fintype]
EnumMset.E [def, in mathcomp.finmap.multiset]
EnumMset.f [def, in mathcomp.finmap.multiset]
enumP_subdef [def, in mathcomp.boot.fintype]
eq_axiom [def, in mathcomp.boot.eqtype]
eq_comparable [def, in mathcomp.boot.eqtype]
Eq_dep_eq [def, in mathcomp.classical.internal_Eqdep_dec]
Eq_dep_eq_on [def, in mathcomp.classical.internal_Eqdep_dec]
eq_ereal [def, in mathcomp.reals.constructive_ereal]
eq_op [def, in mathcomp.boot.eqtype]
Eq_rect_eq [def, in mathcomp.classical.internal_Eqdep_dec]
Eq_rect_eq_on [def, in mathcomp.classical.internal_Eqdep_dec]
eq_shift [def, in mathcomp.boot.fintype]
eqAmod [def, in mathcomp.field.algnum]
eqb [def, in mathcomp.boot.eqtype]
eqC_nat [def, in mathcomp.field.algC]
eqincl [def, in mathcomp.classical.functions]
eqmx [def, in mathcomp.algebra.mxalgebra]
eqn [def, in mathcomp.boot.ssrnat]
eqP [def, in mathcomp.boot.eqtype]
EqQuotient.Exports.join_generic_quotient_EqQuotient_between_eqtype_Equality_and_generic_quotient_Quotient [def, in mathcomp.boot.generic_quotient]
EqQuotient.pack_ [def, in mathcomp.boot.generic_quotient]
EqQuotient.phant_clone [def, in mathcomp.boot.generic_quotient]
EqQuotient.phant_on_ [def, in mathcomp.boot.generic_quotient]
eqseq [def, in mathcomp.boot.seq]
equal_to_pi [def, in mathcomp.boot.generic_quotient]
Equality.pack_ [def, in mathcomp.boot.eqtype]
Equality.phant_clone [def, in mathcomp.boot.eqtype]
Equality.phant_on_ [def, in mathcomp.boot.eqtype]
equicontinuous [def, in mathcomp.analysis.topology_theory.function_spaces]
equiv_class [def, in mathcomp.boot.generic_quotient]
equiv_pack [def, in mathcomp.boot.generic_quotient]
equiv_subfext [def, in mathcomp.field.fieldext]
equiv_subfext_encModRel [def, in mathcomp.field.fieldext]
equiv_subfext_equiv [def, in mathcomp.field.fieldext]
equivalence_partition [def, in mathcomp.boot.finset]
equivmx [def, in mathcomp.algebra.mxalgebra]
equivmx_spec [def, in mathcomp.algebra.mxalgebra]
EquivQuot.canon [def, in mathcomp.boot.generic_quotient]
EquivQuot.encD_equiv_rel [def, in mathcomp.boot.generic_quotient]
EquivQuot.pi [def, in mathcomp.boot.generic_quotient]
EquivQuot.type_of [def, in mathcomp.boot.generic_quotient]
er_map [def, in mathcomp.reals.constructive_ereal]
ereal_ball [def, in mathcomp.reals.constructive_ereal]
ereal_dnbhs [def, in mathcomp.analysis.ereal]
ereal_inf [def, in mathcomp.analysis.ereal]
ereal_inf_inum [def, in mathcomp.analysis.ereal]
ereal_isMeasurable [def, in mathcomp.analysis.measurable_realfun]
ereal_loc_seq [def, in mathcomp.analysis.ereal]
ereal_nbhs [def, in mathcomp.analysis.ereal]
ereal_of_itv_bound [def, in mathcomp.reals.real_interval]
ereal_sup [def, in mathcomp.analysis.ereal]
ereal_sup_inum [def, in mathcomp.analysis.ereal]
ErealGenCInfty.G [def, in mathcomp.analysis.measurable_realfun]
ErealGenInftyO.G [def, in mathcomp.analysis.measurable_realfun]
ErealGenOInfty.G [def, in mathcomp.analysis.measurable_realfun]
eseries [def, in mathcomp.analysis.sequences]
ess_inf [def, in mathcomp.analysis.ess_sup_inf]
ess_sup [def, in mathcomp.analysis.ess_sup_inf]
esum [def, in mathcomp.analysis.esum]
esups [def, in mathcomp.analysis.sequences]
etagged [def, in mathcomp.boot.eqtype]
etelescope [def, in mathcomp.analysis.sequences]
eval [def, in mathcomp.analysis.topology_theory.function_spaces]
even_poly [def, in mathcomp.algebra.poly]
eventually [def, in mathcomp.classical.filter]
eventually_filterType [def, in mathcomp.classical.filter]
eventually_pfilterType [def, in mathcomp.classical.filter]
ex_maxn [def, in mathcomp.boot.ssrnat]
ex_minn [def, in mathcomp.boot.ssrnat]
exp_coeff [def, in mathcomp.analysis.sequences]
exp_finIndexType [def, in mathcomp.boot.finfun]
expand [def, in mathcomp.reals.constructive_ereal]
expand_inj [def, in mathcomp.reals.constructive_ereal]
expe [def, in mathcomp.reals.constructive_ereal]
expectation.body [def, in mathcomp.analysis.probability_theory.random_variable]
expectation.unlock [def, in mathcomp.analysis.probability_theory.random_variable]
expectation_unlock_subterm [def, in mathcomp.analysis.probability_theory.random_variable]
expectation_unlockable [def, in mathcomp.analysis.probability_theory.random_variable]
expeR [def, in mathcomp.analysis.exp]
expg_invn [def, in mathcomp.solvable.cyclic]
expn [def, in mathcomp.boot.ssrnat]
expn_rec [def, in mathcomp.boot.ssrnat]
expn_snum [def, in mathcomp.reals.signed]
exponent [def, in mathcomp.solvable.abelian]
exponential_pdf [def, in mathcomp.analysis.probability_theory.exponential_distribution]
exponential_prob [def, in mathcomp.analysis.probability_theory.exponential_distribution]
expR [def, in mathcomp.analysis.sequences]
expR_inum [def, in mathcomp.analysis.exp]
expR_itv [def, in mathcomp.analysis.exp]
expR_itv_boundl [def, in mathcomp.analysis.exp]
expR_itv_boundr [def, in mathcomp.analysis.exp]
exprn_nonzero_subdef [def, in mathcomp.reals.signed]
exprn_reality_subdef [def, in mathcomp.reals.signed]
exprn_snum [def, in mathcomp.reals.signed]
exprz [def, in mathcomp.algebra.ssrint]
exprz_gte0 [def, in mathcomp.algebra.ssrint]
expv [def, in mathcomp.field.falgebra]
ext_fperm [def, in mathcomp.finmap.finperm]
ext_num_sem [def, in mathcomp.reals.constructive_ereal]
ext_widen_itv [def, in mathcomp.reals.constructive_ereal]
extendDerivation [def, in mathcomp.field.separable]
extnprod_invg [def, in mathcomp.finite_group.gproduct]
extnprod_mulg [def, in mathcomp.finite_group.gproduct]
extprod_invg [def, in mathcomp.finite_group.gproduct]
extprod_mulg [def, in mathcomp.finite_group.gproduct]
extraspecial [def, in mathcomp.solvable.maximal]
Extremal.act_morphism [def, in mathcomp.solvable.extremal]
Extremal.aut_of [def, in mathcomp.solvable.extremal]
Extremal.base_act [def, in mathcomp.solvable.extremal]
Extremal.gact [def, in mathcomp.solvable.extremal]
Extremal.gtype.body [def, in mathcomp.solvable.extremal]
Extremal.gtype.unlock [def, in mathcomp.solvable.extremal]
Extremal.gtype_unlock_subterm [def, in mathcomp.solvable.extremal]
Extremal.gtype_unlockable [def, in mathcomp.solvable.extremal]
extremal2 [def, in mathcomp.solvable.extremal]
extremal_class [def, in mathcomp.solvable.extremal]
extremal_generators [def, in mathcomp.solvable.extremal]
extremum [def, in mathcomp.boot.fintype]