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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 entries)
Instance 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)

Q

Q [module, in Q]
Q [record, in Q]
Qabs [definition, in Qabs]
Qabs [library]
Qabs_triangle_reverse [lemma, in Qabs_triangle_reverse]
Qabs_pos [lemma, in Qabs_pos]
Qabs_neg [lemma, in Qabs_neg]
Qabs_nonneg [lemma, in Qabs_nonneg]
Qabs_diff_Qle_condition [lemma, in Qabs_diff_Qle_condition]
Qabs_opp [lemma, in Qabs_opp]
Qabs_case [lemma, in Qabs_case]
Qabs_Qle_condition [lemma, in Qabs_Qle_condition]
Qabs_Qminus [lemma, in Qabs_Qminus]
Qabs_triangle [lemma, in Qabs_triangle]
Qabs_Qmult [lemma, in Qabs_Qmult]
QArith [library]
QArith_base [library]
Qc [record, in Qc]
Qcanon [library]
Qccompare [definition, in Qccompare]
Qcdiv [definition, in Qcdiv]
Qcdiv_mult_l [lemma, in Qcdiv_mult_l]
Qceiling [definition, in Qceiling]
Qceiling_resp_le [lemma, in Qceiling_resp_le]
Qceiling_Z [lemma, in Qceiling_Z]
Qceiling_lt [lemma, in Qceiling_lt]
Qceq_alt [lemma, in Qceq_alt]
Qcft [definition, in Qcft]
Qcge [abbreviation, in Qcge]
Qcgt [abbreviation, in Qcgt]
Qcgt_alt [lemma, in Qcgt_alt]
Qcinv [definition, in Qcinv]
Qcinv_mult_distr [lemma, in Qcinv_mult_distr]
Qcle [definition, in Qcle]
Qcle_minus_iff [lemma, in Qcle_minus_iff]
Qcle_lt_or_eq [lemma, in Qcle_lt_or_eq]
Qcle_not_lt [lemma, in Qcle_not_lt]
Qcle_refl [lemma, in Qcle_refl]
Qcle_antisym [lemma, in Qcle_antisym]
Qcle_lt_trans [lemma, in Qcle_lt_trans]
Qcle_trans [lemma, in Qcle_trans]
Qclt [definition, in Qclt]
Qclt_le_dec [lemma, in Qclt_le_dec]
Qclt_le_weak [lemma, in Qclt_le_weak]
Qclt_alt [lemma, in Qclt_alt]
Qclt_trans [lemma, in Qclt_trans]
Qclt_not_eq [lemma, in Qclt_not_eq]
Qclt_le_trans [lemma, in Qclt_le_trans]
Qclt_not_le [lemma, in Qclt_not_le]
Qclt_minus_iff [lemma, in Qclt_minus_iff]
Qcmake [constructor, in Qcmake]
Qcminus [definition, in Qcminus]
Qcmult [definition, in Qcmult]
Qcmult_assoc [lemma, in Qcmult_assoc]
Qcmult_inv_l [lemma, in Qcmult_inv_l]
Qcmult_plus_distr_l [lemma, in Qcmult_plus_distr_l]
Qcmult_le_compat_r [lemma, in Qcmult_le_compat_r]
Qcmult_integral [lemma, in Qcmult_integral]
Qcmult_comm [lemma, in Qcmult_comm]
Qcmult_div_r [lemma, in Qcmult_div_r]
Qcmult_lt_compat_r [lemma, in Qcmult_lt_compat_r]
Qcmult_integral_l [lemma, in Qcmult_integral_l]
Qcmult_lt_0_le_reg_r [lemma, in Qcmult_lt_0_le_reg_r]
Qcmult_inv_r [lemma, in Qcmult_inv_r]
Qcmult_plus_distr_r [lemma, in Qcmult_plus_distr_r]
Qcmult_1_r [lemma, in Qcmult_1_r]
Qcmult_1_l [lemma, in Qcmult_1_l]
Qcnot_lt_le [lemma, in Qcnot_lt_le]
Qcnot_le_lt [lemma, in Qcnot_le_lt]
Qcompare [definition, in Qcompare]
Qcompare_antisym [lemma, in Qcompare_antisym]
Qcompare_spec [lemma, in Qcompare_spec]
Qcompare_comp [instance, in Qcompare_comp]
Qcopp [definition, in Qcopp]
Qcopp_involutive [lemma, in Qcopp_involutive]
Qcopp_le_compat [lemma, in Qcopp_le_compat]
Qcplus [definition, in Qcplus]
Qcplus_0_r [lemma, in Qcplus_0_r]
Qcplus_comm [lemma, in Qcplus_comm]
Qcplus_opp_r [lemma, in Qcplus_opp_r]
Qcplus_0_l [lemma, in Qcplus_0_l]
Qcplus_assoc [lemma, in Qcplus_assoc]
Qcplus_le_compat [lemma, in Qcplus_le_compat]
Qcpower [definition, in Qcpower]
Qcpower_1 [lemma, in Qcpower_1]
Qcpower_0 [lemma, in Qcpower_0]
Qcpower_pos [lemma, in Qcpower_pos]
Qcrt [definition, in Qcrt]
Qc_dec [lemma, in Qc_dec]
Qc_is_canon [lemma, in Qc_is_canon]
Qc_eq_dec [lemma, in Qc_eq_dec]
Qc_decomp [lemma, in Qc_decomp]
Qc_eq_bool [definition, in Qc_eq_bool]
Qc_eq_bool_correct [lemma, in Qc_eq_bool_correct]
QDen [abbreviation, in QDen]
Qden [projection, in Qden]
Qdiv [definition, in Qdiv]
Qdiv_comp [instance, in Qdiv_comp]
Qdiv_power [lemma, in Qdiv_power]
Qdiv_mult_l [lemma, in Qdiv_mult_l]
Qeq [definition, in Qeq]
Qeqb_comp [instance, in Qeqb_comp]
Qeq_sym [lemma, in Qeq_sym]
Qeq_dec [lemma, in Qeq_dec]
Qeq_bool_neq [lemma, in Qeq_bool_neq]
Qeq_refl [lemma, in Qeq_refl]
Qeq_bool [definition, in Qeq_bool]
Qeq_eq_bool [lemma, in Qeq_eq_bool]
Qeq_bool_eq [lemma, in Qeq_bool_eq]
Qeq_trans [lemma, in Qeq_trans]
Qeq_alt [lemma, in Qeq_alt]
Qeq_bool_iff [lemma, in Qeq_bool_iff]
Qeq_eqR [lemma, in Qeq_eqR]
Qfield [library]
Qfloor [definition, in Qfloor]
Qfloor_le [lemma, in Qfloor_le]
Qfloor_Z [lemma, in Qfloor_Z]
Qfloor_resp_le [lemma, in Qfloor_resp_le]
Qge [abbreviation, in Qge]
Qge_alt [lemma, in Qge_alt]
Qge_alt [lemma, in Qge_alt]
Qgt [abbreviation, in Qgt]
Qgt_alt [lemma, in Qgt_alt]
QHasMinMax [module, in QHasMinMax]
QHasMinMax.max [definition, in max]
QHasMinMax.max_r [definition, in max_r]
QHasMinMax.max_l [definition, in max_l]
QHasMinMax.min [definition, in min]
QHasMinMax.min_r [definition, in min_r]
QHasMinMax.min_l [definition, in min_l]
QHasMinMax.QMM [module, in QHasMinMax.QMM]
Qinv [definition, in Qinv]
Qinv_mult_distr [lemma, in Qinv_mult_distr]
Qinv_le_0_compat [lemma, in Qinv_le_0_compat]
Qinv_power_n [lemma, in Qinv_power_n]
Qinv_involutive [lemma, in Qinv_involutive]
Qinv_lt_0_compat [lemma, in Qinv_lt_0_compat]
Qinv_power [lemma, in Qinv_power]
Qinv_power_positive [lemma, in Qinv_power_positive]
Qinv_comp [instance, in Qinv_comp]
Qle [definition, in Qle]
Qleb_comp [instance, in Qleb_comp]
Qle_bool_imp_le [lemma, in Qle_bool_imp_le]
Qle_shift_div_l [lemma, in Qle_shift_div_l]
Qle_trans [lemma, in Qle_trans]
Qle_lt_or_eq [lemma, in Qle_lt_or_eq]
Qle_bool [definition, in Qle_bool]
Qle_not_lt [lemma, in Qle_not_lt]
Qle_lt_trans [lemma, in Qle_lt_trans]
Qle_minus_iff [lemma, in Qle_minus_iff]
Qle_floor_ceiling [lemma, in Qle_floor_ceiling]
Qle_shift_inv_l [lemma, in Qle_shift_inv_l]
Qle_Qabs [lemma, in Qle_Qabs]
Qle_bool_iff [lemma, in Qle_bool_iff]
Qle_shift_inv_r [lemma, in Qle_shift_inv_r]
Qle_ceiling [lemma, in Qle_ceiling]
Qle_Rle [lemma, in Qle_Rle]
Qle_antisym [lemma, in Qle_antisym]
Qle_shift_div_r [lemma, in Qle_shift_div_r]
Qle_lteq [lemma, in Qle_lteq]
Qle_alt [lemma, in Qle_alt]
Qle_alt [lemma, in Qle_alt]
Qle_comp [instance, in Qle_comp]
Qle_refl [lemma, in Qle_refl]
Qlt [definition, in Qlt]
Qlt_floor [lemma, in Qlt_floor]
Qlt_le_trans [lemma, in Qlt_le_trans]
Qlt_alt [lemma, in Qlt_alt]
Qlt_shift_div_r [lemma, in Qlt_shift_div_r]
Qlt_le_dec [lemma, in Qlt_le_dec]
Qlt_trans [lemma, in Qlt_trans]
Qlt_irrefl [lemma, in Qlt_irrefl]
Qlt_shift_div_l [lemma, in Qlt_shift_div_l]
Qlt_minus_iff [lemma, in Qlt_minus_iff]
Qlt_compat [instance, in Qlt_compat]
Qlt_Rlt [lemma, in Qlt_Rlt]
Qlt_shift_inv_l [lemma, in Qlt_shift_inv_l]
Qlt_shift_inv_r [lemma, in Qlt_shift_inv_r]
Qlt_not_le [lemma, in Qlt_not_le]
Qlt_le_weak [lemma, in Qlt_le_weak]
Qlt_not_eq [lemma, in Qlt_not_eq]
Qmake [constructor, in Qmake]
QMake [library]
Qmake_Qdiv [lemma, in Qmake_Qdiv]
Qmax [definition, in Qmax]
Qmin [definition, in Qmin]
Qminmax [library]
Qminus [definition, in Qminus]
Qminus_comp [instance, in Qminus_comp]
Qminus' [definition, in Qminus']
Qminus'_correct [lemma, in Qminus'_correct]
Qmult [definition, in Qmult]
Qmult_inv_r [lemma, in Qmult_inv_r]
Qmult_inj_r [lemma, in Qmult_inj_r]
Qmult_comp [instance, in Qmult_comp]
Qmult_lt_0_le_reg_r [lemma, in Qmult_lt_0_le_reg_r]
Qmult_power [lemma, in Qmult_power]
Qmult_le_r [lemma, in Qmult_le_r]
Qmult_power_positive [lemma, in Qmult_power_positive]
Qmult_plus_distr_l [lemma, in Qmult_plus_distr_l]
Qmult_le_compat_r [lemma, in Qmult_le_compat_r]
Qmult_lt_compat_r [lemma, in Qmult_lt_compat_r]
Qmult_le_0_compat [lemma, in Qmult_le_0_compat]
Qmult_0_l [lemma, in Qmult_0_l]
Qmult_lt_l [lemma, in Qmult_lt_l]
Qmult_plus_distr_r [lemma, in Qmult_plus_distr_r]
Qmult_assoc [lemma, in Qmult_assoc]
Qmult_1_r [lemma, in Qmult_1_r]
Qmult_lt_r [lemma, in Qmult_lt_r]
Qmult_integral [lemma, in Qmult_integral]
Qmult_0_r [lemma, in Qmult_0_r]
Qmult_div_r [lemma, in Qmult_div_r]
Qmult_comm [lemma, in Qmult_comm]
Qmult_inj_l [lemma, in Qmult_inj_l]
Qmult_integral_l [lemma, in Qmult_integral_l]
Qmult_1_l [lemma, in Qmult_1_l]
Qmult_le_l [lemma, in Qmult_le_l]
Qmult' [definition, in Qmult']
Qmult'_correct [lemma, in Qmult'_correct]
Qnot_lt_le [lemma, in Qnot_lt_le]
Qnot_eq_sym [lemma, in Qnot_eq_sym]
Qnot_le_lt [lemma, in Qnot_le_lt]
Qnum [projection, in Qnum]
Qopp [definition, in Qopp]
Qopp_involutive [lemma, in Qopp_involutive]
Qopp_plus [lemma, in Qopp_plus]
Qopp_lt_compat [lemma, in Qopp_lt_compat]
Qopp_comp [instance, in Qopp_comp]
Qopp_le_compat [lemma, in Qopp_le_compat]
Qopp_opp [lemma, in Qopp_opp]
QOrder [module, in QOrder]
QOrderedType [library]
Qplus [definition, in Qplus]
Qplus_lt_r [lemma, in Qplus_lt_r]
Qplus_comp [instance, in Qplus_comp]
Qplus_comm [lemma, in Qplus_comm]
Qplus_lt_le_compat [lemma, in Qplus_lt_le_compat]
Qplus_le_r [lemma, in Qplus_le_r]
Qplus_le_compat [lemma, in Qplus_le_compat]
Qplus_0_l [lemma, in Qplus_0_l]
Qplus_inj_l [lemma, in Qplus_inj_l]
Qplus_inj_r [lemma, in Qplus_inj_r]
Qplus_lt_l [lemma, in Qplus_lt_l]
Qplus_opp_r [lemma, in Qplus_opp_r]
Qplus_0_r [lemma, in Qplus_0_r]
Qplus_le_l [lemma, in Qplus_le_l]
Qplus_assoc [lemma, in Qplus_assoc]
Qplus' [definition, in Qplus']
Qplus'_correct [lemma, in Qplus'_correct]
Qpower [definition, in Qpower]
Qpower [library]
Qpower_minus_positive [lemma, in Qpower_minus_positive]
Qpower_0 [lemma, in Qpower_0]
Qpower_positive_0 [lemma, in Qpower_positive_0]
Qpower_comp [instance, in Qpower_comp]
Qpower_pos_positive [lemma, in Qpower_pos_positive]
Qpower_positive_comp [instance, in Qpower_positive_comp]
Qpower_mult [lemma, in Qpower_mult]
Qpower_not_0_positive [lemma, in Qpower_not_0_positive]
Qpower_positive [definition, in Qpower_positive]
Qpower_1 [lemma, in Qpower_1]
Qpower_plus [lemma, in Qpower_plus]
Qpower_opp [lemma, in Qpower_opp]
Qpower_plus' [lemma, in Qpower_plus']
Qpower_positive_1 [lemma, in Qpower_positive_1]
Qpower_decomp [lemma, in Qpower_decomp]
Qpower_plus_positive [lemma, in Qpower_plus_positive]
Qpower_theory [lemma, in Qpower_theory]
Qpower_mult_positive [lemma, in Qpower_mult_positive]
Qpower_pos [lemma, in Qpower_pos]
QProperties [module, in QProperties]
QProperties.add_opp_diag_r [lemma, in add_opp_diag_r]
QProperties.add_assoc [lemma, in add_assoc]
QProperties.add_comm [lemma, in add_comm]
QProperties.add_0_l [lemma, in add_0_l]
QProperties.add_wd [instance, in add_wd]
QProperties.compare_spec [lemma, in compare_spec]
QProperties.compare_wd [instance, in compare_wd]
QProperties.div_mul_inv [lemma, in div_mul_inv]
QProperties.div_wd [instance, in div_wd]
QProperties.eqb [definition, in eqb]
QProperties.eqb_complete [lemma, in eqb_complete]
QProperties.eqb_eq [lemma, in eqb_eq]
QProperties.eqb_correct [lemma, in eqb_correct]
QProperties.eq_bool_wd [instance, in eq_bool_wd]
QProperties.eq_equiv [instance, in eq_equiv]
QProperties.inv_wd [instance, in inv_wd]
QProperties.le_lteq [lemma, in le_lteq]
QProperties.le_wd [instance, in le_wd]
QProperties.lt_compat [definition, in lt_compat]
QProperties.lt_strorder [instance, in lt_strorder]
QProperties.lt_total [lemma, in lt_total]
QProperties.lt_wd [instance, in lt_wd]
QProperties.max_wd [instance, in max_wd]
QProperties.max_r [lemma, in max_r]
QProperties.max_l [lemma, in max_l]
QProperties.min_r [lemma, in min_r]
QProperties.min_l [lemma, in min_l]
QProperties.min_wd [instance, in min_wd]
QProperties.mul_inv_diag_l [lemma, in mul_inv_diag_l]
QProperties.mul_1_l [lemma, in mul_1_l]
QProperties.mul_add_distr_r [lemma, in mul_add_distr_r]
QProperties.mul_comm [lemma, in mul_comm]
QProperties.mul_wd [instance, in mul_wd]
QProperties.mul_assoc [lemma, in mul_assoc]
QProperties.neq_1_0 [lemma, in neq_1_0]
QProperties.opp_wd [instance, in opp_wd]
QProperties.power_wd [instance, in power_wd]
QProperties.red_wd [instance, in red_wd]
QProperties.square_wd [instance, in square_wd]
QProperties.sub_wd [instance, in sub_wd]
QProperties.sub_add_opp [lemma, in sub_add_opp]
Qreals [library]
Qred [definition, in Qred]
Qreduction [library]
Qred_compare [lemma, in Qred_compare]
Qred_complete [lemma, in Qred_complete]
Qred_identity [lemma, in Qred_identity]
Qred_identity2 [lemma, in Qred_identity2]
Qred_opp [lemma, in Qred_opp]
Qred_involutive [lemma, in Qred_involutive]
Qred_correct [lemma, in Qred_correct]
Qred_iff [lemma, in Qred_iff]
Qring [library]
Qround [library]
Qsft [definition, in Qsft]
QSig [library]
Qsqr_nonneg [lemma, in Qsqr_nonneg]
Qsrt [definition, in Qsrt]
QType [module, in QType]
QTypeExt [module, in QTypeExt]
_ ^ _ [notation, in ::x_'^'_x]
_ < _ [notation, in ::x_'<'_x]
/ _ [notation, in ::'/'_x]
_ / _ [notation, in ::x_'/'_x]
QType_Notation [module, in QType_Notation]
_ == _ [notation, in ::x_'=='_x]
- _ [notation, in ::'-'_x]
[ _ ] [notation, in ::'['_x_']']
_ - _ [notation, in ::x_'-'_x]
1 [notation, in ::'1']
_ * _ [notation, in ::x_'*'_x]
_ != _ [notation, in ::x_'!='_x]
_ <= _ [notation, in ::x_'<='_x]
_ + _ [notation, in ::x_'+'_x]
0 [notation, in ::'0']
QType' [module, in QType']
QType.add [axiom, in add]
QType.compare [axiom, in compare]
QType.div [axiom, in div]
QType.eq [definition, in eq]
QType.eq_bool [axiom, in eq_bool]
QType.inv [axiom, in inv]
QType.le [definition, in le]
QType.lt [definition, in lt]
QType.max [axiom, in max]
QType.min [axiom, in min]
QType.minus_one [axiom, in minus_one]
QType.mul [axiom, in mul]
QType.of_Q [axiom, in of_Q]
QType.one [axiom, in one]
QType.opp [axiom, in opp]
QType.power [axiom, in power]
QType.red [axiom, in red]
QType.spec_of_Q [axiom, in spec_of_Q]
QType.spec_max [axiom, in spec_max]
QType.spec_add [axiom, in spec_add]
QType.spec_mul [axiom, in spec_mul]
QType.spec_inv [axiom, in spec_inv]
QType.spec_1 [axiom, in spec_1]
QType.spec_m1 [axiom, in spec_m1]
QType.spec_compare [axiom, in spec_compare]
QType.spec_div [axiom, in spec_div]
QType.spec_eq_bool [axiom, in spec_eq_bool]
QType.spec_sub [axiom, in spec_sub]
QType.spec_power [axiom, in spec_power]
QType.spec_min [axiom, in spec_min]
QType.spec_opp [axiom, in spec_opp]
QType.spec_square [axiom, in spec_square]
QType.spec_0 [axiom, in spec_0]
QType.spec_red [axiom, in spec_red]
QType.square [axiom, in square]
QType.strong_spec_red [axiom, in strong_spec_red]
QType.sub [axiom, in sub]
QType.t [axiom, in t]
QType.to_Q [axiom, in to_Q]
QType.zero [axiom, in zero]
[ _ ] [notation, in ::'['_x_']']
quadruple [lemma, in quadruple]
quadruple_var [lemma, in quadruple_var]
quotient [lemma, in quotient]
quotient_by_2 [lemma, in quotient_by_2]
QuotRem [module, in QuotRem]
QuotRemNotation [module, in QuotRemNotation]
_ rem _ [notation, in ::x_'rem'_x]
_ ÷ _ [notation, in ::x_'÷'_x]
QuotRemSpec [module, in QuotRemSpec]
QuotRemSpec.quot_rem [axiom, in quot_rem]
QuotRemSpec.quot_wd [instance, in quot_wd]
QuotRemSpec.rem_opp_l [axiom, in rem_opp_l]
QuotRemSpec.rem_bound_pos [axiom, in rem_bound_pos]
QuotRemSpec.rem_wd [instance, in rem_wd]
QuotRemSpec.rem_opp_r [axiom, in rem_opp_r]
QuotRem' [module, in QuotRem']
QuotRem.quot [axiom, in quot]
QuotRem.rem [axiom, in rem]
Q_as_DT.eqb [definition, in eqb]
Q_as_OT.le_lteq [definition, in le_lteq]
Q_as_DT [module, in Q_as_DT]
Q_Setoid [instance, in Q_Setoid]
Q_as_OT [module, in Q_as_OT]
Q_as_OT.lt_compat [instance, in lt_compat]
Q_as_OT.lt_strorder [instance, in lt_strorder]
Q_as_DT.t [definition, in t]
Q_as_OT.le [definition, in le]
Q_as_OT.compare_spec [definition, in compare_spec]
Q_as_OT.compare [definition, in compare]
Q_as_DT.eqb_eq [definition, in eqb_eq]
Q_apart_0_1 [lemma, in Q_apart_0_1]
Q_apart_0_1 [lemma, in Q_apart_0_1]
Q_dec [lemma, in Q_dec]
Q_as_DT.eq_equiv [definition, in eq_equiv]
Q_as_OT.lt [definition, in lt]
Q_as_DT.eq [definition, in eq]
Q.plus_max_distr_l [lemma, in plus_max_distr_l]
Q.plus_max_distr_r [lemma, in plus_max_distr_r]
Q.plus_min_distr_l [lemma, in plus_min_distr_l]
Q.plus_min_distr_r [lemma, in plus_min_distr_r]
Q2Qc [definition, in Q2Qc]
Q2R [definition, in Q2R]
Q2R_inv [lemma, in Q2R_inv]
Q2R_div [lemma, in Q2R_div]
Q2R_opp [lemma, in Q2R_opp]
Q2R_mult [lemma, in Q2R_mult]
Q2R_minus [lemma, in Q2R_minus]
Q2R_plus [lemma, in Q2R_plus]



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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 entries)
Instance 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)