| 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 | _ | (7984 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 | _ | (401 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 | _ | (5228 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 | _ | (292 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 | _ | (184 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 | _ | (1519 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 | _ | (85 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 | _ | (275 entries) |
D
d [constructor, in Coq.ZArith.Znumtheory]Dadd [lemma, in Coq.Reals.Rderiv]
Data [module, in Coq.FSets.FMapInterface]
Datatypes [library]
Dcomp [lemma, in Coq.Reals.Rderiv]
Dcompare [lemma, in Coq.NArith.BinPos]
Dcompare_inf [lemma, in Coq.ZArith.ZArith_dec]
Dconst [lemma, in Coq.Reals.Rderiv]
DecBool [library]
decidable [definition, in Coq.Logic.Decidable]
Decidable [library]
DecidableEqDep [module, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet [module, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.eq_dep_eq [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.eq_rect_eq [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.inj_pairP2 [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.inj_pair2 [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.Streicher_K [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.UIP [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.UIP_refl [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.eq_dep_eq [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.eq_rect_eq [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.inj_pairP2 [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.inj_pairT2 [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.Streicher_K [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.UIP [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.UIP_refl [lemma, in Coq.Logic.Eqdep_dec]
DecidableSet [module, in Coq.Logic.Eqdep_dec]
DecidableType [module, in Coq.Logic.Eqdep_dec]
DecidableType [module, in Coq.Logic.DecidableType]
DecidableType [library]
DecidableTypeEx [library]
decide [lemma, in Coq.Logic.Diaconescu]
decimal_exp [definition, in Coq.Reals.Rfunctions]
decomp_sum [lemma, in Coq.Reals.PartSum]
decreasing [definition, in Coq.Reals.Ranalysis1]
decreasing_cv [lemma, in Coq.Reals.SeqProp]
decreasing_growing [lemma, in Coq.Reals.SeqProp]
decreasing_ineq [lemma, in Coq.Reals.SeqProp]
decreasing_prop [lemma, in Coq.Reals.SeqProp]
dec_and [lemma, in Coq.Logic.Decidable]
dec_eq [lemma, in Coq.ZArith.Zorder]
dec_eq_nat [lemma, in Coq.Arith.Peano_dec]
dec_False [lemma, in Coq.Logic.Decidable]
dec_ge [lemma, in Coq.Arith.Compare_dec]
dec_gt [lemma, in Coq.Arith.Compare_dec]
dec_imp [lemma, in Coq.Logic.Decidable]
dec_inh_nat_subset_has_unique_least_element [lemma, in Coq.Logic.ChoiceFacts]
dec_le [lemma, in Coq.Arith.Compare_dec]
dec_lt [lemma, in Coq.Arith.Compare_dec]
dec_not [lemma, in Coq.Logic.Decidable]
dec_not_not [lemma, in Coq.Logic.Decidable]
dec_or [lemma, in Coq.Logic.Decidable]
dec_True [lemma, in Coq.Logic.Decidable]
dec_Zge [lemma, in Coq.ZArith.Zorder]
dec_Zgt [lemma, in Coq.ZArith.Zorder]
dec_Zle [lemma, in Coq.ZArith.Zorder]
dec_Zlt [lemma, in Coq.ZArith.Zorder]
dec_Zne [lemma, in Coq.ZArith.Zorder]
Definitions [library]
Definition_of_Complete [constructor, in Coq.Sets.Cpo]
Definition_of_Conditionally_complete [constructor, in Coq.Sets.Cpo]
Definition_of_covers [constructor, in Coq.Sets.Partial_Order]
Definition_of_Directed [constructor, in Coq.Sets.Cpo]
Definition_of_equivalence [constructor, in Coq.Sets.Relations_1]
definition_of_noetherian [constructor, in Coq.Sets.Relations_3]
Definition_of_order [constructor, in Coq.Sets.Relations_1]
Definition_of_PER [constructor, in Coq.Sets.Relations_1]
Definition_of_Power_set [constructor, in Coq.Sets.Powerset]
Definition_of_preorder [constructor, in Coq.Sets.Relations_1]
Defn_of_Approximant [constructor, in Coq.Sets.Infinite_sets]
deg_rad [lemma, in Coq.Reals.Rtrigo_calc]
Delta [definition, in Coq.Reals.R_sqrt]
Delta_is_pos [definition, in Coq.Reals.R_sqrt]
DependentFunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]
DependentFunctionalRelReification_on [definition, in Coq.Logic.ChoiceFacts]
dependent_description [definition, in Coq.Logic.ClassicalDescription]
dependent_unique_choice [lemma, in Coq.Logic.ClassicalDescription]
dependent_unique_choice [axiom, in Coq.Logic.ClassicalUniqueChoice]
DepOfNodep [module, in Coq.FSets.FSetBridge]
DepOfNodep.Add [definition, in Coq.FSets.FSetBridge]
DepOfNodep.add [definition, in Coq.FSets.FSetBridge]
DepOfNodep.cardinal [definition, in Coq.FSets.FSetBridge]
DepOfNodep.choose [definition, in Coq.FSets.FSetBridge]
DepOfNodep.compare [definition, in Coq.FSets.FSetBridge]
DepOfNodep.compat_P_aux [lemma, in Coq.FSets.FSetBridge]
DepOfNodep.diff [definition, in Coq.FSets.FSetBridge]
DepOfNodep.elements [definition, in Coq.FSets.FSetBridge]
DepOfNodep.elt [definition, in Coq.FSets.FSetBridge]
DepOfNodep.Empty [definition, in Coq.FSets.FSetBridge]
DepOfNodep.empty [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq [definition, in Coq.FSets.FSetBridge]
DepOfNodep.equal [definition, in Coq.FSets.FSetBridge]
DepOfNodep.Equal [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq_In [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq_refl [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq_sym [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq_trans [definition, in Coq.FSets.FSetBridge]
DepOfNodep.Exists [definition, in Coq.FSets.FSetBridge]
DepOfNodep.exists_ [definition, in Coq.FSets.FSetBridge]
DepOfNodep.fdec [definition, in Coq.FSets.FSetBridge]
DepOfNodep.filter [definition, in Coq.FSets.FSetBridge]
DepOfNodep.fold [definition, in Coq.FSets.FSetBridge]
DepOfNodep.for_all [definition, in Coq.FSets.FSetBridge]
DepOfNodep.For_all [definition, in Coq.FSets.FSetBridge]
DepOfNodep.In [definition, in Coq.FSets.FSetBridge]
DepOfNodep.inter [definition, in Coq.FSets.FSetBridge]
DepOfNodep.is_empty [definition, in Coq.FSets.FSetBridge]
DepOfNodep.lt [definition, in Coq.FSets.FSetBridge]
DepOfNodep.lt_not_eq [definition, in Coq.FSets.FSetBridge]
DepOfNodep.lt_trans [definition, in Coq.FSets.FSetBridge]
DepOfNodep.max_elt [definition, in Coq.FSets.FSetBridge]
DepOfNodep.mem [definition, in Coq.FSets.FSetBridge]
DepOfNodep.min_elt [definition, in Coq.FSets.FSetBridge]
DepOfNodep.partition [definition, in Coq.FSets.FSetBridge]
DepOfNodep.remove [definition, in Coq.FSets.FSetBridge]
DepOfNodep.singleton [definition, in Coq.FSets.FSetBridge]
DepOfNodep.subset [definition, in Coq.FSets.FSetBridge]
DepOfNodep.Subset [definition, in Coq.FSets.FSetBridge]
DepOfNodep.t [definition, in Coq.FSets.FSetBridge]
DepOfNodep.union [definition, in Coq.FSets.FSetBridge]
dep_non_dep_functional_choice [lemma, in Coq.Logic.ChoiceFacts]
dep_non_dep_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]
derivable [definition, in Coq.Reals.Ranalysis1]
derivable_comp [lemma, in Coq.Reals.Ranalysis1]
derivable_const [lemma, in Coq.Reals.Ranalysis1]
derivable_continuous [lemma, in Coq.Reals.Ranalysis1]
derivable_continuous_pt [lemma, in Coq.Reals.Ranalysis1]
derivable_cos [lemma, in Coq.Reals.Rtrigo_reg]
derivable_cosh [lemma, in Coq.Reals.Ranalysis4]
derivable_derive [lemma, in Coq.Reals.Ranalysis1]
derivable_div [lemma, in Coq.Reals.Ranalysis3]
derivable_exp [lemma, in Coq.Reals.Ranalysis4]
derivable_finite_sum [lemma, in Coq.Reals.Ranalysis4]
derivable_id [lemma, in Coq.Reals.Ranalysis1]
derivable_inv [lemma, in Coq.Reals.Ranalysis4]
derivable_minus [lemma, in Coq.Reals.Ranalysis1]
derivable_mult [lemma, in Coq.Reals.Ranalysis1]
derivable_opp [lemma, in Coq.Reals.Ranalysis1]
derivable_plus [lemma, in Coq.Reals.Ranalysis1]
derivable_pow [lemma, in Coq.Reals.Ranalysis1]
derivable_pt [definition, in Coq.Reals.Ranalysis1]
derivable_pt_abs [definition, in Coq.Reals.Ranalysis1]
derivable_pt_comp [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_const [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_cos [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_cosh [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_div [lemma, in Coq.Reals.Ranalysis3]
derivable_pt_exp [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_finite_sum [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_id [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_inv [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim [definition, in Coq.Reals.Ranalysis1]
derivable_pt_lim_comp [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_const [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_cos [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_cosh [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim_cos_0 [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_div [lemma, in Coq.Reals.Ranalysis3]
derivable_pt_lim_D_in [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_exp [lemma, in Coq.Reals.Exp_prop]
derivable_pt_lim_exp_0 [lemma, in Coq.Reals.Exp_prop]
derivable_pt_lim_finite_sum [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim_fs [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim_id [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_ln [lemma, in Coq.Reals.Rpower]
derivable_pt_lim_minus [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_mult [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_opp [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_plus [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_pow [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_power [lemma, in Coq.Reals.Rpower]
derivable_pt_lim_pow_pos [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_Rsqr [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_scal [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_sin [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_sinh [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim_sin_0 [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_sqrt [lemma, in Coq.Reals.Sqrt_reg]
derivable_pt_minus [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_mult [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_opp [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_plus [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_pow [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_Rsqr [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_scal [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_sin [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_sinh [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_sqrt [lemma, in Coq.Reals.Sqrt_reg]
derivable_Rsqr [lemma, in Coq.Reals.Ranalysis1]
derivable_scal [lemma, in Coq.Reals.Ranalysis1]
derivable_sin [lemma, in Coq.Reals.Rtrigo_reg]
derivable_sinh [lemma, in Coq.Reals.Ranalysis4]
derive [definition, in Coq.Reals.Ranalysis1]
derive_increasing_interv [lemma, in Coq.Reals.MVT]
derive_increasing_interv_ax [lemma, in Coq.Reals.MVT]
derive_increasing_interv_var [lemma, in Coq.Reals.MVT]
derive_pt [definition, in Coq.Reals.Ranalysis1]
derive_pt_comp [lemma, in Coq.Reals.Ranalysis1]
derive_pt_const [lemma, in Coq.Reals.Ranalysis1]
derive_pt_cos [lemma, in Coq.Reals.Rtrigo_reg]
derive_pt_cosh [lemma, in Coq.Reals.Ranalysis4]
derive_pt_div [lemma, in Coq.Reals.Ranalysis3]
derive_pt_D_in [lemma, in Coq.Reals.Ranalysis1]
derive_pt_eq [lemma, in Coq.Reals.Ranalysis1]
derive_pt_eq_0 [lemma, in Coq.Reals.Ranalysis1]
derive_pt_eq_1 [lemma, in Coq.Reals.Ranalysis1]
derive_pt_exp [lemma, in Coq.Reals.Ranalysis4]
derive_pt_id [lemma, in Coq.Reals.Ranalysis1]
derive_pt_inv [lemma, in Coq.Reals.Ranalysis4]
derive_pt_minus [lemma, in Coq.Reals.Ranalysis1]
derive_pt_mult [lemma, in Coq.Reals.Ranalysis1]
derive_pt_opp [lemma, in Coq.Reals.Ranalysis1]
derive_pt_plus [lemma, in Coq.Reals.Ranalysis1]
derive_pt_pow [lemma, in Coq.Reals.Ranalysis1]
derive_pt_Rsqr [lemma, in Coq.Reals.Ranalysis1]
derive_pt_scal [lemma, in Coq.Reals.Ranalysis1]
derive_pt_sin [lemma, in Coq.Reals.Rtrigo_reg]
derive_pt_sinh [lemma, in Coq.Reals.Ranalysis4]
derive_pt_sqrt [lemma, in Coq.Reals.Sqrt_reg]
deriv_constant2 [lemma, in Coq.Reals.Ranalysis1]
deriv_maximum [lemma, in Coq.Reals.Ranalysis1]
deriv_minimum [lemma, in Coq.Reals.Ranalysis1]
Desc [inductive, in Coq.Relations.Relation_Operators]
description [definition, in Coq.Logic.ClassicalDescription]
description_rel_choice_imp_funct_choice [lemma, in Coq.Logic.ChoiceFacts]
desc_end [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
desc_prefix [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
desc_tail [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
destruct_list [lemma, in Coq.Lists.List]
Dgf [definition, in Coq.Reals.Rlimit]
Diaconescu [library]
Diagram [lemma, in Coq.Relations.Newman]
Dichotomy_lb [definition, in Coq.Reals.Rsqrt_def]
Dichotomy_ub [definition, in Coq.Reals.Rsqrt_def]
dicho_comp [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb [definition, in Coq.Reals.Rsqrt_def]
dicho_lb_car [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_cv [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_dicho_up [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_growing [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_maj [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_maj_y [lemma, in Coq.Reals.Rsqrt_def]
dicho_up [definition, in Coq.Reals.Rsqrt_def]
dicho_up_car [lemma, in Coq.Reals.Rsqrt_def]
dicho_up_cv [lemma, in Coq.Reals.Rsqrt_def]
dicho_up_decreasing [lemma, in Coq.Reals.Rsqrt_def]
dicho_up_min [lemma, in Coq.Reals.Rsqrt_def]
dicho_up_min_x [lemma, in Coq.Reals.Rsqrt_def]
diff [axiom, in Coq.FSets.FSetInterface]
diff [axiom, in Coq.FSets.FSetInterface]
diff [axiom, in Coq.FSets.FSetWeakInterface]
Differential [inductive, in Coq.Reals.Ranalysis1]
Differential_D2 [inductive, in Coq.Reals.Ranalysis1]
diff_false_true [lemma, in Coq.Bool.Bool]
diff_true_false [lemma, in Coq.Bool.Bool]
diff_1 [axiom, in Coq.FSets.FSetWeakInterface]
diff_1 [axiom, in Coq.FSets.FSetInterface]
diff_2 [axiom, in Coq.FSets.FSetWeakInterface]
diff_2 [axiom, in Coq.FSets.FSetInterface]
diff_3 [axiom, in Coq.FSets.FSetWeakInterface]
diff_3 [axiom, in Coq.FSets.FSetInterface]
Directed [inductive, in Coq.Sets.Cpo]
directed_relation_of_argument_class [definition, in Coq.Setoids.Setoid]
directed_relation_of_relation_class [definition, in Coq.Setoids.Setoid]
disc [definition, in Coq.Reals.Rtopology]
DiscrAxioms [library]
discrete_nat [lemma, in Coq.Arith.Compare]
DiscrProps [library]
DiscrR [library]
disc_P1 [lemma, in Coq.Reals.Rtopology]
Disjoint [inductive, in Coq.Sets.Ensembles]
Disjoint_intro [constructor, in Coq.Sets.Ensembles]
Disjoint_Union [library]
distance_refl [lemma, in Coq.Reals.Rgeom]
distance_symm [lemma, in Coq.Reals.Rgeom]
Distributivity [lemma, in Coq.Sets.Powerset_facts]
Distributivity' [lemma, in Coq.Sets.Powerset_facts]
distr_rev [lemma, in Coq.Lists.List]
dist_aux [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
dist_Desc_concat [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
dist_euc [definition, in Coq.Reals.Rgeom]
Div [library]
diveucl [inductive, in Coq.Arith.Euclid]
divex [constructor, in Coq.Arith.Euclid]
div1 [lemma, in Coq.Arith.Div]
div2 [lemma, in Coq.Arith.Div]
div2 [definition, in Coq.Arith.Div2]
Div2 [library]
div2_double [lemma, in Coq.Arith.Div2]
div2_double [lemma, in Coq.Reals.Exp_prop]
div2_double_plus_one [lemma, in Coq.Arith.Div2]
div2_even [lemma, in Coq.Arith.Div2]
div2_not_R0 [lemma, in Coq.Reals.Exp_prop]
div2_odd [lemma, in Coq.Arith.Div2]
div2_S_double [lemma, in Coq.Reals.Exp_prop]
div_eq_inv [lemma, in Coq.Reals.Ranalysis1]
div_fct [definition, in Coq.Reals.Ranalysis1]
div_real_fct [definition, in Coq.Reals.Ranalysis1]
Dln [lemma, in Coq.Reals.Rpower]
DMerge [definition, in Coq.IntMap.Mapfold]
Dminus [lemma, in Coq.Reals.Rderiv]
Dmult [lemma, in Coq.Reals.Rderiv]
Dmult_const [lemma, in Coq.Reals.Rderiv]
domain_finite [definition, in Coq.Reals.Rtopology]
domain_P1 [lemma, in Coq.Reals.Rtopology]
Dopp [lemma, in Coq.Reals.Rderiv]
double [lemma, in Coq.Reals.RIneq]
double [definition, in Coq.Arith.Div2]
double_eq_one_discr [lemma, in Coq.NArith.BinPos]
double_eq_zero_inversion [lemma, in Coq.NArith.BinPos]
double_even [lemma, in Coq.Arith.Div2]
double_moins_un_xO_discr [lemma, in Coq.NArith.BinPos]
double_odd [lemma, in Coq.Arith.Div2]
double_plus [lemma, in Coq.Arith.Div2]
double_plus_one_eq_one_inversion [lemma, in Coq.NArith.BinPos]
double_plus_one_zero_discr [lemma, in Coq.NArith.BinPos]
double_S [lemma, in Coq.Arith.Div2]
double_var [lemma, in Coq.Reals.RIneq]
Dpower [lemma, in Coq.Reals.Rpower]
DrinkerParadox [definition, in Coq.Logic.ClassicalFacts]
Dx [lemma, in Coq.Reals.Rderiv]
Dx_pow_n [lemma, in Coq.Reals.Rderiv]
d_conc [constructor, in Coq.Relations.Relation_Operators]
D_in [definition, in Coq.Reals.Rderiv]
D_in_ext [lemma, in Coq.Reals.Rpower]
D_in_imp [lemma, in Coq.Reals.Rpower]
d_nil [constructor, in Coq.Relations.Relation_Operators]
d_one [constructor, in Coq.Relations.Relation_Operators]
D_pow_n [lemma, in Coq.Reals.Rderiv]
D_x [definition, in Coq.Reals.Rderiv]
D_x_no_cond [lemma, in Coq.Reals.Ranalysis2]
| 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 | _ | (7984 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 | _ | (401 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 | _ | (5228 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 | _ | (292 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 | _ | (184 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 | _ | (1519 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 | _ | (85 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 | _ | (275 entries) |