K (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 |
K
k1AHom [prf, in mathcomp.field.galois]k1HomE [prf, in mathcomp.field.galois]
K_dec [prf, in mathcomp.classical.internal_Eqdep_dec]
K_dec_on [prf, in mathcomp.classical.internal_Eqdep_dec]
K_dec_type [prf, in mathcomp.classical.internal_Eqdep_dec]
K_F [abbrev, in mathcomp.field.fieldext]
kadd [def, in mathcomp.analysis.kernel]
kAHomP [prf, in mathcomp.field.galois]
kAut [def, in mathcomp.field.galois]
kAut1E [prf, in mathcomp.field.galois]
kAut_eq [prf, in mathcomp.field.galois]
kAut_to_gal [prf, in mathcomp.field.galois]
kAutE [prf, in mathcomp.field.galois]
kAutf_lker0 [prf, in mathcomp.field.galois]
kAutfE [prf, in mathcomp.field.galois]
kAutS [prf, in mathcomp.field.galois]
kcomp [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL [mod, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.measurable_fun_kcomp_finite [prf, in mathcomp.analysis.kernel]
kcomp_noparam [def, in mathcomp.analysis.kernel]
kcomp_noparamE [prf, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL [mod, in mathcomp.analysis.kernel]
kdirac [def, in mathcomp.analysis.kernel]
ker [def, in mathcomp.finite_group.morphism]
ker_actperm [prf, in mathcomp.finite_group.action]
ker_autm [prf, in mathcomp.finite_group.automorphism]
ker_comp [prf, in mathcomp.finite_group.morphism]
ker_conj_aut [prf, in mathcomp.finite_group.automorphism]
ker_coset [prf, in mathcomp.finite_group.quotient]
ker_coset_prim [prf, in mathcomp.finite_group.quotient]
ker_cprod_by [def, in mathcomp.solvable.center]
ker_cprod_by_central [prf, in mathcomp.solvable.center]
ker_cprod_by_group [def, in mathcomp.solvable.center]
ker_cprod_by_is_group [prf, in mathcomp.solvable.center]
ker_cprodm [prf, in mathcomp.finite_group.gproduct]
ker_dprodm [prf, in mathcomp.finite_group.gproduct]
ker_eltm [prf, in mathcomp.solvable.cyclic]
ker_factm [prf, in mathcomp.finite_group.morphism]
ker_factm_loc [prf, in mathcomp.finite_group.morphism]
ker_group [def, in mathcomp.finite_group.morphism]
ker_idm [prf, in mathcomp.finite_group.morphism]
ker_ifactm [prf, in mathcomp.finite_group.morphism]
ker_in_cprod [prf, in mathcomp.solvable.center]
ker_injm [prf, in mathcomp.finite_group.morphism]
ker_invm [prf, in mathcomp.finite_group.morphism]
ker_norm [prf, in mathcomp.finite_group.morphism]
ker_normal [prf, in mathcomp.finite_group.morphism]
ker_normal_pre [prf, in mathcomp.finite_group.morphism]
ker_pprodm [prf, in mathcomp.finite_group.gproduct]
ker_quotm [prf, in mathcomp.finite_group.quotient]
ker_rcoset [prf, in mathcomp.finite_group.morphism]
ker_restr_perm [prf, in mathcomp.finite_group.action]
ker_restrm [prf, in mathcomp.finite_group.morphism]
ker_sdprodm [prf, in mathcomp.finite_group.gproduct]
ker_sgval [prf, in mathcomp.finite_group.morphism]
ker_sub_ahom_aspace [def, in mathcomp.field.falgebra]
ker_sub_ahom_is_aspace [prf, in mathcomp.field.falgebra]
ker_sub_pre [prf, in mathcomp.finite_group.morphism]
ker_subg [prf, in mathcomp.finite_group.morphism]
ker_trivg_morphim [prf, in mathcomp.finite_group.morphism]
ker_trivm [prf, in mathcomp.finite_group.morphism]
kercoset_rcoset [prf, in mathcomp.finite_group.quotient]
kerE [prf, in mathcomp.finite_group.morphism]
kermx [def, in mathcomp.algebra.mxalgebra]
kermx0 [prf, in mathcomp.algebra.mxalgebra]
kermx_eq0 [prf, in mathcomp.algebra.mxalgebra]
kermxpoly [def, in mathcomp.algebra.mxpoly]
kermxpoly1 [prf, in mathcomp.algebra.mxpoly]
kermxpoly_min [prf, in mathcomp.algebra.mxpoly]
kermxpoly_prod [prf, in mathcomp.algebra.mxpoly]
kermxpolyC [prf, in mathcomp.algebra.mxpoly]
kermxpolyM [prf, in mathcomp.algebra.mxpoly]
kermxpolyX [prf, in mathcomp.algebra.mxpoly]
kernel [file, in mathcomp.analysis.kernel]
Kernel [abbrev, in mathcomp.analysis.kernel]
Kernel [mod, in mathcomp.analysis.kernel]
Kernel.axioms_ [rec, in mathcomp.analysis.kernel]
Kernel.class [proj, in mathcomp.analysis.kernel]
Kernel.clone [abbrev, in mathcomp.analysis.kernel]
Kernel.copy [abbrev, in mathcomp.analysis.kernel]
Kernel.Exports [mod, in mathcomp.analysis.kernel]
Kernel.Exports.kernel [abbrev, in mathcomp.analysis.kernel]
Kernel.kernel_isKernel_mixin [proj, in mathcomp.analysis.kernel]
Kernel.on [abbrev, in mathcomp.analysis.kernel]
Kernel.on_ [abbrev, in mathcomp.analysis.kernel]
Kernel.pack_ [def, in mathcomp.analysis.kernel]
Kernel.phant_clone [def, in mathcomp.analysis.kernel]
Kernel.phant_on_ [def, in mathcomp.analysis.kernel]
Kernel.sort [proj, in mathcomp.analysis.kernel]
Kernel.type [rec, in mathcomp.analysis.kernel]
kernel_finite_transition [def, in mathcomp.analysis.kernel]
Kernel_isFinite [abbrev, in mathcomp.analysis.kernel]
Kernel_isFinite [mod, in mathcomp.analysis.kernel]
Kernel_isFinite.axioms [abbrev, in mathcomp.analysis.kernel]
Kernel_isFinite.axioms_ [rec, in mathcomp.analysis.kernel]
Kernel_isFinite.Build [abbrev, in mathcomp.analysis.kernel]
Kernel_isFinite.Exports [mod, in mathcomp.analysis.kernel]
Kernel_isFinite.measure_uub [proj, in mathcomp.analysis.kernel]
Kernel_isFinite.phant_axioms [def, in mathcomp.analysis.kernel]
Kernel_isFinite.phant_Build [def, in mathcomp.analysis.kernel]
Kernel_isProbability [abbrev, in mathcomp.analysis.kernel]
Kernel_isProbability [mod, in mathcomp.analysis.kernel]
Kernel_isProbability.axioms [abbrev, in mathcomp.analysis.kernel]
Kernel_isProbability.axioms_ [rec, in mathcomp.analysis.kernel]
Kernel_isProbability.Build [abbrev, in mathcomp.analysis.kernel]
Kernel_isProbability.Exports [mod, in mathcomp.analysis.kernel]
Kernel_isProbability.phant_axioms [def, in mathcomp.analysis.kernel]
Kernel_isProbability.phant_Build [def, in mathcomp.analysis.kernel]
Kernel_isProbability.prob_kernel [proj, in mathcomp.analysis.kernel]
Kernel_isSFinite [abbrev, in mathcomp.analysis.kernel]
Kernel_isSFinite [mod, in mathcomp.analysis.kernel]
Kernel_isSFinite.axioms [abbrev, in mathcomp.analysis.kernel]
Kernel_isSFinite.axioms_ [rec, in mathcomp.analysis.kernel]
Kernel_isSFinite.Build [abbrev, in mathcomp.analysis.kernel]
Kernel_isSFinite.Exports [mod, in mathcomp.analysis.kernel]
Kernel_isSFinite.phant_axioms [def, in mathcomp.analysis.kernel]
Kernel_isSFinite.phant_Build [def, in mathcomp.analysis.kernel]
Kernel_isSFinite.sfinite [proj, in mathcomp.analysis.kernel]
Kernel_isSFinite_subdef [mod, in mathcomp.analysis.kernel]
Kernel_isSFinite_subdef [abbrev, in mathcomp.analysis.kernel]
Kernel_isSFinite_subdef.Build [abbrev, in mathcomp.analysis.kernel]
Kernel_isSubProbability [abbrev, in mathcomp.analysis.kernel]
Kernel_isSubProbability [mod, in mathcomp.analysis.kernel]
Kernel_isSubProbability.axioms [abbrev, in mathcomp.analysis.kernel]
Kernel_isSubProbability.axioms_ [rec, in mathcomp.analysis.kernel]
Kernel_isSubProbability.Build [abbrev, in mathcomp.analysis.kernel]
Kernel_isSubProbability.Exports [mod, in mathcomp.analysis.kernel]
Kernel_isSubProbability.phant_axioms [def, in mathcomp.analysis.kernel]
Kernel_isSubProbability.phant_Build [def, in mathcomp.analysis.kernel]
Kernel_isSubProbability.sprob_kernel [proj, in mathcomp.analysis.kernel]
kernel_measurable_eq_cst [prf, in mathcomp.analysis.kernel]
kernel_measurable_fun_eq_cst [prf, in mathcomp.analysis.kernel]
kernel_measurable_neq_cst [prf, in mathcomp.analysis.kernel]
kernel_sigma_finite [def, in mathcomp.analysis.kernel]
kernel_snd [def, in mathcomp.analysis.kernel]
KernelElpiOperations [mod, in mathcomp.analysis.kernel]
kerP [prf, in mathcomp.finite_group.morphism]
keys_canonical [prf, in mathcomp.finmap.finmap]
kfcomp [def, in mathcomp.analysis.kernel]
kfcompk1 [prf, in mathcomp.analysis.kernel]
kfcompkindic [prf, in mathcomp.analysis.kernel]
kHom [def, in mathcomp.field.galois]
kHom1 [prf, in mathcomp.field.galois]
kHom_dim [prf, in mathcomp.field.galois]
kHom_eq [prf, in mathcomp.field.galois]
kHom_extends [prf, in mathcomp.field.galois]
kHom_horner [prf, in mathcomp.field.galois]
kHom_inv [prf, in mathcomp.field.galois]
kHom_is_additive [def, in mathcomp.field.galois]
kHom_is_monoid_morphism [prf, in mathcomp.field.galois]
kHom_is_multiplicative [def, in mathcomp.field.galois]
kHom_is_zmod_morphism [prf, in mathcomp.field.galois]
kHom_kAut_sub [prf, in mathcomp.field.galois]
kHom_lrmorphism [prf, in mathcomp.field.galois]
kHom_monoid_morphism [prf, in mathcomp.field.galois]
kHom_poly_id [prf, in mathcomp.field.galois]
kHom_rmorphism [def, in mathcomp.field.galois]
kHom_root [prf, in mathcomp.field.galois]
kHom_root_id [prf, in mathcomp.field.galois]
kHom_to_AEnd [prf, in mathcomp.field.galois]
kHom_to_gal [prf, in mathcomp.field.galois]
kHomExtend [def, in mathcomp.field.galois]
kHomExtend_id [prf, in mathcomp.field.galois]
kHomExtend_poly [prf, in mathcomp.field.galois]
kHomExtend_val [prf, in mathcomp.field.galois]
kHomExtendE [prf, in mathcomp.field.galois]
kHomExtendP [prf, in mathcomp.field.galois]
kHomP [prf, in mathcomp.field.galois]
kHomP_tmp [prf, in mathcomp.field.galois]
kHomS [prf, in mathcomp.field.galois]
kHomSl [prf, in mathcomp.field.galois]
kHomSr [prf, in mathcomp.field.galois]
klipschitz_locally [prf, in mathcomp.analysis.normedtype_theory.normed_module]
klipschitzW [prf, in mathcomp.analysis.normedtype_theory.normed_module]
knormalize [def, in mathcomp.analysis.kernel]
KnownSign [mod, in mathcomp.reals.signed]
KnownSign.AnySign [constr, in mathcomp.reals.signed]
KnownSign.Arbitrary [constr, in mathcomp.reals.signed]
KnownSign.EqZero [constr, in mathcomp.reals.signed]
KnownSign.MaybeZero [constr, in mathcomp.reals.signed]
KnownSign.NonNeg [constr, in mathcomp.reals.signed]
KnownSign.NonPos [constr, in mathcomp.reals.signed]
KnownSign.NonZero [constr, in mathcomp.reals.signed]
KnownSign.nullity [ind, in mathcomp.reals.signed]
KnownSign.nullity_bool [def, in mathcomp.reals.signed]
KnownSign.nz_of_bool [def, in mathcomp.reals.signed]
KnownSign.Real [constr, in mathcomp.reals.signed]
KnownSign.real [ind, in mathcomp.reals.signed]
KnownSign.reality [ind, in mathcomp.reals.signed]
KnownSign.Sign [constr, in mathcomp.reals.signed]
KnownSign.sign [ind, in mathcomp.reals.signed]
KnownSign.wider_nullity [def, in mathcomp.reals.signed]
KnownSign.wider_real [def, in mathcomp.reals.signed]
KnownSign.wider_reality [def, in mathcomp.reals.signed]
KnownSign.wider_sign [def, in mathcomp.reals.signed]
kolmogorov_space [def, in mathcomp.analysis.topology_theory.separation_axioms]
kprobability [def, in mathcomp.analysis.kernel]
kproduct [def, in mathcomp.analysis.kernel]
kproduct_snd [def, in mathcomp.analysis.kernel]
kseries [def, in mathcomp.analysis.kernel]
kzero [def, in mathcomp.analysis.kernel]
kzero_uub [prf, in mathcomp.analysis.kernel]