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 (2748 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 (464 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 (376 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 (175 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 (546 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 (261 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 (183 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 (103 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 (64 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 (111 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 (237 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 (19 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 (100 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 (109 entries)

Global Index

A

AbGroup [record, in interfaces.abstract_algebra]
abgroup_commutative [projection, in interfaces.abstract_algebra]
abgroup_group [projection, in interfaces.abstract_algebra]
abs [definition, in interfaces.canonical_names]
Abs [record, in interfaces.canonical_names]
Abs [inductive, in interfaces.canonical_names]
abs [library]
abstract_algebra [library]
abs_nonpos_plus [lemma, in theory.abs]
abs_nonneg [lemma, in theory.abs]
abs_sig [projection, in interfaces.canonical_names]
abs_sig [constructor, in interfaces.canonical_names]
abs_proper [instance, in theory.abs]
abs_nonneg_plus [lemma, in theory.abs]
abs_mult [lemma, in theory.abs]
abs_nonpos [lemma, in theory.abs]
abs_opp [lemma, in theory.abs]
abs_0 [lemma, in theory.abs]
abs_1 [lemma, in theory.abs]
additional_operations [library]
adjunction [section, in theory.categories]
adjunctions [library]
agree_on_nat [lemma, in implementations.natpair_integers]
Algebra [record, in interfaces.ua_basic]
AlgebraOps [record, in interfaces.ua_basic]
AlgebraOps [inductive, in interfaces.ua_basic]
algebras [section, in theory.ua_products]
algebras [library]
algebras.u [variable, in theory.ua_products]
algebra_projection_morphisms [lemma, in theory.ua_products]
algebra_proof [projection, in categories.algebras]
algebra_equiv [projection, in categories.algebras]
algebra_setoids [projection, in interfaces.ua_basic]
algebra_op [projection, in interfaces.ua_basic]
algebra_op [constructor, in interfaces.ua_basic]
algebra_propers [projection, in interfaces.ua_basic]
algebra_ops [projection, in categories.algebras]
algebra_carriers [projection, in categories.algebras]
all [definition, in implementations.polynomials]
alt_Build_Rationals [lemma, in theory.rationals]
alt_Build_Rationals [section, in theory.rationals]
alt_to_frac [instance, in theory.rationals]
alt_injective [lemma, in theory.jections]
another_semiring_strict [section, in orders.semirings]
another_semiring [section, in orders.semirings]
another_full_pseudo_ring_order [section, in orders.rings]
another_rationals [section, in theory.rationals]
another_category [section, in categories.empty]
another_ring_order [section, in orders.rings]
another_integers [section, in theory.rationals]
another_strict_ring_order [section, in orders.rings]
another_pseudo_ring_order [section, in orders.rings]
AntiSymmetric [record, in interfaces.canonical_names]
AntiSymmetric [inductive, in interfaces.canonical_names]
antisymmetry [projection, in interfaces.canonical_names]
antisymmetry [constructor, in interfaces.canonical_names]
Apart [record, in interfaces.canonical_names]
Apart [inductive, in interfaces.canonical_names]
apart [projection, in interfaces.canonical_names]
apart [constructor, in interfaces.canonical_names]
ApartZero [definition, in interfaces.canonical_names]
apart_iff_total_lt [projection, in interfaces.orders]
apart_proper [instance, in orders.orders]
apart_0_proper [lemma, in theory.fields]
apart_total_lt [lemma, in orders.orders]
apart_0_sig_apart_0 [instance, in theory.fields]
apart_proper [instance, in theory.strong_setoids]
apart_0_2 [instance, in orders.semirings]
apart_ne [instance, in theory.strong_setoids]
App [abbreviation, in theory.quote_monoid]
App [abbreviation, in theory.monoid_normalization]
app [definition, in implementations.ne_list]
App [constructor, in interfaces.universal_algebra]
applications [definition, in interfaces.universal_algebra]
applications_rect [lemma, in interfaces.universal_algebra]
Applied [abbreviation, in theory.monoid_normalization]
Applied [inductive, in theory.ua_packed]
AppliedOp [constructor, in theory.ua_packed]
AppliedVar [constructor, in theory.ua_packed]
apply_args [definition, in theory.ua_packed]
app_proper [instance, in implementations.cons_list]
app_assoc_inst [instance, in implementations.cons_list]
app_tree_proper [instance, in varieties.closed_terms]
app_tree_proper [instance, in varieties.open_terms]
app_tree [definition, in interfaces.universal_algebra]
app_tree [definition, in varieties.closed_terms]
app_tree [definition, in varieties.open_terms]
Arguments [inductive, in theory.ua_packed]
arrow [constructor, in categories.functors]
Arrow [record, in categories.categories]
Arrow [record, in categories.functors]
arrow [constructor, in categories.categories]
arrow [definition, in categories.varieties]
arrow [constructor, in categories.JMcat]
arrow [definition, in categories.algebras]
Arrow [projection, in interfaces.canonical_names]
Arrow [constructor, in interfaces.canonical_names]
Arrow [record, in categories.JMcat]
Arrows [record, in interfaces.canonical_names]
Arrows [inductive, in interfaces.canonical_names]
ArrowsAssociative [abbreviation, in interfaces.canonical_names]
arrows_between_isomorphic_objects [lemma, in theory.categories]
Arrows_inst [projection, in categories.categories]
Arrows_inst [projection, in categories.JMcat]
arrow_equiv [projection, in interfaces.abstract_algebra]
arrow_unique [lemma, in varieties.closed_terms]
Associative [record, in interfaces.canonical_names]
Associative [inductive, in interfaces.canonical_names]
associativity [projection, in interfaces.canonical_names]
associativity [constructor, in interfaces.canonical_names]
associativity_arrows [definition, in categories.categories]


B

back [definition, in theory.ua_congruence]
back [lemma, in theory.jections]
back_and_forth [lemma, in theory.ua_congruence]
bad [module, in interfaces.naturals]
bad.Naturals [record, in interfaces.naturals]
bad.naturals_initial [projection, in interfaces.naturals]
better_args [definition, in theory.ua_packed]
better_Applied_rect [definition, in theory.ua_packed]
between_pos [lemma, in orders.rings]
between_nonneg [lemma, in orders.rings]
BigN_Integers [module, in implementations.fast_naturals]
bigQ_div_bigQq [lemma, in implementations.fast_rationals]
bigQ_Zshiftl [instance, in implementations.fast_rationals]
BigQ_Rationals [module, in implementations.fast_rationals]
bigQ_div_bigQq_alt [lemma, in implementations.fast_rationals]
bigQ_shiftl [instance, in implementations.fast_rationals]
bigZ_pow [instance, in implementations.fast_integers]
BigZ_Integers [module, in implementations.fast_integers]
biinduction [projection, in interfaces.canonical_names]
biinduction [constructor, in interfaces.canonical_names]
biinduction [instance, in orders.integers]
Biinduction [record, in interfaces.canonical_names]
Biinduction [inductive, in interfaces.canonical_names]
biinduction [instance, in theory.naturals]
biinduction_iff [lemma, in misc.util]
Bijective [record, in interfaces.abstract_algebra]
bijective_surjective [projection, in interfaces.abstract_algebra]
bijective_injective [projection, in interfaces.abstract_algebra]
bijective_applied [lemma, in theory.jections]
binary_strong_morphism_proper [instance, in theory.strong_setoids]
bind [projection, in interfaces.monads]
bind [constructor, in interfaces.monads]
bind_proper [projection, in interfaces.monads]
bind_proper [instance, in implementations.cons_list]
bool_decide_rel_true [lemma, in misc.util]
bool_decide_rel [definition, in misc.util]
bool_decide_true [lemma, in misc.util]
bool_decide [definition, in misc.util]
bool_decide_false [lemma, in misc.util]
bool_decide_rel_false [lemma, in misc.util]
boring_eval_entailment [definition, in interfaces.universal_algebra]


C

C [constructor, in implementations.semiring_pairs]
cancellation [section, in interfaces.abstract_algebra]
cancellation [section, in theory.rings]
cancel_left [lemma, in theory.jections]
cancel_left' [lemma, in theory.jections]
canonical_names [library]
carrier [definition, in theory.ua_products]
carrier [definition, in theory.ua_subalgebra]
carrier [definition, in theory.ua_subalgebraT]
carrier [abbreviation, in theory.ua_products]
carriers [variable, in varieties.empty]
carriers [abbreviation, in varieties.setoids]
cat [instance, in categories.dual]
CatComp [record, in interfaces.canonical_names]
CatComp [inductive, in interfaces.canonical_names]
CatComp_inst [projection, in categories.categories]
CatComp_inst [projection, in categories.JMcat]
categorical [section, in theory.ua_products]
categorical.for_a_given_c [section, in theory.ua_products]
categories [library]
categories [library]
Category [record, in interfaces.abstract_algebra]
Category_inst [projection, in categories.JMcat]
Category_inst [projection, in categories.categories]
CatId [record, in interfaces.canonical_names]
CatId [inductive, in interfaces.canonical_names]
CatId_inst [projection, in categories.JMcat]
CatId_inst [projection, in categories.categories]
cat_id [projection, in interfaces.canonical_names]
cat_id [constructor, in interfaces.canonical_names]
classquote [library]
close [definition, in interfaces.universal_algebra]
ClosedSubset [record, in theory.ua_subalgebra]
ClosedSubset [record, in theory.ua_subalgebraT]
closed_terms [library]
close_op [definition, in theory.ua_subalgebraT]
close_op [definition, in theory.ua_subalgebra]
close_op_proper [definition, in theory.ua_subalgebraT]
close_op_proper [definition, in theory.ua_subalgebra]
co [instance, in theory.ua_congruence]
coerce [projection, in interfaces.canonical_names]
coerce [constructor, in interfaces.canonical_names]
Coerce [record, in interfaces.canonical_names]
Coerce [inductive, in interfaces.canonical_names]
commonoid_commutative [projection, in interfaces.abstract_algebra]
commonoid_mon [projection, in interfaces.abstract_algebra]
Commutative [record, in interfaces.canonical_names]
Commutative [inductive, in interfaces.canonical_names]
CommutativeMonoid [record, in interfaces.abstract_algebra]
commutativity [projection, in interfaces.canonical_names]
commutativity [constructor, in interfaces.canonical_names]
Comp [constructor, in theory.monoid_normalization]
comp [projection, in interfaces.canonical_names]
comp [constructor, in interfaces.canonical_names]
comp [instance, in categories.algebras]
component_equality_to_product [lemma, in theory.ua_products]
compose_lt [lemma, in orders.semirings]
compose_homomorphisms [instance, in theory.ua_homomorphisms]
compose_transformation [instance, in categories.functors]
compose_functors [section, in interfaces.functors]
compose_order_preserving_back [instance, in orders.maps]
compose_order_morphism [instance, in orders.maps]
compose_morphisms [instance, in varieties.semigroups]
compose_functors [instance, in interfaces.functors]
compose_semiring_morphisms [instance, in theory.rings]
compose_order_embedding [instance, in orders.maps]
compose_morphisms [instance, in theory.setoids]
compose_order_preserving [instance, in orders.maps]
compose_le [lemma, in orders.semirings]
compose_morphisms [instance, in varieties.monoids]
composition [section, in orders.maps]
compositions [section, in theory.jections]
comp_Fmap [instance, in interfaces.functors]
comp_proper [projection, in interfaces.abstract_algebra]
comp_assoc [projection, in interfaces.abstract_algebra]
concat [definition, in implementations.cons_list]
concat_proper [instance, in implementations.cons_list]
concat_app [lemma, in implementations.cons_list]
congruence [instance, in theory.ring_ideals]
Congruence [record, in theory.ua_congruence]
congruence_quotient [projection, in theory.ua_congruence]
congruence_proper [projection, in theory.ua_congruence]
cong_proper [instance, in theory.ring_ideals]
Conj [constructor, in interfaces.universal_algebra]
cons [constructor, in implementations.ne_list]
cons_list [library]
contents [section, in implementations.polynomials]
contents [section, in theory.int_abs]
contents [section, in theory.ua_transference]
contents [section, in theory.quote_monoid]
contents [section, in implementations.field_of_fractions]
contents [section, in theory.nat_distance]
contents [section, in categories.categories]
contents [section, in categories.product]
contents [section, in theory.dec_fields]
contents [section, in varieties.open_terms]
contents [section, in varieties.closed_terms]
contents [section, in categories.functors]
contents [section, in theory.ua_homomorphisms]
contents [section, in implementations.natpair_integers]
contents [section, in categories.dual]
contents [section, in theory.hom_functor]
contents [section, in theory.ua_congruence]
contents [section, in theory.abs]
contents [section, in theory.integers]
contents [section, in theory.monoid_normalization]
contents [section, in implementations.ne_list]
contents [section, in theory.sequences]
contents [section, in theory.naturals]
contents [section, in implementations.nonzero_field_elements]
contents [section, in categories.JMcat]
contents [section, in categories.algebras]
contents [section, in theory.monads]
contents [section, in theory.forget_variety]
contents [section, in categories.varieties]
contents [section, in theory.ua_term_monad]
contents [section, in orders.minmax]
contents [section, in categories.setoids]
contents [section, in theory.categories]
contents [section, in theory.forget_algebra]
contents [section, in theory.ua_subvariety]
contents [section, in orders.dec_fields]
contents [section, in implementations.cons_list]
contents [section, in theory.ua_mapped_operations]
contents [section, in theory.strong_setoids]
contents.ab_ba [variable, in theory.ua_transference]
contents.ab_proper [variable, in theory.ua_transference]
contents.arrow_setoid.e_trans [variable, in categories.functors]
contents.arrow_setoid [section, in categories.functors]
contents.arrow_setoid.e_sym [variable, in categories.functors]
contents.arrow_setoid.e_refl [variable, in categories.functors]
contents.associativity [section, in categories.categories]
contents.associativity.a [variable, in categories.categories]
contents.associativity.b [variable, in categories.categories]
contents.associativity.c [variable, in categories.categories]
contents.associativity.w [variable, in categories.categories]
contents.associativity.x [variable, in categories.categories]
contents.associativity.y [variable, in categories.categories]
contents.associativity.z [variable, in categories.categories]
contents.ba_proper [variable, in theory.ua_transference]
contents.ba_ab [variable, in theory.ua_transference]
contents.borrowed_from_nat [section, in theory.naturals]
contents.borrowed_from_nat.two_vars [variable, in theory.naturals]
contents.borrowed_from_nat.three_vars [variable, in theory.naturals]
contents.borrowed_from_nat.no_vars [variable, in theory.naturals]
contents.ClosedTerm [variable, in varieties.closed_terms]
contents.ClosedTerm0 [variable, in varieties.closed_terms]
contents.epA [variable, in theory.ua_transference]
contents.epB [variable, in theory.ua_transference]
contents.equality [section, in theory.ua_term_monad]
contents.et [variable, in categories.varieties]
contents.et [variable, in varieties.open_terms]
contents.et [variable, in theory.forget_variety]
contents.et [variable, in varieties.closed_terms]
contents.factors [section, in categories.product]
contents.factors.C [variable, in categories.product]
contents.factors.ith_functor [variable, in categories.product]
contents.factors.X [variable, in categories.product]
contents.for_another_ring [section, in implementations.natpair_integers]
contents.for_nice_e.eAlgebra [variable, in theory.ua_congruence]
contents.for_another_ring.preserves_1 [variable, in implementations.natpair_integers]
contents.for_nice_e [section, in theory.ua_congruence]
contents.for_nice_e.lifted_normal [variable, in theory.ua_congruence]
contents.for_another_ring.preserves_mult [variable, in implementations.natpair_integers]
contents.for_another_ring.preserves_0 [variable, in implementations.natpair_integers]
contents.for_another_object.other [variable, in varieties.closed_terms]
contents.for_another_object [section, in varieties.closed_terms]
contents.for_nice_e.lifted_e [variable, in theory.ua_congruence]
contents.for_nice_e.Q [variable, in theory.ua_congruence]
contents.for_another_ring.for_another_morphism [section, in implementations.natpair_integers]
contents.for_another_ring.preserves_plus [variable, in implementations.natpair_integers]
contents.for_nice_e.eSub [variable, in theory.ua_congruence]
contents.hint [variable, in theory.ua_congruence]
contents.hintje [variable, in theory.forget_algebra]
contents.hint' [variable, in theory.ua_congruence]
contents.homo [section, in theory.ua_homomorphisms]
contents.homo.with_f [section, in theory.ua_homomorphisms]
contents.initiality [section, in theory.categories]
contents.isomorphy [section, in theory.categories]
contents.Lookup [section, in theory.quote_monoid]
contents.map_op [section, in theory.ua_mapped_operations]
contents.more_arrows.e_trans [variable, in categories.JMcat]
contents.more_arrows.e_sym [variable, in categories.categories]
contents.more_arrows.e_sym [variable, in categories.JMcat]
contents.more_arrows [section, in categories.JMcat]
contents.more_arrows.e_trans [variable, in categories.categories]
contents.more_arrows.e_refl [variable, in categories.JMcat]
contents.more_arrows [section, in categories.categories]
contents.more_arrows.e_refl [variable, in categories.categories]
contents.obj_iso [variable, in categories.categories]
contents.product [section, in categories.setoids]
contents.products [section, in theory.categories]
contents.products.def [section, in theory.categories]
contents.product_object [variable, in categories.product]
contents.Quote [section, in theory.quote_monoid]
contents.sig [variable, in varieties.open_terms]
contents.sign [variable, in theory.ua_term_monad]
contents.sign [variable, in categories.algebras]
contents.sign [variable, in theory.forget_algebra]
contents.Sorts [variable, in theory.ua_mapped_operations]
contents.structural_eq [variable, in varieties.open_terms]
contents.structural_eq [variable, in varieties.closed_terms]
contents.TargetArrows [variable, in theory.forget_algebra]
contents.σ [variable, in theory.ua_homomorphisms]
cotransitive [projection, in interfaces.canonical_names]
cotransitive [constructor, in interfaces.canonical_names]
CoTransitive [record, in interfaces.canonical_names]
CoTransitive [inductive, in interfaces.canonical_names]
curry [definition, in theory.ua_packed]
curry_decode [definition, in theory.ua_packed]
curry_decode0 [definition, in theory.ua_packed]
CutMinus [record, in interfaces.additional_operations]
CutMinus [inductive, in interfaces.additional_operations]
CutMinusSpec [record, in interfaces.additional_operations]
cut_minus_min3 [lemma, in theory.cut_minus]
cut_minus_opp [lemma, in theory.cut_minus]
cut_minus_proper [instance, in theory.cut_minus]
cut_minus_plus_distr [lemma, in theory.cut_minus]
cut_minus_zero_plus_toggle [lemma, in theory.cut_minus]
cut_minus_plus_l_rev [lemma, in theory.cut_minus]
cut_minus_properties [section, in theory.cut_minus]
cut_minus_plus_toggle3 [lemma, in theory.cut_minus]
cut_minus_default [section, in theory.cut_minus]
cut_minus_nonneg [lemma, in theory.cut_minus]
cut_minus_le [projection, in interfaces.additional_operations]
cut_minus_plus_toggle1 [lemma, in theory.cut_minus]
cut_minus_rightabsorb [lemma, in theory.cut_minus]
cut_minus_properties.min [section, in theory.cut_minus]
cut_minus [projection, in interfaces.additional_operations]
cut_minus [constructor, in interfaces.additional_operations]
cut_minus_rightidentity [lemma, in theory.cut_minus]
cut_minus_plus_r_rev [lemma, in theory.cut_minus]
cut_minus_diag [lemma, in theory.cut_minus]
cut_minus_plus_toggle2 [lemma, in theory.cut_minus]
cut_minus_leftabsorb [lemma, in theory.cut_minus]
cut_minus_min2 [lemma, in theory.cut_minus]
cut_minus_ring_minus [lemma, in theory.cut_minus]
cut_minus_mult_distr_r [lemma, in theory.cut_minus]
cut_minus_zeros_le [lemma, in theory.cut_minus]
cut_minus_le_trans [lemma, in theory.cut_minus]
cut_minus_0 [projection, in interfaces.additional_operations]
cut_minus_min1 [lemma, in theory.cut_minus]
cut_minus_mult_distr_l [lemma, in theory.cut_minus]
cut_minus [library]


D

DecField [record, in interfaces.abstract_algebra]
decfield_ring [projection, in interfaces.abstract_algebra]
decfield_nontrivial [projection, in interfaces.abstract_algebra]
decide [projection, in interfaces.canonical_names]
decide [constructor, in interfaces.canonical_names]
decide_rel [definition, in misc.util]
Decision [record, in interfaces.canonical_names]
Decision [inductive, in interfaces.canonical_names]
DecMultInv [record, in interfaces.canonical_names]
DecMultInv [inductive, in interfaces.canonical_names]
decode [definition, in theory.ua_packed]
decode_morphism_and_ops [lemma, in varieties.groups]
decode_operations [section, in varieties.monoids]
decode_variety_and_ops [instance, in varieties.semirings]
decode_operations [section, in varieties.groups]
decode_variety_and_ops [instance, in varieties.monoids]
decode_morphism_and_ops [lemma, in varieties.rings]
decode_morphism_and_ops [lemma, in varieties.monoids]
decode_variety_and_ops [instance, in varieties.groups]
decode_morphism_and_ops [lemma, in varieties.semirings]
decode_variety_and_ops [instance, in varieties.setoids]
decode_morphism_and_ops [lemma, in varieties.semigroups]
decode_operations [section, in varieties.semigroups]
decode_variety_and_ops [instance, in varieties.rings]
decode_variety_and_ops [instance, in varieties.semigroups]
decode_operations [section, in varieties.rings]
decode0 [definition, in theory.ua_packed]
decompose_lt [lemma, in orders.semirings]
decompose_le [lemma, in orders.semirings]
DecreasingNonNegative [record, in theory.series]
DecreasingNonNegative [inductive, in theory.series]
decreasing_nonneg [projection, in theory.series]
decreasing_nonneg [constructor, in theory.series]
dec_mult_inv_ne_0_iff [lemma, in theory.dec_fields]
dec_mult_inv_ne_0 [instance, in theory.dec_fields]
dec_full_pseudo_order [instance, in orders.orders]
dec_from_lt_dec [instance, in orders.orders]
dec_mult_inv_0 [projection, in interfaces.abstract_algebra]
dec_field_to_domain_inj [instance, in theory.dec_fields]
dec_mult_inv_1 [lemma, in theory.dec_fields]
dec_lt [definition, in orders.orders]
dec_pseudo_srorder [instance, in orders.semirings]
dec_strictly_order_preserving_back_mor [instance, in orders.maps]
dec_mult_inv_swap_l [lemma, in theory.dec_fields]
dec_mult_inv_distr [lemma, in theory.dec_fields]
dec_mult_inv_correct [lemma, in theory.dec_fields]
dec_mult_inverse [projection, in interfaces.abstract_algebra]
dec_setoid [section, in theory.strong_setoids]
dec_strict_partial_order [instance, in orders.orders]
dec_mult_inv_swap_r [lemma, in theory.dec_fields]
dec_order [instance, in orders.orders]
dec_mult_inv_involutive [lemma, in theory.dec_fields]
dec_mult_inv_opp [lemma, in theory.dec_fields]
dec_pseudo_order [instance, in orders.orders]
dec_partial_order [section, in orders.orders]
dec_semiring_order [section, in orders.semirings]
dec_strong_binary_morphism [instance, in theory.strong_setoids]
dec_strictly_order_preserving_inj [instance, in orders.maps]
dec_strong_setoid [instance, in theory.strong_setoids]
dec_quotients [lemma, in theory.dec_fields]
dec_mult_inv [projection, in interfaces.canonical_names]
dec_mult_inv [constructor, in interfaces.canonical_names]
dec_mult_inv_proper [projection, in interfaces.abstract_algebra]
dec_strong_injective [instance, in theory.strong_setoids]
dec_full_pseudo_srorder [instance, in orders.semirings]
dec_mult_inv_zero [lemma, in theory.dec_fields]
dec_mult_inv_inj [instance, in theory.dec_fields]
dec_strong_morphism [instance, in theory.strong_setoids]
dec_mult_inv_to_mult_inv [lemma, in theory.dec_fields]
dec_setoid_morphisms [section, in theory.strong_setoids]
dec_fields [library]
dec_fields [library]
default_order [section, in orders.integers]
default_cut_minus [instance, in theory.cut_minus]
default_order [section, in orders.rationals]
default_shiftl_integers [section, in theory.shiftl]
default_nat_pow [instance, in theory.nat_pow]
default_shiftl_int [instance, in theory.shiftl]
default_order [section, in orders.naturals]
default_shiftl [instance, in theory.shiftl]
default_abs [instance, in theory.abs]
default_apart [instance, in theory.strong_setoids]
default_shiftl_naturals [section, in theory.shiftl]
default_apart_trivial [instance, in theory.strong_setoids]
den [projection, in implementations.field_of_fractions]
den_ne_0 [projection, in implementations.field_of_fractions]
Disj [constructor, in interfaces.universal_algebra]
Distribute [record, in interfaces.canonical_names]
distribute_l [projection, in interfaces.canonical_names]
distribute_l [constructor, in interfaces.canonical_names]
distribute_sum [lemma, in theory.sequences]
distribute_r [projection, in interfaces.canonical_names]
distribute_r [constructor, in interfaces.canonical_names]
DivEuclid [record, in interfaces.additional_operations]
DivEuclid [inductive, in interfaces.additional_operations]
div_mod [projection, in interfaces.additional_operations]
div_euclid_proper [projection, in interfaces.additional_operations]
div_euclid [projection, in interfaces.additional_operations]
div_euclid [constructor, in interfaces.additional_operations]
div_euclid_0 [projection, in interfaces.additional_operations]
DN [definition, in misc.util]
dnn_hd_nonneg [lemma, in theory.series]
dnn_Str_nth [definition, in theory.series]
dnn_Str_nth_tl [instance, in theory.series]
dnn_tl [instance, in theory.series]
dnn_Str_nth_nonneg [lemma, in theory.series]
dnn_alt [lemma, in theory.series]
DtoQ [definition, in implementations.dyadics]
DtoQ_slow_preserves_opp [lemma, in implementations.dyadics]
DtoQ_slow [definition, in implementations.dyadics]
DtoQ_slow' [abbreviation, in implementations.dyadics]
DtoQ_slow_preserves_1 [lemma, in implementations.dyadics]
DtoQ_slow' [abbreviation, in implementations.dyadics]
DtoQ_slow_correct [lemma, in implementations.dyadics]
DtoQ_slow_preserves_plus [lemma, in implementations.dyadics]
DtoQ_slow_preserves_mult [lemma, in implementations.dyadics]
DtoQ_slow_preserves_0 [lemma, in implementations.dyadics]
DtoQ_correct [lemma, in implementations.dyadics]
DtoQ' [abbreviation, in implementations.dyadics]
DtoStdQ [abbreviation, in implementations.dyadics]
dual [library]
dyadic [constructor, in implementations.dyadics]
Dyadic [record, in implementations.dyadics]
Dyadic [abbreviation, in implementations.dyadics]
dyadics [section, in implementations.dyadics]
dyadics [library]
dyadics.DtoQ [section, in implementations.dyadics]
dyadics.DtoQ_slow [section, in implementations.dyadics]
dyadics.embed_rationals [section, in implementations.dyadics]
dyadics.with_rationals [section, in implementations.dyadics]
dyadic_proper [instance, in implementations.dyadics]
dy_shiftl [instance, in implementations.dyadics]
dy_equiv [instance, in implementations.dyadics]
dy_eq_dec_aux_neg [lemma, in implementations.dyadics]
dy_mult [instance, in implementations.dyadics]
dy_inject [instance, in implementations.dyadics]
dy_opp [instance, in implementations.dyadics]
dy_pow [instance, in implementations.dyadics]
dy_pow_spec [instance, in implementations.dyadics]
dy_le_dec [instance, in implementations.dyadics]
dy_abs [instance, in implementations.dyadics]
dy_le [instance, in implementations.dyadics]
dy_1 [instance, in implementations.dyadics]
dy_eq_dec_aux [lemma, in implementations.dyadics]
dy_eq_dec [instance, in implementations.dyadics]
dy_0 [instance, in implementations.dyadics]
dy_le_dec_aux [lemma, in implementations.dyadics]
dy_plus [instance, in implementations.dyadics]
dy_lt [instance, in implementations.dyadics]


E

e [instance, in categories.categories]
e [instance, in categories.dual]
e [definition, in categories.product]
E [abbreviation, in categories.empty]
e [inductive, in varieties.closed_terms]
e [instance, in categories.JMcat]
e [instance, in categories.functors]
e [projection, in categories.setoids]
eAlgebra_eSub [lemma, in theory.ua_congruence]
ee [inductive, in varieties.open_terms]
ElimProduct [record, in theory.categories]
ElimProduct [inductive, in theory.categories]
empty [library]
empty [library]
Empty_map [definition, in categories.empty]
encode_algebra_only [lemma, in varieties.semigroups]
encode_algebra_and_ops [instance, in varieties.rings]
encode_operations [instance, in varieties.monoids]
encode_variety_and_ops [section, in varieties.monoids]
encode_morphism_only [lemma, in varieties.rings]
encode_variety_and_ops [section, in varieties.semigroups]
encode_algebra_and_ops [instance, in varieties.groups]
encode_morphism_and_ops [lemma, in varieties.groups]
encode_variety_and_ops [instance, in varieties.semigroups]
encode_algebra_only [lemma, in varieties.rings]
encode_morphism_only [lemma, in varieties.semigroups]
encode_morphism_and_ops [lemma, in varieties.rings]
encode_operations [instance, in varieties.groups]
encode_with_ops [section, in varieties.rings]
encode_variety_and_ops [section, in varieties.groups]
encode_variety_and_ops [instance, in varieties.rings]
encode_variety_and_ops [instance, in varieties.monoids]
encode_morphism_only [lemma, in varieties.monoids]
encode_algebra_only [lemma, in varieties.monoids]
encode_operations [instance, in varieties.semigroups]
encode_algebra_and_ops [instance, in varieties.monoids]
encode_morphism_and_ops [lemma, in varieties.monoids]
encode_operations [instance, in varieties.rings]
encode_morphism_only [lemma, in varieties.groups]
encode_algebra_only [lemma, in varieties.groups]
encode_algebra_and_ops [instance, in varieties.semigroups]
encode_variety_and_ops [instance, in varieties.groups]
encode_morphism_and_ops [lemma, in varieties.semigroups]
Entailment [record, in interfaces.universal_algebra]
entailment_premises [projection, in interfaces.universal_algebra]
entailment_conclusion [projection, in interfaces.universal_algebra]
entailment_as_conjunctive_statement [definition, in interfaces.universal_algebra]
entailment_as_statement [definition, in interfaces.universal_algebra]
Eq [constructor, in interfaces.universal_algebra]
EqEntailment [definition, in interfaces.universal_algebra]
equal_by_normal [lemma, in theory.quote_monoid]
equal_dec_quotients [lemma, in theory.dec_fields]
equal_quotients [lemma, in theory.fields]
equal_by_one_quotient [lemma, in theory.dec_fields]
equal_because_sole [lemma, in theory.adjunctions]
equal_by_zero_sum [lemma, in theory.rings]
EquationalTheory [record, in interfaces.universal_algebra]
Equiv [record, in interfaces.canonical_names]
Equiv [inductive, in interfaces.canonical_names]
equiv [projection, in interfaces.canonical_names]
equiv [constructor, in interfaces.canonical_names]
equivalence_proper [instance, in misc.workarounds]
equiv_default_relation [instance, in interfaces.canonical_names]
Equiv_inst [projection, in categories.JMcat]
Equiv_inst [projection, in categories.categories]
eq_le [lemma, in orders.orders]
eq_le_flip [lemma, in orders.orders]
eq_not_lt [lemma, in orders.orders]
eSub_eAlgebra [lemma, in theory.ua_congruence]
eta [projection, in categories.functors]
et_sig [projection, in interfaces.universal_algebra]
et_laws [projection, in interfaces.universal_algebra]
EuclidSpec [record, in interfaces.additional_operations]
eval [abbreviation, in theory.quote_monoid]
eval [abbreviation, in theory.monoid_normalization]
eval [definition, in interfaces.universal_algebra]
eval_proper [instance, in interfaces.universal_algebra]
eval_in_other [definition, in varieties.closed_terms]
eval_stmt_proper [instance, in interfaces.universal_algebra]
eval_is_close [lemma, in varieties.closed_terms]
eval_quote' [definition, in theory.quote_monoid]
eval_quote [projection, in theory.quote_monoid]
eval_stmt [definition, in interfaces.universal_algebra]
eval_map_var [lemma, in interfaces.universal_algebra]
eval_strong_proper [instance, in interfaces.universal_algebra]
EventuallyForAll [definition, in theory.streams]
EventuallyForAll_tl [lemma, in theory.streams]
EventuallyForAll_proper [instance, in theory.streams]
EventuallyForAll_Str_nth_tl [lemma, in theory.streams]
everyOther [definition, in theory.series]
everyOther_dnn [instance, in theory.series]
everyOther_inc [instance, in theory.series]
ex [definition, in theory.quote_monoid]
expo [projection, in implementations.dyadics]
exp_preservation [section, in theory.nat_pow]
exp_preservation [section, in theory.shiftl]
exp_preservation [section, in theory.int_pow]
Ext [constructor, in interfaces.universal_algebra]
extend [projection, in interfaces.sequences]
extend [constructor, in interfaces.sequences]
ExtendToSeq [record, in interfaces.sequences]
ExtendToSeq [inductive, in interfaces.sequences]
extend_comp [lemma, in theory.sequences]
extend_inject [lemma, in theory.sequences]
extend_morphism [projection, in interfaces.sequences]
ext_equiv_trans [instance, in theory.setoids]
ext_if [constructor, in theory.streams]
ext_equiv_sym [instance, in theory.setoids]
ext_equiv [definition, in interfaces.canonical_names]
e_mult_assoc [constructor, in varieties.groups]
e_sym [constructor, in varieties.closed_terms]
e_mult_1_l [constructor, in varieties.monoids]
e_mult_assoc [constructor, in varieties.semigroups]
e_vars [constructor, in varieties.open_terms]
e_sub [constructor, in varieties.open_terms]
e_trans [constructor, in varieties.closed_terms]
e_refl [constructor, in varieties.open_terms]
e_law [constructor, in varieties.open_terms]
e_plus_0_l [constructor, in varieties.rings]
e_law [constructor, in varieties.closed_terms]
e_sym [constructor, in varieties.open_terms]
e_plus_assoc [constructor, in varieties.rings]
e_distr_r [constructor, in varieties.semirings]
e_mult_comm [constructor, in varieties.semirings]
e_mult_1_l [constructor, in varieties.groups]
e_mult_0_l [constructor, in varieties.semirings]
e_sub [constructor, in varieties.closed_terms]
e_plus_comm [constructor, in varieties.semirings]
e_mult_1_r [constructor, in varieties.monoids]
e_mult_assoc [constructor, in varieties.semirings]
e_plus_assoc [constructor, in varieties.semirings]
e_mult_1_r [constructor, in varieties.groups]
e_mult_inv_r [constructor, in varieties.groups]
e_distr_l [constructor, in varieties.rings]
e_distr [constructor, in varieties.rings]
e_mult_assoc [constructor, in varieties.monoids]
e_mult_inv_l [constructor, in varieties.groups]
e_mult_comm [constructor, in varieties.rings]
e_mult_0_l [constructor, in varieties.rings]
e_mult_1_l [constructor, in varieties.semirings]
e_plus_0_l [constructor, in varieties.semirings]
e_trans [constructor, in varieties.open_terms]
e_plus_opp_l [constructor, in varieties.rings]
e_distr_l [constructor, in varieties.semirings]
e_mult_1_l [constructor, in varieties.rings]
e_refl [constructor, in varieties.closed_terms]
e_plus_comm [constructor, in varieties.rings]
e_mult_assoc [constructor, in varieties.rings]
e_plus_opp_r [constructor, in varieties.rings]


F

factor [definition, in categories.product]
factorials [definition, in theory.series]
factorials_help [definition, in theory.series]
fac_help [definition, in theory.series]
fastZ_shiftl [instance, in implementations.fast_integers]
fast_integers [library]
fast_rationals [library]
fast_naturals [library]
Field [record, in interfaces.abstract_algebra]
fields [library]
field_properties [section, in theory.fields]
field_plus_ext [projection, in interfaces.abstract_algebra]
field_div_0_l [lemma, in theory.fields]
field_mult_ext [projection, in interfaces.abstract_algebra]
field_strongsetoid [projection, in interfaces.abstract_algebra]
field_ring [projection, in interfaces.abstract_algebra]
field_div_diag [lemma, in theory.fields]
field_nontrivial [projection, in interfaces.abstract_algebra]
field_of_fractions [library]
finite [constructor, in interfaces.canonical_names]
first_iso [lemma, in theory.ua_congruence]
first_iso [section, in theory.ua_congruence]
flipA [instance, in categories.dual]
flip_neg_mult_l [lemma, in orders.semirings]
flip_le_dec_mult_inv_r [lemma, in orders.dec_fields]
flip_nonpos_mult_r [lemma, in orders.semirings]
flip_nonneg_opp [lemma, in orders.rings]
flip_neg_minus [lemma, in orders.rings]
flip_lt_opp [lemma, in orders.rings]
flip_le_minus_l [lemma, in orders.rings]
flip_bijection_pseudoinstance [lemma, in theory.jections]
flip_le_opp [lemma, in orders.rings]
flip_le_minus_r [lemma, in orders.rings]
flip_lt_minus_r [lemma, in orders.rings]
flip_opp_zero [lemma, in theory.rings]
flip_nonpos_minus [lemma, in orders.rings]
flip_neg_mult_r [lemma, in orders.semirings]
flip_lt_dec_mult_inv_r [lemma, in orders.dec_fields]
flip_le_dec_mult_inv [lemma, in orders.dec_fields]
flip_opp_ne_0 [lemma, in theory.rings]
flip_nonpos_mult_l [lemma, in orders.semirings]
flip_lt_minus_l [lemma, in orders.rings]
flip_lt_dec_mult_inv_l [lemma, in orders.dec_fields]
flip_pos_opp [lemma, in orders.rings]
flip_neg_opp [lemma, in orders.rings]
flip_nonpos_opp [lemma, in orders.rings]
flip_lt_dec_mult_inv [lemma, in orders.dec_fields]
flip_pos_minus [lemma, in orders.rings]
flip_nonneg_minus [lemma, in orders.rings]
flip_le_dec_mult_inv_l [lemma, in orders.dec_fields]
flip_bijection [lemma, in theory.jections]
Fmap [record, in interfaces.functors]
Fmap [inductive, in interfaces.functors]
fmap [projection, in interfaces.functors]
fmap [constructor, in interfaces.functors]
Fmap_inst [projection, in categories.categories]
Fmap_inst [projection, in categories.functors]
fmap_op [definition, in categories.dual]
fmap_alt [lemma, in theory.sequences]
Fmap_inst [projection, in categories.JMcat]
fold [definition, in interfaces.sequences]
foldr [definition, in implementations.ne_list]
foldr1 [definition, in implementations.ne_list]
fold_inject [lemma, in theory.sequences]
fold_map [lemma, in theory.sequences]
fold_mor [instance, in interfaces.sequences]
forallArgs [definition, in theory.ua_packed]
ForAllIf [inductive, in theory.streams]
ForAllIf_proper [instance, in theory.streams]
forallSplit [definition, in theory.ua_packed]
ForAll_True [lemma, in theory.streams]
ForAll_tl [lemma, in theory.streams]
ForAll_proper [instance, in theory.streams]
forget [definition, in varieties.semigroups]
forget [definition, in varieties.monoids]
forget [instance, in theory.forget_algebra]
forget [definition, in varieties.groups]
forget [definition, in theory.forget_variety]
forget_variety [library]
forget_algebra [library]
forth [definition, in theory.ua_congruence]
for_another_semiring.f_preserves_plus [variable, in implementations.peano_naturals]
for_signature.Vars [section, in interfaces.universal_algebra]
for_φAdjunction.η [variable, in theory.adjunctions]
for_φAdjunction.hint' [variable, in theory.adjunctions]
for_signature.σ [variable, in interfaces.universal_algebra]
for_φAdjunction.hint'' [variable, in theory.adjunctions]
for_φAdjunction.ε [variable, in theory.adjunctions]
for_another_semiring.f_preserves_mult [variable, in implementations.peano_naturals]
for_ηAdjunction.hint [variable, in theory.adjunctions]
for_ηεAdjunction.hint [variable, in theory.adjunctions]
for_signature [section, in interfaces.universal_algebra]
for_φAdjunction.hint''' [variable, in theory.adjunctions]
for_ηAdjunction.hint' [variable, in theory.adjunctions]
for_signature.applications_ind [section, in interfaces.universal_algebra]
for_ηεAdjunction.hint'''' [variable, in theory.adjunctions]
for_another_semiring [section, in implementations.peano_naturals]
for_φAdjunction.hint''''' [variable, in theory.adjunctions]
for_ηεAdjunction.hint' [variable, in theory.adjunctions]
for_ηAdjunction [section, in theory.adjunctions]
for_ηAdjunction.hint'' [variable, in theory.adjunctions]
for_ηεAdjunction [section, in theory.adjunctions]
for_ηεAdjunction.hint''''' [variable, in theory.adjunctions]
for_another_semiring.f_preserves_0 [variable, in implementations.peano_naturals]
for_ηεAdjunction.hint'' [variable, in theory.adjunctions]
for_φAdjunction.hint'''' [variable, in theory.adjunctions]
for_φAdjunction [section, in theory.adjunctions]
for_ηAdjunction.hint''' [variable, in theory.adjunctions]
for_signature.eval [section, in interfaces.universal_algebra]
for_ηεAdjunction.hint''' [variable, in theory.adjunctions]
for_ηεAdjunction.φ [variable, in theory.adjunctions]
for_φAdjunction.hint [variable, in theory.adjunctions]
for_ηAdjunction.φ [variable, in theory.adjunctions]
for_another_semiring.f_preserves_1 [variable, in implementations.peano_naturals]
Frac [record, in implementations.field_of_fractions]
frac [constructor, in implementations.field_of_fractions]
Frac_lift [definition, in implementations.field_of_fractions]
Frac_nonzero_num [lemma, in implementations.field_of_fractions]
Frac_dec_mult_inv [instance, in implementations.field_of_fractions]
Frac_plus [instance, in implementations.field_of_fractions]
Frac_mult [instance, in implementations.field_of_fractions]
Frac_dec [instance, in implementations.field_of_fractions]
Frac_0 [instance, in implementations.field_of_fractions]
Frac_1 [instance, in implementations.field_of_fractions]
Frac_dec_mult_num_den [lemma, in implementations.field_of_fractions]
Frac_opp [instance, in implementations.field_of_fractions]
Frac_equiv [instance, in implementations.field_of_fractions]
Frac_inject [instance, in implementations.field_of_fractions]
from_stdlib_semiring_theory [definition, in theory.rings]
from_full_pseudo_ring_order [section, in orders.rings]
from_instance [section, in varieties.semirings]
from_ring_order [lemma, in orders.rings]
from_instance [section, in varieties.setoids]
from_strict_ring_order [section, in orders.rings]
from_ua [definition, in theory.monoid_normalization]
from_stdlib_field_theory [definition, in theory.dec_fields]
from_stdlib_semiring_theory [section, in theory.rings]
from_stdlib_ring_theory [section, in theory.rings]
from_pseudo_ring_order [lemma, in orders.rings]
from_nat_stmt [lemma, in theory.naturals]
from_full_pseudo_ring_order [lemma, in orders.rings]
from_strict_ring_order [lemma, in orders.rings]
from_another_ring [section, in theory.rings]
from_pseudo_ring_order [section, in orders.rings]
from_stdlib_ring_theory [definition, in theory.rings]
from_variety [section, in varieties.setoids]
from_stdlib_field_theory [section, in theory.dec_fields]
from_ring_order [section, in orders.rings]
FullPseudoOrder [record, in interfaces.orders]
FullPseudoSemiRingOrder [record, in interfaces.orders]
full_pseudo_srorder_pso [projection, in interfaces.orders]
full_pseudo_srorder_le_iff_not_lt_flip [projection, in interfaces.orders]
full_pseudo_order [section, in orders.orders]
full_pseudo_semiring_order [section, in orders.semirings]
full_pseudo_order_preserving [lemma, in orders.maps]
full_pseudo_order_preserving_back [lemma, in orders.maps]
full_pseudo_strictly_preserving [section, in orders.maps]
full_pseudo_order_pseudo [projection, in interfaces.orders]
Functor [record, in interfaces.functors]
functors [section, in categories.dual]
functors [library]
functors [library]
functors [library]
Functor_inst [projection, in categories.JMcat]
functor_from [projection, in interfaces.functors]
Functor_inst [projection, in categories.functors]
functor_morphism [projection, in interfaces.functors]
functor_class [section, in interfaces.functors]
Functor_inst [projection, in categories.categories]
functor_to [projection, in interfaces.functors]


G

g [definition, in implementations.natpair_integers]
geneq [definition, in theory.ua_term_monad]
geneq_sym [lemma, in theory.ua_term_monad]
geneq_trans [lemma, in theory.ua_term_monad]
gen_bind [definition, in theory.ua_term_monad]
ge_1_mult_le_compat_r [lemma, in orders.semirings]
ge_1_gt_1_mult_compat [lemma, in orders.semirings]
ge_1_mult_compat [lemma, in orders.semirings]
ge_1_mult_le_compat_l [lemma, in orders.semirings]
ginv_r [projection, in interfaces.abstract_algebra]
ginv_l [projection, in interfaces.abstract_algebra]
Group [record, in interfaces.abstract_algebra]
GroupInv [record, in interfaces.canonical_names]
GroupInv [inductive, in interfaces.canonical_names]
groupmor_props [section, in theory.groups]
groups [library]
groups [library]
group_props [section, in theory.groups]
group_inv [projection, in interfaces.canonical_names]
group_inv [constructor, in interfaces.canonical_names]
group_monoid [projection, in interfaces.abstract_algebra]
gt_1_mult_lt_compat_r [lemma, in orders.semirings]
gt_1_ge_1_mult_compat [lemma, in orders.semirings]
gt_1_mult_lt_compat_l [lemma, in orders.semirings]


H

HasProducts [record, in theory.categories]
HasProducts [inductive, in theory.categories]
head [definition, in implementations.ne_list]
head_arg [definition, in theory.ua_packed]
heq [definition, in theory.ua_subvariety]
heq_eval [lemma, in theory.ua_subvariety]
heq_eval_const [lemma, in theory.ua_subvariety]
heq_proper [instance, in theory.ua_subvariety]
HeteroAssociative [record, in interfaces.canonical_names]
HeteroAssociative [inductive, in interfaces.canonical_names]
HeteroSymmetric [record, in interfaces.canonical_names]
HeteroSymmetric [inductive, in interfaces.canonical_names]
hetero_symmetric [projection, in interfaces.canonical_names]
hetero_symmetric [constructor, in interfaces.canonical_names]
homFrom [definition, in theory.hom_functor]
HomoMorphism [record, in theory.ua_homomorphisms]
HomoMorphism_Proper [lemma, in theory.ua_homomorphisms]
homo_proper [projection, in theory.ua_homomorphisms]
homo_target_algebra [projection, in theory.ua_homomorphisms]
homo_source_algebra [projection, in theory.ua_homomorphisms]
hom_functor [library]


I

Ideal [record, in theory.ring_ideals]
ideal_congruence [section, in theory.ring_ideals]
Ideal_NonEmpty [projection, in theory.ring_ideals]
Ideal_closed_plus_opp [projection, in theory.ring_ideals]
ideal_congruence.hint [variable, in theory.ring_ideals]
Ideal_closed_mult_r [projection, in theory.ring_ideals]
Ideal_closed_mult_l [projection, in theory.ring_ideals]
ideal_congruence.ideal [variable, in theory.ring_ideals]
Identity [definition, in interfaces.universal_algebra]
identity_as_eq [definition, in interfaces.universal_algebra]
identity_as_entailment [definition, in interfaces.universal_algebra]
Identity0 [definition, in interfaces.universal_algebra]
id_homomorphism [instance, in theory.ua_homomorphisms]
id_morphism [instance, in theory.setoids]
id_order_preserving [instance, in orders.maps]
id_order_morphism [instance, in orders.maps]
id_order_preserving_back [instance, in orders.maps]
id_r [projection, in interfaces.abstract_algebra]
id_functor [instance, in interfaces.functors]
id_transformation [instance, in categories.functors]
id_semiring_morphism [instance, in theory.rings]
id_morphism [instance, in varieties.monoids]
id_morphism [instance, in varieties.semigroups]
id_injective [instance, in theory.jections]
id_functor [section, in interfaces.functors]
id_l [projection, in interfaces.abstract_algebra]
id_lr_arrows [definition, in categories.categories]
id_nat_trans [definition, in theory.categories]
iffT [definition, in misc.util]
image [definition, in theory.ua_congruence]
image_proper [lemma, in theory.ua_congruence]
impl [instance, in theory.ua_subalgebraT]
impl [instance, in theory.ua_subalgebra]
Impl [constructor, in interfaces.universal_algebra]
implementation [instance, in varieties.semirings]
implementation [instance, in varieties.empty]
IncreasingNonNegative [record, in theory.series]
IncreasingNonNegative [inductive, in theory.series]
increasing_nonneg [projection, in theory.series]
increasing_nonneg [constructor, in theory.series]
induction [lemma, in orders.integers]
induction [lemma, in theory.naturals]
induction_nonneg [lemma, in orders.integers]
infinite [constructor, in interfaces.canonical_names]
initial [definition, in theory.categories]
Initial [record, in theory.categories]
Initial [inductive, in theory.categories]
InitialArrow [record, in theory.categories]
InitialArrow [inductive, in theory.categories]
initials_unique' [lemma, in theory.categories]
initials_unique [lemma, in theory.categories]
initial_maps.Int [variable, in interfaces.integers]
initial_arrow_unique [projection, in theory.categories]
initial_arrow_unique [constructor, in theory.categories]
initial_maps [section, in interfaces.naturals]
initial_arrow [projection, in theory.categories]
initial_arrow [constructor, in theory.categories]
initial_maps.A [variable, in interfaces.naturals]
initial_maps [section, in interfaces.integers]
inject [projection, in interfaces.sequences]
inject [constructor, in interfaces.sequences]
injective [projection, in interfaces.abstract_algebra]
Injective [record, in interfaces.abstract_algebra]
injective_ne_0 [instance, in theory.rings]
Injective_proper [instance, in theory.jections]
injective_mor [projection, in interfaces.abstract_algebra]
injective_preserves_0 [lemma, in theory.rings]
injective_ne_1 [lemma, in theory.rings]
injective_nats [instance, in theory.rationals]
InjectToSeq [record, in interfaces.sequences]
InjectToSeq [inductive, in interfaces.sequences]
inject_epi [lemma, in theory.sequences]
inject_nat_N [instance, in implementations.stdlib_binary_naturals]
inject_bigN_bigQ [instance, in implementations.fast_rationals]
inject_Z_bigQ [instance, in implementations.fast_rationals]
inject_fastN_fastZ [instance, in implementations.fast_integers]
inject_N_nat [instance, in implementations.stdlib_binary_naturals]
inject_bigQ_frac_bigZ [instance, in implementations.fast_rationals]
inject_nat_Z [instance, in implementations.stdlib_binary_integers]
inject_bigQ_frac_bigZ_correct [lemma, in implementations.fast_rationals]
inject_bigZ_bigQ [instance, in implementations.fast_rationals]
inject_N_Z [instance, in implementations.stdlib_binary_integers]
inject_Z_Q [instance, in implementations.stdlib_rationals]
inn_Str_nth_tl [instance, in theory.series]
inn_tl [instance, in theory.series]
inn_Str_nth [lemma, in theory.series]
IntAbs [record, in interfaces.integers]
IntAbs [inductive, in interfaces.integers]
IntAsNat [record, in interfaces.integers]
IntAsNat [inductive, in interfaces.integers]
intdom_ring [projection, in interfaces.abstract_algebra]
intdom_nontrivial_apart [instance, in theory.rings]
intdom_nontrivial [projection, in interfaces.abstract_algebra]
intdom_nozeroes [projection, in interfaces.abstract_algebra]
Integers [record, in interfaces.integers]
integers [library]
integers [library]
integers [library]
IntegersToRing [record, in interfaces.integers]
IntegersToRing [inductive, in interfaces.integers]
integers_to_integers_injective [instance, in theory.integers]
integers_order.another_ring [section, in orders.integers]
integers_order [section, in orders.integers]
integers_to_ring_mor [projection, in interfaces.integers]
integers_order.another_ring.f_preserves_nonneg [variable, in orders.integers]
integers_to_ring [projection, in interfaces.integers]
integers_to_ring [constructor, in interfaces.integers]
integers_le_plus [lemma, in orders.integers]
integers_initial [projection, in interfaces.integers]
integers_ring [projection, in interfaces.integers]
integers_to_rationals_injective [instance, in theory.rationals]
integers_order.another_ring.f_preserves_nonneg_back [variable, in orders.integers]
integer_initial [lemma, in interfaces.integers]
integer_initial_arrow [instance, in interfaces.integers]
IntegralDomain [record, in interfaces.abstract_algebra]
integral_domain_props [section, in theory.rings]
internal_simplify [definition, in theory.monoid_normalization]
intfrac_rationals [section, in implementations.intfrac_rationals]
intfrac_rationals [library]
IntPowSpec [record, in interfaces.additional_operations]
IntroProduct [record, in theory.categories]
IntroProduct [inductive, in theory.categories]
int_abs_1 [lemma, in theory.int_abs]
int_abs_proper [instance, in theory.int_abs]
int_pow_mult [lemma, in theory.int_pow]
int_pow_properties [section, in theory.int_pow]
int_abs [definition, in interfaces.integers]
int_pow_opp_alt [lemma, in theory.int_pow]
int_pow_base_1 [instance, in theory.int_pow]
int_as_nat [projection, in interfaces.integers]
int_as_nat [constructor, in interfaces.integers]
int_abs_0 [lemma, in theory.int_abs]
int_pow_S [projection, in interfaces.additional_operations]
int_le [instance, in orders.integers]
int_abs_0_alt [lemma, in theory.int_abs]
int_lt [instance, in orders.integers]
int_pow_1 [instance, in theory.int_pow]
int_pow [section, in implementations.positive_semiring_elements]
int_pow_nat_pow [lemma, in theory.int_pow]
int_pow_2 [lemma, in theory.int_pow]
int_pow_exp_lt_back [instance, in theory.int_pow]
int_abs_nat [lemma, in theory.int_abs]
int_abs_nonneg_mult [lemma, in theory.int_abs]
int_pow_inj [instance, in theory.int_pow]
int_abs_nonneg [lemma, in theory.int_abs]
int_abs_opp_nat [lemma, in theory.int_abs]
int_pow_pos [instance, in theory.int_pow]
int_pow_ne_0 [instance, in theory.int_pow]
int_pow_default [instance, in theory.int_pow]
int_pow_opp [lemma, in theory.int_pow]
int_pow_base_0 [projection, in interfaces.additional_operations]
int_pow_exp_plus [lemma, in theory.int_pow]
int_abs_uniq [lemma, in theory.int_abs]
int_pow_proper [projection, in interfaces.additional_operations]
int_pow_ge_1 [lemma, in theory.int_pow]
int_pow_mult_inv [lemma, in theory.int_pow]
int_pow_default [section, in theory.int_pow]
int_pow_exp_mult [lemma, in theory.int_pow]
int_pow_4 [lemma, in theory.int_pow]
int_pow_nonneg [instance, in theory.int_pow]
int_pow_S_nonneg [lemma, in theory.int_pow]
int_abs_opp [lemma, in theory.int_abs]
int_pow_exp_lt [instance, in theory.int_pow]
int_abs_ne_0 [lemma, in theory.int_abs]
int_abs_nonneg_plus [lemma, in theory.int_abs]
int_pow_exp_le [instance, in theory.int_pow]
int_pow_gt_1 [lemma, in theory.int_pow]
int_abs_neg_is_pos [lemma, in theory.int_abs]
int_abs_sig [projection, in interfaces.integers]
int_abs_sig [constructor, in interfaces.integers]
int_pow_exp_le_back [instance, in theory.int_pow]
int_pow_0 [projection, in interfaces.additional_operations]
int_pow_3 [lemma, in theory.int_pow]
int_abs [library]
int_pow [library]
inv [constructor, in varieties.groups]
InVariety [record, in interfaces.universal_algebra]
Inverse [record, in interfaces.canonical_names]
Inverse [inductive, in interfaces.canonical_names]
inverse [projection, in interfaces.canonical_names]
inverse [constructor, in interfaces.canonical_names]
invert_homomorphism [lemma, in theory.ua_homomorphisms]
inv_0 [lemma, in theory.groups]
inv_proper [projection, in interfaces.abstract_algebra]
inv_involutive [lemma, in theory.groups]
in_domain_equivalence [instance, in theory.ua_congruence]
in_domain [section, in theory.ua_congruence]
in_domain [definition, in theory.ua_congruence]
iso [definition, in theory.categories]
isomorphic_image_is_rationals [section, in theory.rationals]
isos_unique [definition, in theory.categories]
isoT [definition, in theory.categories]
iso_to_frac [instance, in theory.rationals]
iso_equivalence [instance, in theory.categories]
iso_setoid [instance, in theory.categories]
iso_is_rationals [lemma, in theory.rationals]
iso_arrows [definition, in theory.categories]
is_field [section, in theory.dec_fields]
is_iso [definition, in theory.categories]
is_ne_0 [definition, in theory.rings]
is_nonneg [definition, in theory.rings]
is_pos [definition, in theory.rings]
is_sole [definition, in misc.util]
ith_obj [abbreviation, in categories.product]
i_to_r [abbreviation, in orders.integers]
i_to_r [abbreviation, in orders.rationals]
i_to_r [abbreviation, in orders.rationals]


J

jections [section, in interfaces.abstract_algebra]
jections [library]
JMcat [library]
JMrelation [library]


K

kernel [definition, in theory.ring_ideals]
kernel_is_ideal [section, in theory.ring_ideals]


L

L [inductive, in implementations.ne_list]
last [definition, in implementations.ne_list]
Laws [inductive, in varieties.monoids]
laws [section, in varieties.rings]
laws [section, in varieties.groups]
Laws [definition, in varieties.setoids]
Laws [inductive, in varieties.rings]
laws [lemma, in varieties.semirings]
Laws [inductive, in varieties.groups]
Laws [inductive, in varieties.semigroups]
Laws [inductive, in varieties.semirings]
laws [section, in varieties.semigroups]
laws [section, in varieties.semirings]
laws [section, in varieties.monoids]
laws [lemma, in theory.ua_subvariety]
Laws [definition, in varieties.empty]
laws_hold [lemma, in theory.ua_products]
laws_hold [lemma, in varieties.open_terms]
laws_hold [lemma, in varieties.closed_terms]
Le [record, in interfaces.canonical_names]
Le [inductive, in interfaces.canonical_names]
le [projection, in interfaces.canonical_names]
le [constructor, in interfaces.canonical_names]
LeftAbsorb [record, in interfaces.canonical_names]
LeftAbsorb [inductive, in interfaces.canonical_names]
LeftCancellation [record, in interfaces.abstract_algebra]
LeftCancellation [inductive, in interfaces.abstract_algebra]
LeftHeteroDistribute [record, in interfaces.canonical_names]
LeftHeteroDistribute [inductive, in interfaces.canonical_names]
LeftIdentity [record, in interfaces.canonical_names]
LeftIdentity [inductive, in interfaces.canonical_names]
LeftInverse [record, in interfaces.canonical_names]
LeftInverse [inductive, in interfaces.canonical_names]
left_inverse [projection, in interfaces.canonical_names]
left_inverse [constructor, in interfaces.canonical_names]
left_identity [projection, in interfaces.canonical_names]
left_identity [constructor, in interfaces.canonical_names]
left_cancellation_ne_0 [lemma, in theory.rings]
left_absorb [projection, in interfaces.canonical_names]
left_absorb [constructor, in interfaces.canonical_names]
left_cancellation [projection, in interfaces.abstract_algebra]
left_cancellation [constructor, in interfaces.abstract_algebra]
le_iff_not_lt_flip [projection, in interfaces.orders]
le_iff_lt_plus_1 [lemma, in orders.integers]
le_0_4 [instance, in orders.semirings]
le_total [instance, in orders.orders]
le_1_2 [lemma, in orders.semirings]
le_3_4 [lemma, in orders.semirings]
le_not_lt_flip [lemma, in orders.orders]
le_2_4 [lemma, in orders.semirings]
le_2_3 [lemma, in orders.semirings]
le_0_1 [instance, in orders.semirings]
le_lt_trans [lemma, in orders.orders]
le_0_3 [instance, in orders.semirings]
le_1_4 [lemma, in orders.semirings]
le_or_lt [lemma, in orders.orders]
le_equiv_lt [lemma, in orders.orders]
le_0_2 [instance, in orders.semirings]
le_iff_lt_plus_1 [lemma, in orders.naturals]
le_1_3 [lemma, in orders.semirings]
le_flip [lemma, in orders.orders]
lifted_e_proper [instance, in theory.ua_congruence]
liftM [instance, in theory.monads]
liftM2 [definition, in theory.monads]
ListPermutation [abbreviation, in implementations.ne_list]
list_map [lemma, in implementations.ne_list]
list_eq [instance, in implementations.cons_list]
Lookup [record, in theory.quote_monoid]
lookup [projection, in theory.quote_monoid]
lookup_right [instance, in theory.quote_monoid]
lookup_left [instance, in theory.quote_monoid]
lookup_correct [projection, in theory.quote_monoid]
Lt [record, in interfaces.canonical_names]
Lt [inductive, in interfaces.canonical_names]
lt [projection, in interfaces.canonical_names]
lt [constructor, in interfaces.canonical_names]
lt_antisym [lemma, in orders.orders]
lt_2_3 [lemma, in orders.semirings]
lt_le_trans [lemma, in orders.orders]
lt_apart_flip [lemma, in orders.orders]
lt_1_4 [lemma, in orders.semirings]
lt_2_4 [lemma, in orders.semirings]
lt_iff_plus_1_le [lemma, in orders.integers]
lt_iff_plus_1_le [lemma, in orders.naturals]
lt_1_3 [lemma, in orders.semirings]
lt_0_4 [instance, in orders.semirings]
lt_0_1 [instance, in orders.semirings]
lt_3_4 [lemma, in orders.semirings]
lt_dec [definition, in orders.orders]
lt_ne_flip [lemma, in orders.orders]
lt_flip [lemma, in orders.orders]
lt_trichotomy [instance, in orders.orders]
lt_iff_le_apart [projection, in interfaces.orders]
lt_dec_slow [definition, in orders.orders]
lt_iff_le_ne [lemma, in orders.orders]
lt_1_2 [lemma, in orders.semirings]
lt_apart [lemma, in orders.orders]
lt_0_3 [instance, in orders.semirings]
lt_ne [lemma, in orders.orders]
lt_le [lemma, in orders.orders]
lt_not_le_flip [lemma, in orders.orders]
lt_0_2 [instance, in orders.semirings]


M

M [definition, in theory.ua_term_monad]
makes_products [projection, in theory.categories]
makes_products [constructor, in theory.categories]
make_tuple [projection, in theory.categories]
make_tuple [constructor, in theory.categories]
mant [projection, in implementations.dyadics]
map [definition, in implementations.ne_list]
maps [library]
map_op_proper [instance, in theory.ua_mapped_operations]
map_obj [projection, in categories.JMcat]
map_var [definition, in interfaces.universal_algebra]
map_iso [lemma, in theory.ua_mapped_operations]
map_op [definition, in theory.ua_mapped_operations]
map_obj [projection, in categories.categories]
map_obj [projection, in categories.functors]
map_setoid [definition, in theory.functors]
map_proper [instance, in theory.streams]
max [definition, in orders.minmax]
max_proper [instance, in orders.minmax]
max_ub_r [lemma, in orders.minmax]
max_diag [lemma, in orders.minmax]
max_l [lemma, in orders.minmax]
max_commutative [instance, in orders.minmax]
max_ub_l [lemma, in orders.minmax]
max_associative [instance, in orders.minmax]
max_r [lemma, in orders.minmax]
Me [instance, in theory.ua_term_monad]
measure [definition, in theory.monoid_normalization]
merge [definition, in theory.quote_monoid]
min [definition, in orders.minmax]
minmax [library]
min_associative [instance, in orders.minmax]
min_commutative [instance, in orders.minmax]
min_proper [instance, in orders.minmax]
min_lb_l [lemma, in orders.minmax]
min_r [lemma, in orders.minmax]
min_lb_r [lemma, in orders.minmax]
min_diag [lemma, in orders.minmax]
min_l [lemma, in orders.minmax]
mkIdentity0 [definition, in interfaces.universal_algebra]
ModEuclid [record, in interfaces.additional_operations]
ModEuclid [inductive, in interfaces.additional_operations]
mod_euclid_proper [projection, in interfaces.additional_operations]
mod_euclid [projection, in interfaces.additional_operations]
mod_euclid [constructor, in interfaces.additional_operations]
mod_euclid_rem [projection, in interfaces.additional_operations]
mod_euclid_0 [projection, in interfaces.additional_operations]
Monad [record, in interfaces.monads]
MonadBind [record, in interfaces.monads]
MonadBind [inductive, in interfaces.monads]
MonadReturn [record, in interfaces.monads]
MonadReturn [inductive, in interfaces.monads]
monads [library]
monads [library]
monmor_a [projection, in interfaces.abstract_algebra]
monmor_sgmor [projection, in interfaces.abstract_algebra]
monmor_b [projection, in interfaces.abstract_algebra]
mono [instance, in categories.setoids]
Mono [record, in theory.categories]
Mono [inductive, in theory.categories]
mono [instance, in categories.product]
mono [instance, in theory.forget_algebra]
mono [projection, in theory.categories]
mono [constructor, in theory.categories]
Monoid [record, in interfaces.abstract_algebra]
monoids [library]
MonoidUnit [record, in interfaces.canonical_names]
MonoidUnit [inductive, in interfaces.canonical_names]
monoid_left_id [projection, in interfaces.abstract_algebra]
monoid_semigroup [projection, in interfaces.abstract_algebra]
monoid_morphism_proper [instance, in theory.groups]
monoid_right_id [projection, in interfaces.abstract_algebra]
Monoid_Morphism [record, in interfaces.abstract_algebra]
monoid_normalization [library]
mon_runit [projection, in interfaces.monads]
mon_unit [projection, in interfaces.canonical_names]
mon_unit [constructor, in interfaces.canonical_names]
mon_lunit [projection, in interfaces.monads]
mon_assoc [projection, in interfaces.monads]
mon_setoid [projection, in interfaces.monads]
more [section, in theory.streams]
MoreArguments [constructor, in theory.ua_packed]
more_shiftl_dec_field [section, in theory.shiftl]
more_morphisms [section, in theory.strong_setoids]
morph [definition, in varieties.closed_terms]
morphisms [section, in implementations.field_of_fractions]
morphisms [section, in theory.dec_fields]
morphisms [section, in theory.fields]
morphisms [section, in theory.strong_setoids]
morphisms_involutive [lemma, in theory.rationals]
morphisms_involutive [lemma, in theory.naturals]
morphisms_involutive [lemma, in theory.integers]
morphism_order_preserving [instance, in orders.rationals]
morphism_order_preserving [instance, in orders.naturals]
morphism_proper [instance, in theory.setoids]
morphism_classes [section, in interfaces.abstract_algebra]
morphism_order_preserving [instance, in orders.integers]
morphism_composition [section, in theory.rings]
mor_from_sr_to_alg [lemma, in varieties.setoids]
mor_from_sr_to_alg [lemma, in varieties.semirings]
msig [abbreviation, in theory.monoid_normalization]
msig [abbreviation, in theory.quote_monoid]
mult [constructor, in varieties.semigroups]
mult [constructor, in varieties.semirings]
mult [constructor, in varieties.groups]
mult [constructor, in varieties.rings]
mult [constructor, in varieties.monoids]
MultInv [record, in interfaces.canonical_names]
MultInv [inductive, in interfaces.canonical_names]
mult_inv_irrelevant [lemma, in theory.fields]
mult_inv_distr [lemma, in implementations.nonzero_field_elements]
mult_0_l [instance, in theory.rings]
mult_0_r [instance, in theory.rings]
mult_inv_apart_zero [instance, in theory.fields]
mult_ne_0 [instance, in theory.rings]
mult_lt_compat [lemma, in orders.semirings]
mult_inv_proper_alt [lemma, in theory.fields]
mult_apart_zero_r [lemma, in theory.fields]
mult_le_compat [lemma, in orders.semirings]
mult_1_r [instance, in theory.rings]
mult_inv_dec_field [instance, in theory.dec_fields]
mult_Streams [definition, in theory.series]
mult_inv_distr_alt [lemma, in theory.fields]
mult_1_l [instance, in theory.rings]
mult_apart_zero_l [lemma, in theory.fields]
mult_Streams_inc [instance, in theory.series]
mult_Streams_dnn [instance, in theory.series]
mult_inverse_alt [lemma, in theory.fields]
mult_inv [projection, in interfaces.canonical_names]
mult_inv [constructor, in interfaces.canonical_names]
mult_inv_proper [projection, in interfaces.abstract_algebra]
mult_apart_zero [instance, in theory.fields]
mult_inverse [projection, in interfaces.abstract_algebra]


N

NatDistance [record, in interfaces.naturals]
NatDistance [inductive, in interfaces.naturals]
natdistancecut_minus [instance, in theory.nat_distance]
natdistance_default [instance, in theory.nat_distance]
natpair_integers [library]
NatPowSpec [record, in interfaces.additional_operations]
natural [projection, in theory.categories]
natural [constructor, in theory.categories]
Naturals [record, in interfaces.naturals]
naturals [library]
naturals [library]
naturals [library]
NaturalsToSemiRing [record, in interfaces.naturals]
NaturalsToSemiRing [inductive, in interfaces.naturals]
naturals_nonneg [lemma, in orders.naturals]
naturals_to_semiring [projection, in interfaces.naturals]
naturals_to_semiring [constructor, in interfaces.naturals]
naturals_to_integers_injective [instance, in theory.integers]
naturals_initial [projection, in interfaces.naturals]
naturals_ring [projection, in interfaces.naturals]
naturals_to_naturals_injective [instance, in theory.naturals]
naturals_order.another_ring [section, in orders.naturals]
naturals_to_semiring_mor [projection, in interfaces.naturals]
naturals_order [section, in orders.naturals]
naturals_order.another_semiring [section, in orders.naturals]
NaturalTransformation [record, in theory.categories]
NaturalTransformation [inductive, in theory.categories]
NaturalTransformation [section, in theory.categories]
NaturalTransformation_inst [projection, in categories.functors]
natural_le_plus [lemma, in orders.naturals]
natural_initial_arrow [definition, in interfaces.naturals]
natural_transformations_id_comp [section, in categories.functors]
natural_initial [lemma, in interfaces.naturals]
nat_le [instance, in implementations.peano_naturals]
nat_plus [instance, in implementations.peano_naturals]
nat_mult [instance, in implementations.peano_naturals]
nat_pow_base_0 [lemma, in theory.nat_pow]
nat_pow_3 [lemma, in theory.nat_pow]
nat_pow_properties [section, in theory.nat_pow]
nat_nontrivial_apart [instance, in theory.naturals]
nat_0 [instance, in implementations.peano_naturals]
nat_pow_exp_mult [lemma, in theory.nat_pow]
nat_pow_base_1 [instance, in theory.nat_pow]
nat_nontrivial [instance, in theory.naturals]
nat_pow_nonneg [instance, in theory.nat_pow]
nat_lt [instance, in implementations.peano_naturals]
nat_pow_default [section, in theory.nat_pow]
nat_lt [instance, in orders.naturals]
nat_cut_minus [instance, in implementations.peano_naturals]
nat_pow_exp_plus [lemma, in theory.nat_pow]
nat_pow_base_mult [lemma, in theory.nat_pow]
nat_pow_peano [instance, in theory.nat_pow]
nat_pow_S [projection, in interfaces.additional_operations]
nat_dec [instance, in implementations.peano_naturals]
nat_distance [definition, in interfaces.naturals]
nat_pow_ne_0 [instance, in theory.nat_pow]
nat_pow_2 [lemma, in theory.nat_pow]
nat_equiv [instance, in implementations.peano_naturals]
nat_distance_proper [instance, in theory.nat_distance]
nat_pow_ge_1 [lemma, in theory.nat_pow]
nat_distance_unique_respectful [lemma, in theory.nat_distance]
nat_le [instance, in orders.naturals]
nat_le_dec [instance, in implementations.peano_naturals]
nat_distance_sig [projection, in interfaces.naturals]
nat_distance_sig [constructor, in interfaces.naturals]
nat_pow_4 [lemma, in theory.nat_pow]
nat_pow_pos [instance, in theory.nat_pow]
nat_pow_apart_0 [instance, in theory.nat_pow]
nat_pow_proper [projection, in interfaces.additional_operations]
nat_pow_1 [instance, in theory.nat_pow]
nat_1 [instance, in implementations.peano_naturals]
nat_distance_unique [lemma, in theory.nat_distance]
nat_pow_0 [projection, in interfaces.additional_operations]
nat_pow [library]
nat_distance [library]
neg [projection, in implementations.semiring_pairs]
neg_dec_mult_inv_compat [lemma, in orders.dec_fields]
neg_mult [lemma, in orders.semirings]
neg_mult_decompose [lemma, in orders.semirings]
neg_plus_compat [lemma, in orders.semirings]
neg_pos_mult [lemma, in orders.semirings]
ne_list [abbreviation, in interfaces.ua_basic]
ne_0_ge_1 [lemma, in orders.naturals]
ne_total_lt [lemma, in orders.orders]
ne_apart [instance, in theory.strong_setoids]
ne_list [library]
NoMoreArguments [constructor, in theory.ua_packed]
NonEmpty [record, in misc.util]
NonEmpty [inductive, in misc.util]
NonNeg [definition, in interfaces.canonical_names]
nonneg_minus_compat_back [lemma, in orders.rings]
nonneg_integers_naturals [section, in implementations.nonneg_integers_naturals]
nonneg_mult_compat [projection, in interfaces.orders]
nonneg_semiring_elements [section, in implementations.nonneg_semiring_elements]
NonNeg_lt [instance, in implementations.nonneg_semiring_elements]
NonNeg_equiv_dec [instance, in implementations.nonneg_semiring_elements]
NonNeg_le [instance, in implementations.nonneg_semiring_elements]
NonNeg_0 [instance, in implementations.nonneg_semiring_elements]
NonNeg_mult [instance, in implementations.nonneg_semiring_elements]
nonneg_nonpos_mult [lemma, in orders.semirings]
NonNeg_plus [instance, in implementations.nonneg_semiring_elements]
NonNeg_1 [instance, in implementations.nonneg_semiring_elements]
NonNeg_inject [instance, in implementations.nonneg_semiring_elements]
NonNeg_trivial_apart [instance, in implementations.nonneg_semiring_elements]
NonNeg_le_dec [instance, in implementations.nonneg_semiring_elements]
NonNeg_apart_dec [instance, in implementations.nonneg_semiring_elements]
nonneg_dec_mult_inv_compat [instance, in orders.dec_fields]
nonneg_plus_le_compat_l [lemma, in orders.semirings]
nonneg_plus_lt_compat_l [lemma, in orders.semirings]
nonneg_minus_compat [lemma, in orders.rings]
nonneg_plus_lt_compat_r [lemma, in orders.semirings]
nonneg_mant [lemma, in implementations.dyadics]
nonneg_plus_le_compat_r [lemma, in orders.semirings]
nonneg_plus_compat [instance, in orders.semirings]
nonneg_integers_naturals [library]
nonneg_semiring_elements [library]
NonPos [definition, in interfaces.canonical_names]
nonpos_nonneg_mult [lemma, in orders.semirings]
nonpos_mult [lemma, in orders.semirings]
nonpos_plus_compat [lemma, in orders.semirings]
nonpos_dec_mult_inv_compat [lemma, in orders.dec_fields]
nonpos_mant [lemma, in implementations.dyadics]
NonZero_inject [definition, in implementations.nonzero_field_elements]
NonZero_mult [instance, in implementations.nonzero_field_elements]
NonZero_1 [instance, in implementations.nonzero_field_elements]
nonzero_field_elements [library]
non_empty [projection, in misc.util]
non_empty [constructor, in misc.util]
notations [module, in interfaces.universal_algebra]
notations [module, in implementations.ne_list]
notations.ne_list [abbreviation, in implementations.ne_list]
_ === _ [notation, in interfaces.universal_algebra]
_ -=> _ [notation, in interfaces.universal_algebra]
_ ::: _ [notation, in implementations.ne_list]
not_le_1_0 [lemma, in orders.semirings]
not_lt_le_flip [lemma, in orders.orders]
not_symmetry [lemma, in misc.util]
not_le_ne [lemma, in orders.orders]
not_le_2_0 [lemma, in orders.semirings]
not_le_not_lt [lemma, in orders.orders]
not_lt_apart_lt_flip [lemma, in orders.orders]
not_le_lt_flip [lemma, in orders.orders]
novars [definition, in theory.quote_monoid]
NoZeroDivisors [record, in interfaces.canonical_names]
NoZeroDivisors [inductive, in interfaces.canonical_names]
no_zero_divisors [projection, in interfaces.canonical_names]
no_zero_divisors [constructor, in interfaces.canonical_names]
no_vars [definition, in interfaces.universal_algebra]
Npair_to_Z [definition, in implementations.stdlib_binary_integers]
nqe [definition, in theory.ua_products]
nqe_always [lemma, in theory.ua_products]
nqe_proper [instance, in theory.ua_products]
NtoZ_uniq [lemma, in implementations.natpair_integers]
NType_Integers.inject_NType_N [instance, in implementations.NType_naturals]
NType_Integers.NType_lt [instance, in implementations.NType_naturals]
NType_Integers.NType_two_2 [lemma, in implementations.NType_naturals]
NType_Integers.NType_le [instance, in implementations.NType_naturals]
NType_Integers.NType_shiftl [instance, in implementations.NType_naturals]
NType_Integers.NType_succ_1_plus [lemma, in implementations.NType_naturals]
NType_Integers.inject_NType_Z [instance, in implementations.NType_naturals]
NType_Integers.axioms [module, in implementations.NType_naturals]
NType_Integers.NType_1 [instance, in implementations.NType_naturals]
NType_Integers [module, in implementations.NType_naturals]
NType_Integers.NType_equiv [instance, in implementations.NType_naturals]
NType_Integers.NType_plus [instance, in implementations.NType_naturals]
NType_Integers.NType_0 [instance, in implementations.NType_naturals]
NType_Integers.NType_mult [instance, in implementations.NType_naturals]
NType_Integers.inject_N_NType [instance, in implementations.NType_naturals]
NType_Integers.NType_semiring_theory [lemma, in implementations.NType_naturals]
NType_Integers.NType_pow [instance, in implementations.NType_naturals]
NType_naturals [library]
num [projection, in implementations.field_of_fractions]
nz_one_plus_zero [lemma, in theory.naturals]
n_to_sr [abbreviation, in orders.naturals]
N_0 [instance, in implementations.stdlib_binary_naturals]
N_1 [instance, in implementations.stdlib_binary_naturals]
n_to_sr [abbreviation, in orders.rationals]
n_to_sr [abbreviation, in implementations.natpair_integers]
N_mult [instance, in implementations.stdlib_binary_naturals]
n_to_sr [abbreviation, in implementations.natpair_integers]
N_le [instance, in implementations.stdlib_binary_naturals]
N_plus [instance, in implementations.stdlib_binary_naturals]
N_equiv [instance, in implementations.stdlib_binary_naturals]
N_lt [instance, in implementations.stdlib_binary_naturals]


O

obj [projection, in categories.JMcat]
obj [projection, in categories.categories]
Object [record, in categories.functors]
object [definition, in varieties.monoids]
Object [definition, in varieties.empty]
object [section, in categories.product]
object [constructor, in categories.functors]
object [definition, in varieties.setoids]
Object [definition, in varieties.semigroups]
object [definition, in varieties.rings]
object [definition, in theory.forget_algebra]
object [definition, in varieties.groups]
object [constructor, in categories.JMcat]
object [definition, in varieties.semirings]
Object [definition, in varieties.rings]
Object [record, in categories.setoids]
object [constructor, in categories.setoids]
object [constructor, in categories.varieties]
Object [record, in categories.JMcat]
Object [record, in categories.categories]
object [definition, in varieties.semigroups]
Object [record, in categories.algebras]
object [constructor, in categories.algebras]
object [definition, in varieties.empty]
object [constructor, in categories.categories]
Object [record, in categories.varieties]
Object [definition, in categories.product]
Object [definition, in varieties.monoids]
Object [definition, in varieties.groups]
Object [definition, in varieties.semirings]
obvious [projection, in misc.util]
obvious [constructor, in misc.util]
obvious [section, in misc.util]
Obvious [record, in misc.util]
Obvious [inductive, in misc.util]
obvious_sum_dst_l [instance, in misc.util]
obvious_sum_src [instance, in misc.util]
obvious_sum_dst_r [instance, in misc.util]
of_nat [definition, in implementations.nonneg_integers_naturals]
one [constructor, in varieties.semirings]
one [constructor, in implementations.ne_list]
one [constructor, in varieties.rings]
one [constructor, in varieties.monoids]
one [constructor, in varieties.groups]
one_sum [lemma, in theory.naturals]
Op [abbreviation, in theory.quote_monoid]
op [inductive, in varieties.rings]
op [inductive, in varieties.groups]
Op [abbreviation, in theory.monoid_normalization]
op [inductive, in varieties.monoids]
op [definition, in varieties.empty]
op [definition, in varieties.setoids]
op [inductive, in varieties.semigroups]
Op [constructor, in interfaces.universal_algebra]
op [inductive, in varieties.semirings]
OpenTerm [abbreviation, in varieties.open_terms]
OpenTerm0 [definition, in varieties.open_terms]
open_terms [library]
operation [projection, in interfaces.ua_basic]
operation_type [projection, in interfaces.ua_basic]
opp [constructor, in varieties.rings]
opp_0 [lemma, in theory.rings]
opp_mult_distr_l [lemma, in theory.rings]
opp_to_semiring [lemma, in orders.naturals]
opp_to_sr_le_to_sr [lemma, in orders.naturals]
opp_zero_prod_l [lemma, in theory.rings]
opp_zero_prod_r [lemma, in theory.rings]
opp_to_semiring_nonpos [lemma, in orders.naturals]
opp_swap_r [lemma, in theory.rings]
opp_involutive [lemma, in theory.rings]
opp_mult_opp [lemma, in theory.rings]
opp_distr [lemma, in theory.rings]
opp_mult [lemma, in theory.rings]
opp_swap_l [lemma, in theory.rings]
opp_mult_distr_r [lemma, in theory.rings]
ops [section, in interfaces.monads]
ops_from_alg_to_sr [section, in varieties.semirings]
OpType [abbreviation, in interfaces.universal_algebra]
OpType [abbreviation, in theory.ua_homomorphisms]
OpType [definition, in interfaces.ua_basic]
op_type_equiv [definition, in interfaces.ua_basic]
op_closed [definition, in theory.ua_subalgebra]
op_type [definition, in interfaces.ua_basic]
_ -=> _ [notation, in interfaces.universal_algebra]
op_closed_proper [instance, in theory.ua_subalgebra]
op_closed_proper [definition, in theory.ua_subalgebraT]
op_type_notations [module, in interfaces.universal_algebra]
op_closed [definition, in theory.ua_subalgebraT]
op_type [abbreviation, in theory.ua_congruence]
OrderEmbedding [record, in interfaces.orders]
OrderIsomorphism [record, in interfaces.orders]
OrderPreserving [record, in interfaces.orders]
OrderPreservingBack [record, in interfaces.orders]
orders [library]
orders [library]
order_morphism_mor [projection, in interfaces.orders]
order_preserving [section, in theory.cut_minus]
order_preserving_back_proper [instance, in orders.maps]
order_iso_surjective [projection, in interfaces.orders]
order_embedding_back [projection, in interfaces.orders]
order_preserving_back_flip_pos [lemma, in orders.maps]
order_preserving_back_pos [lemma, in orders.maps]
Order_Morphism [record, in interfaces.orders]
order_unique [section, in orders.naturals]
order_maps [section, in interfaces.orders]
order_preserving [section, in theory.abs]
order_preserving_back_morphism [projection, in interfaces.orders]
order_preserving [section, in orders.minmax]
order_morphism_proper_b [projection, in interfaces.orders]
order_preserving_back_flip [lemma, in orders.maps]
order_embedding_preserving [projection, in interfaces.orders]
order_preserving_morphism [projection, in interfaces.orders]
order_preserving_flip [lemma, in orders.maps]
order_morphism_proper [instance, in orders.maps]
order_preserving_flip_nonneg [lemma, in orders.maps]
order_preserving [projection, in interfaces.orders]
order_preserving_ops [section, in orders.maps]
order_preserving_back [projection, in interfaces.orders]
order_iso_embedding [projection, in interfaces.orders]
order_embedding_proper [instance, in orders.maps]
order_preserving_nonneg [lemma, in orders.maps]
order_preserving_proper [instance, in orders.maps]
order_morphism_proper_a [projection, in interfaces.orders]
other_results [section, in orders.naturals]
other_results [section, in orders.integers]


P

pa [instance, in categories.product]
packed [section, in theory.ua_packed]
packed.forallArgs [section, in theory.ua_packed]
pair_proper [instance, in theory.setoids]
PartialOrder [record, in interfaces.orders]
partial_order [section, in orders.orders]
pdr_equiv [instance, in misc.util]
peano_naturals [library]
Permutation [definition, in implementations.ne_list]
Permutation_ne_tl_length [lemma, in implementations.ne_list]
Pinv [lemma, in theory.ring_ideals]
plus [constructor, in varieties.semirings]
plus [constructor, in varieties.rings]
plus_0_l [instance, in theory.rings]
plus_le_lt_compat [lemma, in orders.semirings]
plus_lt_compat [lemma, in orders.semirings]
plus_le_compat [lemma, in orders.semirings]
plus_0_r [instance, in theory.rings]
plus_le_compat_l [lemma, in orders.semirings]
plus_lt_compat_l [lemma, in orders.semirings]
plus_lt_le_compat [lemma, in orders.semirings]
plus_mult_distr_l [lemma, in theory.rings]
plus_le_compat_r [lemma, in orders.semirings]
plus_opp_l [lemma, in theory.rings]
plus_opp_r [lemma, in theory.rings]
plus_lt_compat_r [lemma, in orders.semirings]
plus_mult_distr_r [lemma, in theory.rings]
PofSplit [definition, in theory.ua_packed]
pointwise_dependent_relation [definition, in misc.util]
pointwise_dependent_relation [section, in misc.util]
poly [definition, in implementations.polynomials]
polynomials [library]
poly_eq_zero [definition, in implementations.polynomials]
poly_eq [instance, in implementations.polynomials]
poly_constant [definition, in implementations.polynomials]
poly_one [instance, in implementations.polynomials]
poly_mult_cr [definition, in implementations.polynomials]
poly_zero [instance, in implementations.polynomials]
Pos [definition, in interfaces.canonical_names]
pos [projection, in implementations.semiring_pairs]
PoshSequence [record, in interfaces.sequences]
posh_free [definition, in interfaces.sequences]
posh_inject [definition, in interfaces.sequences]
posh_extend [definition, in interfaces.sequences]
posh_fmap [instance, in interfaces.sequences]
PosInf [inductive, in interfaces.canonical_names]
positives [definition, in theory.series]
positives_help [definition, in theory.series]
positive_semiring_elements [section, in implementations.positive_semiring_elements]
positive_semiring_elements.shiftl [section, in implementations.positive_semiring_elements]
positive_semiring_elements [library]
Pos_shiftl [instance, in implementations.positive_semiring_elements]
pos_mult_compat [projection, in interfaces.orders]
pos_neg_mult [lemma, in orders.semirings]
pos_plus_compat [instance, in orders.semirings]
pos_plus_lt_compat_r [lemma, in orders.semirings]
pos_plus_le_lt_compat_l [lemma, in orders.semirings]
pos_minus_compat [lemma, in orders.rings]
pos_plus_le_lt_compat_r [lemma, in orders.semirings]
pos_plus_lt_compat_l [lemma, in orders.semirings]
Pos_plus [instance, in implementations.positive_semiring_elements]
Pos_inject [instance, in implementations.positive_semiring_elements]
Pos_mult [instance, in implementations.positive_semiring_elements]
Pos_1 [instance, in implementations.positive_semiring_elements]
pos_mult_decompose [lemma, in orders.semirings]
Pos_int_pow [instance, in implementations.positive_semiring_elements]
pos_dec_mult_inv_compat [instance, in orders.dec_fields]
Pow [record, in interfaces.additional_operations]
Pow [inductive, in interfaces.additional_operations]
pow [projection, in interfaces.additional_operations]
pow [constructor, in interfaces.additional_operations]
powers [definition, in theory.series]
powers_help [definition, in theory.series]
powers_help_proper [instance, in theory.series]
powers_proper [instance, in theory.series]
po_proper [projection, in interfaces.orders]
po_preorder [projection, in interfaces.orders]
po_setoid [projection, in interfaces.orders]
po_antisym [projection, in interfaces.orders]
Pplus [lemma, in theory.ring_ideals]
practical [section, in interfaces.sequences]
prep_proper [instance, in varieties.closed_terms]
preservation [lemma, in theory.ua_products]
preservation [section, in theory.series]
preservation [section, in theory.shiftl]
preservation [section, in theory.int_pow]
Preservation [definition, in theory.ua_homomorphisms]
preservation [section, in theory.nat_pow]
Preservation_proper' [lemma, in theory.ua_homomorphisms]
Preservation_proper'' [instance, in theory.ua_homomorphisms]
Preservation_proper [instance, in theory.ua_homomorphisms]
preserves [projection, in theory.ua_homomorphisms]
preserves_cut_minus [lemma, in theory.cut_minus]
preserves_lt_1 [lemma, in orders.semirings]
preserves_nat_pow_exp [lemma, in theory.nat_pow]
preserves_2 [lemma, in theory.rings]
preserves_powers_help [lemma, in theory.series]
preserves_mult_inv [lemma, in theory.fields]
preserves_comp [projection, in interfaces.functors]
preserves_inv [lemma, in theory.groups]
preserves_mon_unit [projection, in interfaces.abstract_algebra]
preserves_le_1 [lemma, in orders.semirings]
preserves_opp [lemma, in theory.rings]
preserves_0 [lemma, in theory.rings]
preserves_int_pow_exp [lemma, in theory.int_pow]
preserves_4 [lemma, in theory.rings]
preserves_max [lemma, in orders.minmax]
preserves_shiftl_exp [lemma, in theory.shiftl]
preserves_minus [lemma, in theory.rings]
preserves_nonpos [lemma, in orders.semirings]
preserves_abs [lemma, in theory.abs]
preserves_ge_opp1 [lemma, in orders.rings]
preserves_int_pow [lemma, in theory.int_pow]
preserves_ge_1 [lemma, in orders.semirings]
preserves_dec_mult_inv [lemma, in theory.dec_fields]
preserves_mult [lemma, in theory.rings]
preserves_positives [lemma, in theory.series]
preserves_plus [lemma, in theory.rings]
preserves_pos [instance, in orders.semirings]
preserves_factorials [lemma, in theory.series]
preserves_powers [lemma, in theory.series]
preserves_1 [lemma, in theory.rings]
preserves_sg_op [projection, in interfaces.abstract_algebra]
preserves_id [projection, in interfaces.functors]
preserves_nonneg [instance, in orders.semirings]
preserves_nat_pow [lemma, in theory.nat_pow]
preserves_min [lemma, in orders.minmax]
preserves_gt_1 [lemma, in orders.semirings]
preserves_neg [lemma, in orders.semirings]
preserves_shiftl [lemma, in theory.shiftl]
preserves_3 [lemma, in theory.rings]
preserves_le_opp1 [lemma, in orders.rings]
preserving_preserves_nonneg [lemma, in orders.semirings]
preserving_back_preserves_nonneg [lemma, in orders.rings]
Producer [record, in theory.categories]
Producer [inductive, in theory.categories]
product [definition, in theory.sequences]
product [section, in theory.setoids]
product [projection, in theory.categories]
product [constructor, in theory.categories]
Product [record, in theory.categories]
Product [inductive, in theory.categories]
product [library]
products_unique [lemma, in theory.categories]
product_e [instance, in theory.ua_products]
product_algebra [instance, in theory.ua_products]
product_equiv [instance, in theory.setoids]
product_ops [instance, in theory.ua_products]
product_variety [instance, in theory.ua_products]
product_factors [projection, in theory.categories]
product_factors [constructor, in theory.categories]
product.product [variable, in theory.setoids]
prod_equiv [definition, in theory.setoids]
proj [definition, in theory.ua_subalgebra]
project [definition, in categories.product]
projected_strict_order [lemma, in orders.maps]
projected_pseudo_order [lemma, in orders.maps]
projected_full_pseudo_ring_order [lemma, in orders.rings]
projected_full_pseudo_order [lemma, in orders.maps]
projected_setoid [lemma, in theory.setoids]
projected_strong_setoid [lemma, in theory.strong_setoids]
projected_ring_order [lemma, in orders.rings]
projected_strict_ring_order [lemma, in orders.rings]
projected_srorder [lemma, in orders.semirings]
projected_ring [lemma, in theory.rings]
projected_partial_order [lemma, in orders.maps]
projected_total_order [lemma, in orders.maps]
projected_strict_setoid_order [lemma, in orders.maps]
projected_pseudo_ring_order [lemma, in orders.rings]
projection_morphism [instance, in theory.setoids]
propers [section, in orders.maps]
proper_arrows [definition, in categories.categories]
PropHolds [record, in misc.util]
PropHolds [inductive, in misc.util]
prop_holds [projection, in misc.util]
prop_holds [constructor, in misc.util]
PseudoOrder [record, in interfaces.orders]
PseudoSemiRingOrder [record, in interfaces.orders]
pseudo_order_lt_apart_flip [lemma, in orders.orders]
pseudo_order_embedding_inj [lemma, in orders.maps]
pseudo_semiring_order [section, in orders.semirings]
pseudo_srorder_partial_minus [projection, in interfaces.orders]
pseudo_srorder_pos_mult_compat [projection, in interfaces.orders]
pseudo_order [section, in orders.orders]
pseudo_injective [section, in orders.maps]
pseudo_srorder_mult_ext [projection, in interfaces.orders]
pseudo_srorder_strict [projection, in interfaces.orders]
pseudo_srorder_plus [projection, in interfaces.orders]
pseudo_order_cotrans [projection, in interfaces.orders]
pseudo_order_lt_apart [lemma, in orders.orders]
pseudo_order_antisym [projection, in interfaces.orders]
pseudo_order_lt_ext [lemma, in orders.orders]
pseudo_order_cotrans_twice [lemma, in orders.orders]
pseudo_order_embedding_ext [instance, in orders.maps]
pseudo_order_setoid [projection, in interfaces.orders]
Pvars [definition, in theory.ua_subvariety]
P0 [lemma, in theory.ring_ideals]


Q

QtoFrac [abbreviation, in theory.rationals]
QType_Rationals.QType_Zpow [instance, in implementations.QType_rationals]
QType_Rationals.QType_0 [instance, in implementations.QType_rationals]
QType_Rationals.QType_equiv [instance, in implementations.QType_rationals]
QType_Rationals.QType_dec_mult_inv [instance, in implementations.QType_rationals]
QType_Rationals.QType_lt [instance, in implementations.QType_rationals]
QType_Rationals.anyQ_field_theory [lemma, in implementations.QType_rationals]
QType_Rationals.inject_Q_QType [instance, in implementations.QType_rationals]
QType_Rationals.QType_Npow [instance, in implementations.QType_rationals]
QType_Rationals [module, in implementations.QType_rationals]
QType_Rationals.QType_plus [instance, in implementations.QType_rationals]
QType_Rationals.QType_1 [instance, in implementations.QType_rationals]
QType_Rationals.QType_opp [instance, in implementations.QType_rationals]
QType_Rationals.inject_QType_Q [instance, in implementations.QType_rationals]
QType_Rationals.props [module, in implementations.QType_rationals]
QType_Rationals.QType_le [instance, in implementations.QType_rationals]
QType_Rationals.QType_mult [instance, in implementations.QType_rationals]
QType_rationals [library]
quote [projection, in theory.quote_monoid]
Quote [record, in theory.quote_monoid]
quote_zero [instance, in theory.quote_monoid]
quote_mult [instance, in theory.quote_monoid]
quote_equality [lemma, in theory.quote_monoid]
quote_new_var [instance, in theory.quote_monoid]
quote_old_var [instance, in theory.quote_monoid]
quote_monoid [library]
quote' [definition, in theory.quote_monoid]
quotients [lemma, in implementations.nonzero_field_elements]
quotient_variety [lemma, in theory.ua_congruence]
quot_obj [definition, in theory.ua_congruence]
Q_0 [instance, in implementations.stdlib_rationals]
Q_opp [instance, in implementations.stdlib_rationals]
Q_pow [instance, in implementations.stdlib_rationals]
Q_shiftl [instance, in implementations.stdlib_rationals]
Q_to_fracZ [instance, in implementations.stdlib_rationals]
Q_lt [instance, in implementations.stdlib_rationals]
Q_1 [instance, in implementations.stdlib_rationals]
Q_le [instance, in implementations.stdlib_rationals]
Q_plus [instance, in implementations.stdlib_rationals]
Q_mult [instance, in implementations.stdlib_rationals]
Q_mult_inv [instance, in implementations.stdlib_rationals]
Q_eq [instance, in implementations.stdlib_rationals]
Q_Npow [instance, in implementations.stdlib_rationals]


R

R [inductive, in misc.JMrelation]
RalgebraAction [record, in interfaces.canonical_names]
RalgebraAction [inductive, in interfaces.canonical_names]
ralgebra_action [projection, in interfaces.canonical_names]
ralgebra_action [constructor, in interfaces.canonical_names]
Rationals [record, in interfaces.rationals]
rationals [library]
rationals [library]
rationals [library]
RationalsToFrac [record, in interfaces.rationals]
RationalsToFrac [inductive, in interfaces.rationals]
rationals_and_another_rationals [section, in orders.rationals]
rationals_to_frac [projection, in interfaces.rationals]
rationals_to_frac [constructor, in interfaces.rationals]
rationals_to_rationals [definition, in theory.rationals]
rationals_order_isomorphic [section, in orders.rationals]
rationals_decompose_pos_den [lemma, in orders.rationals]
rationals_decompose [lemma, in theory.rationals]
rationals_decompose_le [lemma, in orders.rationals]
rationals_embed_ints [projection, in interfaces.rationals]
rationals_lt [instance, in orders.rationals]
rationals_frac [projection, in interfaces.rationals]
rationals_le [instance, in orders.rationals]
rationals_frac_mor [projection, in interfaces.rationals]
rationals_field [projection, in interfaces.rationals]
rationals_and_another_rationals.f_preserves_nonneg [variable, in orders.rationals]
rationals_to_frac [section, in interfaces.rationals]
rationals_and_integers [section, in orders.rationals]
rec_impl [definition, in theory.ua_products]
rec_impl_proper [instance, in theory.ua_products]
reflexive [lemma, in misc.JMrelation]
refl_arrows [definition, in theory.categories]
relate [constructor, in misc.JMrelation]
replicate_Sn [definition, in implementations.ne_list]
result [definition, in interfaces.ua_basic]
ret [projection, in interfaces.monads]
ret [constructor, in interfaces.monads]
retract_is_int_to_ring [definition, in theory.integers]
retract_is_int.for_another_ring [section, in theory.integers]
retract_is_nat.for_another_semirings [section, in theory.naturals]
retract_is_nat [definition, in theory.naturals]
retract_is_nat [section, in theory.naturals]
retract_is_int [definition, in theory.integers]
retract_is_nat_to_sr [definition, in theory.naturals]
retract_is_int [section, in theory.integers]
ret_proper [projection, in interfaces.monads]
ret_proper [instance, in implementations.cons_list]
RightAbsorb [record, in interfaces.canonical_names]
RightAbsorb [inductive, in interfaces.canonical_names]
RightCancellation [record, in interfaces.abstract_algebra]
RightCancellation [inductive, in interfaces.abstract_algebra]
RightHeteroDistribute [record, in interfaces.canonical_names]
RightHeteroDistribute [inductive, in interfaces.canonical_names]
RightIdentity [record, in interfaces.canonical_names]
RightIdentity [inductive, in interfaces.canonical_names]
RightInverse [record, in interfaces.canonical_names]
RightInverse [inductive, in interfaces.canonical_names]
right_cancellation_ne_0 [lemma, in theory.rings]
right_inverse [projection, in interfaces.canonical_names]
right_inverse [constructor, in interfaces.canonical_names]
right_cancel_from_left [lemma, in theory.rings]
right_absorb [projection, in interfaces.canonical_names]
right_absorb [constructor, in interfaces.canonical_names]
right_identity [projection, in interfaces.canonical_names]
right_identity [constructor, in interfaces.canonical_names]
right_cancellation [projection, in interfaces.abstract_algebra]
right_cancellation [constructor, in interfaces.abstract_algebra]
Ring [record, in interfaces.abstract_algebra]
ringmor_props [section, in theory.rings]
RingMult [record, in interfaces.canonical_names]
RingMult [inductive, in interfaces.canonical_names]
RingMultInverse [record, in interfaces.canonical_names]
RingMultInverse [inductive, in interfaces.canonical_names]
ringmult_is_semigroupop [instance, in interfaces.canonical_names]
RingOne [record, in interfaces.canonical_names]
RingOne [inductive, in interfaces.canonical_names]
ringone_is_monoidunit [instance, in interfaces.canonical_names]
RingPlus [record, in interfaces.canonical_names]
RingPlus [inductive, in interfaces.canonical_names]
ringplus_is_semigroupop [instance, in interfaces.canonical_names]
rings [library]
rings [library]
rings [library]
RingUnit [record, in interfaces.canonical_names]
RingUnit [inductive, in interfaces.canonical_names]
RingZero [record, in interfaces.canonical_names]
RingZero [inductive, in interfaces.canonical_names]
ringzero_is_monoidunit [instance, in interfaces.canonical_names]
ring_mult [projection, in interfaces.canonical_names]
ring_mult [constructor, in interfaces.canonical_names]
ring_props [section, in theory.rings]
ring_monoid [projection, in interfaces.abstract_algebra]
ring_zero [projection, in interfaces.canonical_names]
ring_zero [constructor, in interfaces.canonical_names]
Ring_Semi [instance, in theory.rings]
ring_group [projection, in interfaces.abstract_algebra]
ring_mult_inverse [projection, in interfaces.canonical_names]
ring_mult_inverse [constructor, in interfaces.canonical_names]
ring_dist [projection, in interfaces.abstract_algebra]
ring_mult_left_cancel [instance, in theory.rings]
ring_plus [projection, in interfaces.canonical_names]
ring_plus [constructor, in interfaces.canonical_names]
ring_unit_mult_inverse [projection, in interfaces.canonical_names]
ring_unit_mult_inverse [constructor, in interfaces.canonical_names]
ring_one [projection, in interfaces.canonical_names]
ring_one [constructor, in interfaces.canonical_names]
ring_order [section, in orders.rings]
ring_ideals [library]


S

same_morphism [lemma, in theory.naturals]
same_morphism [lemma, in implementations.natpair_integers]
same_morphism [lemma, in theory.integers]
ScalarMult [record, in interfaces.vectorspace]
ScalarMult [inductive, in interfaces.vectorspace]
scalar_mult [projection, in interfaces.vectorspace]
scalar_mult [constructor, in interfaces.vectorspace]
SemiGroup [record, in interfaces.abstract_algebra]
SemiGroupOp [record, in interfaces.canonical_names]
SemiGroupOp [inductive, in interfaces.canonical_names]
semigroups [library]
SemiGroup_Morphism [record, in interfaces.abstract_algebra]
semigroup_morphism_proper [instance, in theory.groups]
SemiRing [record, in interfaces.abstract_algebra]
semiringmor_a [projection, in interfaces.abstract_algebra]
semiringmor_props [section, in theory.rings]
semiringmor_plus_mor [projection, in interfaces.abstract_algebra]
semiringmor_b [projection, in interfaces.abstract_algebra]
semiringmor_mult_mor [projection, in interfaces.abstract_algebra]
SemiRingOrder [record, in interfaces.orders]
semirings [library]
semirings [library]
semiring_pairs.with_semiring_order [section, in implementations.semiring_pairs]
semiring_props [section, in theory.rings]
semiring_plus_monoid [projection, in interfaces.abstract_algebra]
semiring_pairs.with_strict_semiring_order [section, in implementations.semiring_pairs]
SemiRing_Morphism [record, in interfaces.abstract_algebra]
semiring_pairs.with_full_pseudo_semiring_order [section, in implementations.semiring_pairs]
semiring_order [section, in orders.semirings]
semiring_pairs [section, in implementations.semiring_pairs]
semiring_morphism_proper [instance, in theory.rings]
semiring_folds [section, in theory.sequences]
semiring_pairs.SRpair_mult_proper_r [variable, in implementations.semiring_pairs]
semiring_mult_monoid [projection, in interfaces.abstract_algebra]
semiring_left_absorb [projection, in interfaces.abstract_algebra]
semiring_distr [projection, in interfaces.abstract_algebra]
semiring_pairs [library]
Sequence [record, in interfaces.sequences]
sequences [library]
sequences [library]
sequence_extend_makes_morphisms [projection, in interfaces.sequences]
sequence_inject_natural [projection, in interfaces.sequences]
sequence_fmap_id [projection, in interfaces.sequences]
sequence_adjunction [projection, in interfaces.sequences]
sequence_makes_monoids [projection, in interfaces.sequences]
sequence_fmap_proper [projection, in interfaces.sequences]
sequence_fmap_comp [projection, in interfaces.sequences]
sequence_extend_morphism [projection, in interfaces.sequences]
sequence_only_extend_commutes [projection, in interfaces.sequences]
sequence_extend_commutes [projection, in interfaces.sequences]
sequence_inject_morphism [projection, in interfaces.sequences]
sequence_map_morphism [projection, in interfaces.sequences]
series [section, in theory.series]
series [library]
series.every_other [section, in theory.series]
series.factorials [section, in theory.series]
series.mult [section, in theory.series]
series.positives [section, in theory.series]
series.powers [section, in theory.series]
series.powers.with_nat_pow [section, in theory.series]
series.powers.with_int_pow [section, in theory.series]
Setoid [record, in interfaces.abstract_algebra]
Setoid [inductive, in interfaces.abstract_algebra]
setoidmor_a [projection, in interfaces.abstract_algebra]
setoidmor_b [projection, in interfaces.abstract_algebra]
setoids [library]
setoids [library]
setoids [library]
setoid_eq [projection, in interfaces.abstract_algebra]
setoid_eq [constructor, in interfaces.abstract_algebra]
setoid_morphisms [section, in interfaces.abstract_algebra]
setoid_proof [projection, in categories.setoids]
setoid_functor [section, in interfaces.functors]
setoid_binary_morphisms [section, in interfaces.abstract_algebra]
Setoid_Morphism [record, in interfaces.abstract_algebra]
setoid_functor_as_posh_functor [section, in theory.functors]
setoid_tactics [library]
sfmap [projection, in interfaces.functors]
sfmap [constructor, in interfaces.functors]
SFmap [record, in interfaces.functors]
SFmap [inductive, in interfaces.functors]
SFunctor [record, in interfaces.functors]
sfunctor_comp [projection, in interfaces.functors]
sfunctor_morphism [projection, in interfaces.functors]
sfunctor_makes_morphisms [projection, in interfaces.functors]
sfunctor_makes_setoids [projection, in interfaces.functors]
sfunctor_id [projection, in interfaces.functors]
sgmor_setmor [projection, in interfaces.abstract_algebra]
sgmor_b [projection, in interfaces.abstract_algebra]
sgmor_a [projection, in interfaces.abstract_algebra]
sg_op [projection, in interfaces.canonical_names]
sg_op [constructor, in interfaces.canonical_names]
sg_op_proper [projection, in interfaces.abstract_algebra]
sg_setoid [projection, in interfaces.abstract_algebra]
sg_inv_distr [lemma, in theory.groups]
sg_ass [projection, in interfaces.abstract_algebra]
shiftl [section, in theory.shiftl]
ShiftL [record, in interfaces.additional_operations]
ShiftL [inductive, in interfaces.additional_operations]
shiftl [projection, in interfaces.additional_operations]
shiftl [constructor, in interfaces.additional_operations]
shiftl [library]
ShiftLSpec [record, in interfaces.additional_operations]
shiftl_le_flip_l [lemma, in theory.shiftl]
shiftl_opp_1_to_half [lemma, in theory.shiftl]
shiftl_spec_from_int_pow [lemma, in interfaces.additional_operations]
shiftl_opp [lemma, in theory.shiftl]
shiftl_le_flip_r [lemma, in theory.shiftl]
shiftl_inj [instance, in theory.shiftl]
shiftl_opp_to_mult_inv_nat_pow [lemma, in theory.shiftl]
shiftl_nonneg [instance, in theory.shiftl]
shiftl_opp_nat_pow [lemma, in theory.shiftl]
shiftl_int_pow [lemma, in theory.shiftl]
shiftl_base_nat_pow [lemma, in theory.shiftl]
shiftl_exp_plus [lemma, in theory.shiftl]
shiftl_reverse [lemma, in theory.shiftl]
shiftl_S [projection, in interfaces.additional_operations]
shiftl_base_0 [instance, in theory.shiftl]
shiftl_mult_r [lemma, in theory.shiftl]
shiftl_dec_field [section, in theory.shiftl]
shiftl_mult_l [lemma, in theory.shiftl]
shiftl_ne_0 [instance, in theory.shiftl]
shiftl_base_1_to_int_pow [lemma, in theory.shiftl]
shiftl_spec_from_nat_pow [lemma, in interfaces.additional_operations]
shiftl_base_1_int_pow [lemma, in theory.shiftl]
shiftl_order [lemma, in theory.shiftl]
shiftl_pos [instance, in theory.shiftl]
shiftl_opp_1_half [lemma, in theory.shiftl]
shiftl_nat_pow_alt [lemma, in theory.shiftl]
shiftl_opp_1_to_fourth [lemma, in theory.shiftl]
shiftl_opp_1_fourth [lemma, in theory.shiftl]
shiftl_to_int_pow [lemma, in theory.shiftl]
shiftl_field [section, in theory.shiftl]
shiftl_1 [lemma, in theory.shiftl]
shiftl_nat_pow [lemma, in theory.shiftl]
shiftl_0 [projection, in interfaces.additional_operations]
shiftl_proper [projection, in interfaces.additional_operations]
shiftl_strong_inj [instance, in theory.shiftl]
shiftl_base_plus [lemma, in theory.shiftl]
shiftl_2 [lemma, in theory.shiftl]
shiftl.shiftl_strict_order_embedding [variable, in theory.shiftl]
shiftr [projection, in interfaces.additional_operations]
shiftr [constructor, in interfaces.additional_operations]
ShiftR [record, in interfaces.additional_operations]
ShiftR [inductive, in interfaces.additional_operations]
ShiftRSpec [record, in interfaces.additional_operations]
shiftr_proper [projection, in interfaces.additional_operations]
shiftr_0 [projection, in interfaces.additional_operations]
shiftr_S [projection, in interfaces.additional_operations]
sig [definition, in varieties.semirings]
sig [definition, in varieties.monoids]
sig [definition, in varieties.setoids]
sig [definition, in varieties.empty]
sig [definition, in varieties.semigroups]
sig [definition, in varieties.rings]
sig [definition, in varieties.groups]
Signature [record, in interfaces.ua_basic]
sigT_equiv [definition, in interfaces.canonical_names]
sigT_Setoid [instance, in theory.setoids]
sig_type_trans [instance, in interfaces.ua_basic]
sig_type_sym [instance, in interfaces.ua_basic]
sig_Setoid [instance, in theory.setoids]
sig_apart [definition, in interfaces.canonical_names]
sig_type_trans' [instance, in interfaces.ua_basic]
sig_equiv [definition, in interfaces.canonical_names]
sig_strong_setoid [instance, in theory.strong_setoids]
sig_type_refl [lemma, in interfaces.ua_basic]
simple [module, in quote.classquote]
simpleZ_abs [instance, in implementations.natpair_integers]
simple_distribute_r [projection, in interfaces.canonical_names]
simple_associativity [projection, in interfaces.canonical_names]
simple_associativity [constructor, in interfaces.canonical_names]
simple_distribute_l [projection, in interfaces.canonical_names]
simple_product [section, in theory.setoids]
simple.approach_A.Quote [record, in quote.classquote]
simple.approach_A.Quote [inductive, in quote.classquote]
simple.approach_B.example [lemma, in quote.classquote]
simple.approach_B.instances [section, in quote.classquote]
simple.approach_A.quote [projection, in quote.classquote]
simple.approach_A.quote [constructor, in quote.classquote]
simple.approach_B [module, in quote.classquote]
simple.approach_B.quote [projection, in quote.classquote]
simple.approach_A.example [lemma, in quote.classquote]
simple.approach_B.do_quote [lemma, in quote.classquote]
simple.approach_A [module, in quote.classquote]
simple.approach_B.Quote [record, in quote.classquote]
simple.approach_B.eval_quote [projection, in quote.classquote]
simple.approach_A.instances [section, in quote.classquote]
simple.eval [definition, in quote.classquote]
simple.Expr [inductive, in quote.classquote]
simple.Mult [constructor, in quote.classquote]
simple.One [constructor, in quote.classquote]
simple.Plus [constructor, in quote.classquote]
simple.Zero [constructor, in quote.classquote]
simplify [definition, in theory.monoid_normalization]
singlevar [definition, in theory.quote_monoid]
single_sorted_signature [definition, in interfaces.ua_basic]
slow_int_abs [instance, in theory.int_abs]
slow_nat_le_dec [instance, in orders.naturals]
slow_rat_dec [instance, in theory.rationals]
sm_proper [projection, in interfaces.abstract_algebra]
sort [definition, in orders.minmax]
sorts [projection, in interfaces.ua_basic]
sort_proper [instance, in orders.minmax]
specializable [section, in interfaces.integers]
specialized [section, in varieties.monoids]
specialized [section, in varieties.semigroups]
square [lemma, in theory.ua_congruence]
square_nonneg [lemma, in orders.semirings]
square_pos [lemma, in orders.semirings]
srorder_partial_minus [projection, in interfaces.orders]
srorder_plus [projection, in interfaces.orders]
srorder_po [projection, in interfaces.orders]
SRpair [record, in implementations.semiring_pairs]
SRpair_lt [instance, in implementations.semiring_pairs]
SRpair_0 [instance, in implementations.semiring_pairs]
SRpair_le [instance, in implementations.semiring_pairs]
SRpair_equiv [instance, in implementations.semiring_pairs]
SRpair_opp [instance, in implementations.semiring_pairs]
SRpair_plus [instance, in implementations.semiring_pairs]
SRpair_trivial_apart [instance, in implementations.semiring_pairs]
SRpair_1 [instance, in implementations.semiring_pairs]
SRpair_dec [instance, in implementations.semiring_pairs]
SRpair_apart [instance, in implementations.semiring_pairs]
SRpair_mult [instance, in implementations.semiring_pairs]
SRpair_le_dec [instance, in implementations.semiring_pairs]
SRpair_inject [instance, in implementations.semiring_pairs]
SRpair_splits [lemma, in implementations.semiring_pairs]
stable [projection, in misc.util]
stable [constructor, in misc.util]
Stable [record, in misc.util]
Stable [inductive, in misc.util]
Statement [inductive, in interfaces.universal_algebra]
stdlib_semiring_theory [lemma, in theory.rings]
stdlib_ring_theory [lemma, in theory.rings]
stdlib_field_theory [definition, in theory.dec_fields]
stdlib_binary_integers [library]
stdlib_rationals [library]
stdlib_binary_naturals [library]
StdQ [abbreviation, in implementations.dyadics]
StdQtoQ [abbreviation, in implementations.dyadics]
streams [section, in theory.streams]
streams [library]
stream_eq [instance, in theory.streams]
stream_eq_coind [constructor, in theory.streams]
Stream_eq_coind [inductive, in theory.streams]
stream_eq_Str_nth [lemma, in theory.streams]
StrictlyOrderPreserving [record, in interfaces.orders]
StrictlyOrderPreservingBack [record, in interfaces.orders]
strictly_order_preserving_morphism [projection, in interfaces.orders]
strictly_order_preserving_back_mor [instance, in orders.maps]
strictly_order_preserving_inj [instance, in orders.maps]
strictly_order_preserving_flip [lemma, in orders.maps]
strictly_order_preserving_back [projection, in interfaces.orders]
strictly_order_preserving_flip_pos [lemma, in orders.maps]
strictly_order_preserving_back_flip [lemma, in orders.maps]
strictly_order_preserving_pos [lemma, in orders.maps]
strictly_order_preserving [section, in orders.maps]
strictly_order_preserving_back_morphism [projection, in interfaces.orders]
strictly_order_preserving_dec [section, in orders.maps]
strictly_order_preserving [projection, in interfaces.orders]
StrictOrderEmbedding [record, in interfaces.orders]
StrictOrder_Morphism [record, in interfaces.orders]
StrictPartialOrder [record, in interfaces.orders]
StrictSemiRingOrder [record, in interfaces.orders]
StrictSetoidOrder [record, in interfaces.orders]
strict_po_po [projection, in interfaces.orders]
strict_order_morphism_proper_a [projection, in interfaces.orders]
strict_po_apart_ne [instance, in orders.orders]
strict_srorder_partial_minus [projection, in interfaces.orders]
strict_srorder_so [projection, in interfaces.orders]
strict_semiring_order [section, in orders.semirings]
strict_order_embedding_preserving [projection, in interfaces.orders]
strict_order_embedding_back [projection, in interfaces.orders]
strict_srorder_plus [projection, in interfaces.orders]
strict_order_morphism_mor [projection, in interfaces.orders]
strict_partial_order [section, in orders.orders]
strict_po_setoid [projection, in interfaces.orders]
strict_order_morphism_proper_b [projection, in interfaces.orders]
strict_order [section, in orders.orders]
strict_ring_order [section, in orders.rings]
strict_po_trans [projection, in interfaces.orders]
strict_setoid_order_setoid [projection, in interfaces.orders]
strict_setoid_order_proper [projection, in interfaces.orders]
strict_setoid_order_strict [projection, in interfaces.orders]
StrongInjective [record, in interfaces.abstract_algebra]
StrongLeftCancellation [record, in interfaces.abstract_algebra]
StrongLeftCancellation [inductive, in interfaces.abstract_algebra]
StrongRightCancellation [record, in interfaces.abstract_algebra]
StrongRightCancellation [inductive, in interfaces.abstract_algebra]
StrongSemiRing_Morphism [record, in interfaces.abstract_algebra]
StrongSetoid [record, in interfaces.abstract_algebra]
StrongSetoid_BinaryMorphism [record, in interfaces.abstract_algebra]
StrongSetoid_Morphism [record, in interfaces.abstract_algebra]
strong_setoid_irreflexive [projection, in interfaces.abstract_algebra]
strong_binary_setoidmor_c [projection, in interfaces.abstract_algebra]
strong_semiringmor_sr_mor [projection, in interfaces.abstract_algebra]
strong_right_cancel_from_left [lemma, in theory.rings]
strong_extensionality [projection, in interfaces.abstract_algebra]
strong_setoid_morphism_1 [instance, in theory.strong_setoids]
strong_binary_setoidmor_a [projection, in interfaces.abstract_algebra]
strong_setoid_morphism_unary_2 [instance, in theory.strong_setoids]
strong_binary_setoid_morphism_commutative [lemma, in theory.strong_setoids]
strong_setoid_cotrans [projection, in interfaces.abstract_algebra]
strong_right_cancellation [projection, in interfaces.abstract_algebra]
strong_right_cancellation [constructor, in interfaces.abstract_algebra]
strong_left_cancellation_cancel [instance, in theory.rings]
strong_semiringmor_strong_mor [projection, in interfaces.abstract_algebra]
strong_setoidmor_b [projection, in interfaces.abstract_algebra]
strong_binary_extensionality [projection, in interfaces.abstract_algebra]
strong_left_cancellation [projection, in interfaces.abstract_algebra]
strong_left_cancellation [constructor, in interfaces.abstract_algebra]
strong_cancellation [section, in theory.rings]
strong_injective [projection, in interfaces.abstract_algebra]
strong_right_cancellation_cancel [instance, in theory.rings]
strong_binary_setoidmor_b [projection, in interfaces.abstract_algebra]
strong_morphism_proper [instance, in theory.strong_setoids]
strong_injective_preserves_0 [lemma, in theory.fields]
strong_setoid_symmetric [projection, in interfaces.abstract_algebra]
strong_setoidmor_a [projection, in interfaces.abstract_algebra]
strong_injective_injective [instance, in theory.strong_setoids]
strong_binary_setoid_morphism_both_coordinates [lemma, in theory.strong_setoids]
strong_injective_mor [projection, in interfaces.abstract_algebra]
strong_setoids [library]
structural_eq_refl [instance, in varieties.open_terms]
structural_eq_refl [instance, in varieties.closed_terms]
structure [section, in interfaces.monads]
Str_nth_positives [lemma, in theory.series]
Str_nth_positives_help [lemma, in theory.series]
Str_nth_powers [lemma, in theory.series]
Str_nth_everyOther [lemma, in theory.series]
Str_nth_tl_everyOther [lemma, in theory.series]
Str_nth_powers_help [lemma, in theory.series]
Str_nth_factorials [lemma, in theory.series]
Str_nth_powers_int_pow [lemma, in theory.series]
Str_nth_factorials_help [lemma, in theory.series]
Str_nth_powers_help_int_pow [lemma, in theory.series]
subalgebra [instance, in theory.ua_subalgebra]
subalgebra [instance, in theory.ua_subalgebraT]
subalgebras [section, in theory.ua_subalgebraT]
subalgebras [section, in theory.ua_subalgebra]
subobject [definition, in theory.ua_congruence]
subset_proper [projection, in theory.ua_subalgebraT]
subset_closed [projection, in theory.ua_subalgebraT]
subset_closed [projection, in theory.ua_subalgebra]
subset_proper [projection, in theory.ua_subalgebra]
subst_eval [lemma, in varieties.closed_terms]
sum [definition, in theory.sequences]
surjective [projection, in interfaces.abstract_algebra]
Surjective [record, in interfaces.abstract_algebra]
surjective_applied [lemma, in theory.jections]
Surjective_proper [instance, in theory.jections]
surjective_mor [projection, in interfaces.abstract_algebra]
surjective_applied' [lemma, in theory.jections]
symmetric [lemma, in misc.JMrelation]
sym_arrows [definition, in categories.categories]
S_nat_1_plus [lemma, in implementations.peano_naturals]
S_nat_plus_1 [lemma, in implementations.peano_naturals]


T

T [definition, in interfaces.universal_algebra]
T [projection, in categories.setoids]
tail [definition, in implementations.ne_list]
tails [definition, in implementations.ne_list]
tails_are_shorter [lemma, in implementations.ne_list]
tail_args [definition, in theory.ua_packed]
take [definition, in implementations.ne_list]
TargetObject [abbreviation, in theory.forget_algebra]
Term [inductive, in interfaces.universal_algebra]
Term [abbreviation, in theory.quote_monoid]
Term [inductive, in theory.monoid_normalization]
Term0 [definition, in interfaces.universal_algebra]
theory [definition, in varieties.monoids]
theory [definition, in varieties.setoids]
theory [definition, in varieties.groups]
theory [definition, in varieties.semigroups]
theory [definition, in varieties.rings]
theory [definition, in varieties.empty]
theory [definition, in varieties.semirings]
the_object [definition, in varieties.closed_terms]
the_object [definition, in varieties.open_terms]
the_arrow [definition, in varieties.closed_terms]
tight_apart [projection, in interfaces.abstract_algebra]
tl_length [lemma, in implementations.ne_list]
toR [abbreviation, in implementations.peano_naturals]
total [projection, in interfaces.canonical_names]
total [constructor, in interfaces.canonical_names]
TotalRelation [record, in interfaces.canonical_names]
TotalRelation [inductive, in interfaces.canonical_names]
to_ring_injective [lemma, in theory.integers]
to_ring_unique [lemma, in theory.integers]
to_frac_inverse [instance, in theory.rationals]
to_semiring_involutive [lemma, in theory.naturals]
to_ring_twice [lemma, in theory.integers]
to_frac_unique [lemma, in theory.rationals]
to_nat [instance, in implementations.nonneg_integers_naturals]
to_rationals_unique [lemma, in theory.rationals]
to_semiring_injective [lemma, in theory.naturals]
to_semiring_nonneg [lemma, in orders.naturals]
to_ua [definition, in theory.monoid_normalization]
to_rationals_unique_alt [lemma, in theory.rationals]
to_ring_self [lemma, in theory.integers]
to_list [definition, in implementations.ne_list]
to_rationals_involutive [lemma, in theory.rationals]
to_semiring_self [lemma, in theory.naturals]
to_semiring_unique_alt [lemma, in theory.naturals]
to_ring_unique_alt [lemma, in theory.integers]
to_semiring_twice [lemma, in theory.naturals]
to_semiring_unique [lemma, in theory.naturals]
to_ring_involutive [lemma, in theory.integers]
transfer_statement [lemma, in theory.ua_transference]
transfer_eval' [lemma, in theory.ua_transference]
transfer_statement_and_vars [lemma, in theory.ua_transference]
transfer_eval [lemma, in theory.ua_transference]
transitive [lemma, in misc.JMrelation]
trans_arrows [definition, in categories.categories]
trichotomy [projection, in interfaces.canonical_names]
trichotomy [constructor, in interfaces.canonical_names]
Trichotomy [record, in interfaces.canonical_names]
Trichotomy [inductive, in interfaces.canonical_names]
TrivialApart [record, in interfaces.canonical_names]
TrivialApart [inductive, in interfaces.canonical_names]
trivial_apart [projection, in interfaces.canonical_names]
trivial_apart [constructor, in interfaces.canonical_names]
tuple_round_trip [lemma, in theory.categories]
tuple_proj [projection, in theory.categories]
tuple_proj [constructor, in theory.categories]
two_level_rect [lemma, in implementations.ne_list]
T0 [definition, in interfaces.universal_algebra]


U

ua [module, in theory.quote_monoid]
ua [module, in interfaces.sequences]
uaTerm [abbreviation, in theory.monoid_normalization]
ua_vars_equiv [instance, in interfaces.universal_algebra]
ua_term_monad [library]
ua_packed [library]
ua_mapped_operations [library]
ua_congruence [library]
ua_subvariety [library]
ua_subalgebra [library]
ua_basic [library]
ua_products [library]
ua_homomorphisms [library]
ua_transference [library]
ua_subalgebraT [library]
uncurry [definition, in misc.util]
Unit [constructor, in theory.monoid_normalization]
unit [library]
units_dont_divide_zero [lemma, in theory.rings]
UniversalArrow [section, in theory.categories]
UniversalArrow [record, in theory.categories]
UniversalArrow [inductive, in theory.categories]
universal_arrow [projection, in theory.categories]
universal_arrow [constructor, in theory.categories]
universal_algebra [library]
univwit [definition, in theory.adjunctions]
uniwit [instance, in theory.adjunctions]
unJM [lemma, in misc.JMrelation]
upper_classes [section, in interfaces.abstract_algebra]
util [library]


V

Var [constructor, in theory.monoid_normalization]
Var [constructor, in interfaces.universal_algebra]
varieties [section, in theory.ua_products]
varieties [library]
varieties.carrier_e [variable, in theory.ua_products]
variety [instance, in varieties.empty]
variety [instance, in varieties.semirings]
variety_carriers [projection, in categories.varieties]
variety_proof [projection, in categories.varieties]
variety_laws [projection, in interfaces.universal_algebra]
variety_algebra [projection, in interfaces.universal_algebra]
variety_equiv [projection, in categories.varieties]
variety_ops [projection, in categories.varieties]
Vars [definition, in interfaces.universal_algebra]
Vars [definition, in theory.quote_monoid]
VectorSpace [record, in interfaces.vectorspace]
vectorspace [library]
vs_field [projection, in interfaces.vectorspace]
vs_assoc [projection, in interfaces.vectorspace]
vs_abgroup [projection, in interfaces.vectorspace]
vs_distr_r [projection, in interfaces.vectorspace]
vs_left_identity [projection, in interfaces.vectorspace]
vs_distr_l [projection, in interfaces.vectorspace]
vv [abbreviation, in theory.ua_congruence]


W

with_vars.bla [lemma, in quote.classquote]
with_vars.quote_equality [lemma, in quote.classquote]
with_vars.novars [definition, in quote.classquote]
with_sorts.Sorts [variable, in interfaces.ua_basic]
with_vars.eval_quote' [definition, in quote.classquote]
with_vars.Quote [record, in quote.classquote]
with_vars.quote_old_var [instance, in quote.classquote]
with_vars.Var [constructor, in quote.classquote]
with_vars.obvious_sum_dst_l [instance, in quote.classquote]
with_vars.Vars [definition, in quote.classquote]
with_vars.Lookup [record, in quote.classquote]
with_vars.inspect.x [variable, in quote.classquote]
with_vars.eval_map_var [lemma, in quote.classquote]
with_vars.quote_mult [instance, in quote.classquote]
with_vars.obvious_sum_src [instance, in quote.classquote]
with_vars.obvious [projection, in quote.classquote]
with_vars.obvious [constructor, in quote.classquote]
with_vars.inspect [section, in quote.classquote]
with_vars.quote [projection, in quote.classquote]
with_vars.lookup_right [instance, in quote.classquote]
with_vars.obvious_sum_dst_r [instance, in quote.classquote]
with_vars.Obvious [record, in quote.classquote]
with_vars.Obvious [inductive, in quote.classquote]
with_sorts [section, in interfaces.ua_basic]
with_vars.eval [definition, in quote.classquote]
with_vars.quote_zero [instance, in quote.classquote]
with_vars.Quote [section, in quote.classquote]
with_vars.eval_quote [projection, in quote.classquote]
with_vars.lookup_left [instance, in quote.classquote]
with_vars.quote' [definition, in quote.classquote]
with_vars.map_var [definition, in quote.classquote]
with_vars.lookup [projection, in quote.classquote]
with_vars.Value [definition, in quote.classquote]
with_vars.lookup_correct [projection, in quote.classquote]
with_vars.Expr [inductive, in quote.classquote]
with_vars.inspect.y [variable, in quote.classquote]
with_vars.sum_assoc [lemma, in quote.classquote]
with_vars [module, in quote.classquote]
with_vars.eval_proper [instance, in quote.classquote]
with_sorts.carrier [variable, in interfaces.ua_basic]
with_vars.merge [definition, in quote.classquote]
with_vars.monkey [lemma, in quote.classquote]
with_vars.singlevar [definition, in quote.classquote]
with_vars.quote_new_var [instance, in quote.classquote]
with_vars.Zero [constructor, in quote.classquote]
with_vars.Mult [constructor, in quote.classquote]
with_vars.Lookup [section, in quote.classquote]
with_vars.obvious [section, in quote.classquote]
workarounds [library]
workaround_tactics [library]


X

x [abbreviation, in varieties.monoids]
x [abbreviation, in varieties.semirings]
x [abbreviation, in varieties.groups]
x [abbreviation, in varieties.semigroups]
x [abbreviation, in varieties.rings]
x' [abbreviation, in theory.naturals]


Y

y [abbreviation, in varieties.groups]
y [abbreviation, in varieties.semirings]
y [abbreviation, in varieties.rings]
y [abbreviation, in varieties.semigroups]
y [abbreviation, in varieties.monoids]
y' [abbreviation, in theory.naturals]


Z

z [abbreviation, in varieties.rings]
z [abbreviation, in varieties.monoids]
Z [abbreviation, in implementations.natpair_integers]
z [abbreviation, in varieties.groups]
z [abbreviation, in varieties.semigroups]
z [abbreviation, in varieties.semirings]
zero [constructor, in varieties.semirings]
zero [constructor, in varieties.rings]
ZeroDivisor [record, in interfaces.canonical_names]
ZeroDivisor [inductive, in interfaces.canonical_names]
ZeroProduct [record, in interfaces.canonical_names]
ZeroProduct [inductive, in interfaces.canonical_names]
zero_sum [lemma, in theory.naturals]
zero_product_no_zero_divisors [instance, in interfaces.canonical_names]
zero_product [instance, in theory.integers]
zero_divisor [projection, in interfaces.canonical_names]
zero_divisor [constructor, in interfaces.canonical_names]
zero_product_aux [lemma, in implementations.natpair_integers]
zero_product [projection, in interfaces.canonical_names]
zero_product [constructor, in interfaces.canonical_names]
zipWith_proper [instance, in theory.streams]
ZPos_cut_minus [instance, in implementations.nonneg_integers_naturals]
ZPos_to_nat_sr_morphism [instance, in implementations.nonneg_integers_naturals]
ZtoQ [abbreviation, in theory.rationals]
ZtoQ_shift [lemma, in implementations.dyadics]
ZtoStdQ [abbreviation, in implementations.dyadics]
ZType_Integers.axioms [module, in implementations.ZType_integers]
ZType_Integers.ZType_Npow [instance, in implementations.ZType_integers]
ZType_Integers.ZType_1 [instance, in implementations.ZType_integers]
ZType_Integers [module, in implementations.ZType_integers]
ZType_Integers.ZType_equiv [instance, in implementations.ZType_integers]
ZType_Integers.ZType_plus [instance, in implementations.ZType_integers]
ZType_Integers.ZType_pow [instance, in implementations.ZType_integers]
ZType_Integers.ZType_two_2 [lemma, in implementations.ZType_integers]
ZType_Integers.ZType_shiftl [instance, in implementations.ZType_integers]
ZType_Integers.ZType_0 [instance, in implementations.ZType_integers]
ZType_Integers.ZType_ring_theory [lemma, in implementations.ZType_integers]
ZType_Integers.ZType_div [instance, in implementations.ZType_integers]
ZType_Integers.ZType_succ_1_plus [lemma, in implementations.ZType_integers]
ZType_Integers.ZType_mult [instance, in implementations.ZType_integers]
ZType_Integers.inject_ZType_Z [instance, in implementations.ZType_integers]
ZType_Integers.ZType_opp [instance, in implementations.ZType_integers]
ZType_Integers.ZType_le [instance, in implementations.ZType_integers]
ZType_Integers.ZType_mod [instance, in implementations.ZType_integers]
ZType_Integers.ZType_lt [instance, in implementations.ZType_integers]
ZType_Integers.inject_Z_ZType [instance, in implementations.ZType_integers]
ZType_integers [library]
Z_le [instance, in implementations.stdlib_binary_integers]
Z_0 [instance, in implementations.stdlib_binary_integers]
Z_plus [instance, in implementations.stdlib_binary_integers]
Z_shiftl [instance, in implementations.stdlib_binary_integers]
Z_1 [instance, in implementations.stdlib_binary_integers]
Z_Npow [instance, in implementations.stdlib_binary_integers]
z_to_ring [instance, in implementations.natpair_integers]
Z_to_Npair [instance, in implementations.stdlib_binary_integers]
Z_lt [instance, in implementations.stdlib_binary_integers]
z_to_r [abbreviation, in implementations.natpair_integers]
Z_opp [instance, in implementations.stdlib_binary_integers]
Z_mult [instance, in implementations.stdlib_binary_integers]
Z_Nshiftl [instance, in implementations.stdlib_binary_integers]
Z_pow [instance, in implementations.stdlib_binary_integers]
Z_equiv [instance, in implementations.stdlib_binary_integers]
z' [abbreviation, in theory.naturals]


other

_ = _ (type_scope) [notation, in interfaces.canonical_names]
_ ≠ _ (type_scope) [notation, in interfaces.canonical_names]
_ ⪥ _ (type_scope) [notation, in interfaces.canonical_names]
_ < _ < _ [notation, in interfaces.canonical_names]
_ >> _ [notation, in interfaces.monads]
_ ∸ _ [notation, in interfaces.additional_operations]
_ ≤ _ ≤ _ [notation, in interfaces.canonical_names]
_ / _ [notation, in interfaces.canonical_names]
_ ◎ _ [notation, in interfaces.canonical_names]
_ ≡ _ [notation, in interfaces.canonical_names]
_ ⇛ _ [notation, in theory.categories]
_ ≪ _ [notation, in interfaces.additional_operations]
_ ⟶ _ [notation, in interfaces.canonical_names]
_ ↾ _ [notation, in interfaces.canonical_names]
_ ∞ [notation, in interfaces.canonical_names]
_ ⁻ [notation, in interfaces.canonical_names]
_ - _ [notation, in interfaces.canonical_names]
_ ≢ _ [notation, in interfaces.canonical_names]
_ ₀ [notation, in interfaces.canonical_names]
_ · _ [notation, in interfaces.vectorspace]
_ ₊ [notation, in interfaces.canonical_names]
_ // _ [notation, in interfaces.canonical_names]
_ ⁺ [notation, in interfaces.canonical_names]
_ ← _ ; _ [notation, in interfaces.monads]
_ & _ [notation, in interfaces.canonical_names]
_ >>= _ [notation, in interfaces.monads]
_ $ _ [notation, in implementations.dyadics]
_ ^ _ [notation, in interfaces.additional_operations]
_ < _ ≤ _ [notation, in interfaces.canonical_names]
_ `div` _ [notation, in interfaces.additional_operations]
_ ≤ _ < _ [notation, in interfaces.canonical_names]
_ `mod` _ [notation, in interfaces.additional_operations]
_ ⁻¹ [notation, in interfaces.canonical_names]
_ < _ [notation, in interfaces.canonical_names]
_ ≫ _ [notation, in interfaces.additional_operations]
_ * _ [notation, in interfaces.canonical_names]
_ + _ [notation, in interfaces.canonical_names]
_ ≤ _ [notation, in interfaces.canonical_names]
' _ [notation, in interfaces.canonical_names]
(& _ ) [notation, in interfaces.canonical_names]
(&) [notation, in interfaces.canonical_names]
( _ &) [notation, in interfaces.canonical_names]
( _ ≡) [notation, in interfaces.canonical_names]
( _ =) [notation, in interfaces.canonical_names]
( _ *.) [notation, in interfaces.canonical_names]
( _ ≢) [notation, in interfaces.canonical_names]
( _ <) [notation, in interfaces.canonical_names]
( _ ≪) [notation, in interfaces.additional_operations]
( _ ◎) [notation, in interfaces.canonical_names]
( _ +) [notation, in interfaces.canonical_names]
( _ ⪥) [notation, in interfaces.canonical_names]
( _ ·) [notation, in interfaces.vectorspace]
( _ ^) [notation, in interfaces.additional_operations]
( _ ≤) [notation, in interfaces.canonical_names]
( _ ≠) [notation, in interfaces.canonical_names]
(+ _ ) [notation, in interfaces.canonical_names]
(+) [notation, in interfaces.canonical_names]
(-) [notation, in interfaces.canonical_names]
(.* _ ) [notation, in interfaces.canonical_names]
(.*.) [notation, in interfaces.canonical_names]
(/) [notation, in interfaces.canonical_names]
(//) [notation, in interfaces.canonical_names]
(< _ ) [notation, in interfaces.canonical_names]
(<) [notation, in interfaces.canonical_names]
(= _ ) [notation, in interfaces.canonical_names]
(=) [notation, in interfaces.canonical_names]
(^ _ ) [notation, in interfaces.additional_operations]
(^) [notation, in interfaces.additional_operations]
(→) [notation, in interfaces.canonical_names]
(∸) [notation, in interfaces.additional_operations]
(≠ _ ) [notation, in interfaces.canonical_names]
(≠) [notation, in interfaces.canonical_names]
(≡ _ ) [notation, in interfaces.canonical_names]
(≡) [notation, in interfaces.canonical_names]
(≢ _ ) [notation, in interfaces.canonical_names]
(≢) [notation, in interfaces.canonical_names]
(≤ _ ) [notation, in interfaces.canonical_names]
(≤) [notation, in interfaces.canonical_names]
(≪ _ ) [notation, in interfaces.additional_operations]
(≪) [notation, in interfaces.additional_operations]
(≫) [notation, in interfaces.additional_operations]
(◎ _ ) [notation, in interfaces.canonical_names]
(◎) [notation, in interfaces.canonical_names]
(⪥ _ ) [notation, in interfaces.canonical_names]
(⪥) [notation, in interfaces.canonical_names]
(· _ ) [notation, in interfaces.vectorspace]
(·) [notation, in interfaces.vectorspace]
- 3 [notation, in interfaces.canonical_names]
- 2 [notation, in interfaces.canonical_names]
- _ [notation, in interfaces.canonical_names]
- 1 [notation, in interfaces.canonical_names]
- 4 [notation, in interfaces.canonical_names]
/ _ [notation, in interfaces.canonical_names]
// _ [notation, in interfaces.canonical_names]
0 [notation, in interfaces.canonical_names]
1 [notation, in interfaces.canonical_names]
2 [notation, in interfaces.canonical_names]
3 [notation, in interfaces.canonical_names]
4 [notation, in interfaces.canonical_names]
Φ [abbreviation, in theory.ua_congruence]
ηAdjunction [record, in theory.categories]
ηAdjunction_φAdjunction [instance, in theory.adjunctions]
η_adjunction_natural [projection, in theory.categories]
η_adjunction_right_functor [projection, in theory.categories]
η_natural [instance, in theory.adjunctions]
η_adjunction_left_functor [projection, in theory.categories]
η_adjunction_universal [projection, in theory.categories]
ηεAdjunction [record, in theory.categories]
ηεAdjunction_ηAdjunction [instance, in theory.adjunctions]
ηεAdjunction_φAdjunction [instance, in theory.adjunctions]
ηε_adjunction_ε_natural [projection, in theory.categories]
ηε_adjunction_right_functor [projection, in theory.categories]
ηε_adjunction_η_natural [projection, in theory.categories]
ηε_adjunction_identity_at_F [projection, in theory.categories]
ηε_adjunction_identity_at_G [projection, in theory.categories]
ηε_adjunction_left_functor [projection, in theory.categories]
φAdjunction [record, in theory.categories]
φAdjunction_ηεAdjunction [instance, in theory.adjunctions]
φAdjunction_ηAdjunction [instance, in theory.adjunctions]
φ_adjunction_left_functor [projection, in theory.categories]
φ_adjunction_natural_left_inv [lemma, in theory.adjunctions]
φ_adjunction_bijective [projection, in theory.categories]
φ_adjunction_right_functor [projection, in theory.categories]
φ_in_terms_of_ε [lemma, in theory.adjunctions]
φ_adjunction_natural_left [projection, in theory.categories]
φ_adjunction_natural_right_inv [lemma, in theory.adjunctions]
φ_in_terms_of_η [lemma, in theory.adjunctions]
φ_adjunction_natural_right [projection, in theory.categories]



Instance Index

A

abs_proper [in theory.abs]
alt_to_frac [in theory.rationals]
apart_proper [in orders.orders]
apart_0_sig_apart_0 [in theory.fields]
apart_proper [in theory.strong_setoids]
apart_0_2 [in orders.semirings]
apart_ne [in theory.strong_setoids]
app_proper [in implementations.cons_list]
app_assoc_inst [in implementations.cons_list]
app_tree_proper [in varieties.closed_terms]
app_tree_proper [in varieties.open_terms]


B

bigQ_Zshiftl [in implementations.fast_rationals]
bigQ_shiftl [in implementations.fast_rationals]
bigZ_pow [in implementations.fast_integers]
biinduction [in orders.integers]
biinduction [in theory.naturals]
binary_strong_morphism_proper [in theory.strong_setoids]
bind_proper [in implementations.cons_list]


C

cat [in categories.dual]
co [in theory.ua_congruence]
comp [in categories.algebras]
compose_homomorphisms [in theory.ua_homomorphisms]
compose_transformation [in categories.functors]
compose_order_preserving_back [in orders.maps]
compose_order_morphism [in orders.maps]
compose_morphisms [in varieties.semigroups]
compose_functors [in interfaces.functors]
compose_semiring_morphisms [in theory.rings]
compose_order_embedding [in orders.maps]
compose_morphisms [in theory.setoids]
compose_order_preserving [in orders.maps]
compose_morphisms [in varieties.monoids]
comp_Fmap [in interfaces.functors]
concat_proper [in implementations.cons_list]
congruence [in theory.ring_ideals]
cong_proper [in theory.ring_ideals]
cut_minus_proper [in theory.cut_minus]


D

decode_variety_and_ops [in varieties.semirings]
decode_variety_and_ops [in varieties.monoids]
decode_variety_and_ops [in varieties.groups]
decode_variety_and_ops [in varieties.setoids]
decode_variety_and_ops [in varieties.rings]
decode_variety_and_ops [in varieties.semigroups]
dec_mult_inv_ne_0 [in theory.dec_fields]
dec_full_pseudo_order [in orders.orders]
dec_from_lt_dec [in orders.orders]
dec_field_to_domain_inj [in theory.dec_fields]
dec_pseudo_srorder [in orders.semirings]
dec_strictly_order_preserving_back_mor [in orders.maps]
dec_strict_partial_order [in orders.orders]
dec_order [in orders.orders]
dec_pseudo_order [in orders.orders]
dec_strong_binary_morphism [in theory.strong_setoids]
dec_strictly_order_preserving_inj [in orders.maps]
dec_strong_setoid [in theory.strong_setoids]
dec_strong_injective [in theory.strong_setoids]
dec_full_pseudo_srorder [in orders.semirings]
dec_mult_inv_inj [in theory.dec_fields]
dec_strong_morphism [in theory.strong_setoids]
default_cut_minus [in theory.cut_minus]
default_nat_pow [in theory.nat_pow]
default_shiftl_int [in theory.shiftl]
default_shiftl [in theory.shiftl]
default_abs [in theory.abs]
default_apart [in theory.strong_setoids]
default_apart_trivial [in theory.strong_setoids]
dnn_Str_nth_tl [in theory.series]
dnn_tl [in theory.series]
dyadic_proper [in implementations.dyadics]
dy_shiftl [in implementations.dyadics]
dy_equiv [in implementations.dyadics]
dy_mult [in implementations.dyadics]
dy_inject [in implementations.dyadics]
dy_opp [in implementations.dyadics]
dy_pow [in implementations.dyadics]
dy_pow_spec [in implementations.dyadics]
dy_le_dec [in implementations.dyadics]
dy_abs [in implementations.dyadics]
dy_le [in implementations.dyadics]
dy_1 [in implementations.dyadics]
dy_eq_dec [in implementations.dyadics]
dy_0 [in implementations.dyadics]
dy_plus [in implementations.dyadics]
dy_lt [in implementations.dyadics]


E

e [in categories.categories]
e [in categories.dual]
e [in categories.JMcat]
e [in categories.functors]
encode_algebra_and_ops [in varieties.rings]
encode_operations [in varieties.monoids]
encode_algebra_and_ops [in varieties.groups]
encode_variety_and_ops [in varieties.semigroups]
encode_operations [in varieties.groups]
encode_variety_and_ops [in varieties.rings]
encode_variety_and_ops [in varieties.monoids]
encode_operations [in varieties.semigroups]
encode_algebra_and_ops [in varieties.monoids]
encode_operations [in varieties.rings]
encode_algebra_and_ops [in varieties.semigroups]
encode_variety_and_ops [in varieties.groups]
equivalence_proper [in misc.workarounds]
equiv_default_relation [in interfaces.canonical_names]
eval_proper [in interfaces.universal_algebra]
eval_stmt_proper [in interfaces.universal_algebra]
eval_strong_proper [in interfaces.universal_algebra]
EventuallyForAll_proper [in theory.streams]
everyOther_dnn [in theory.series]
everyOther_inc [in theory.series]
ext_equiv_trans [in theory.setoids]
ext_equiv_sym [in theory.setoids]


F

fastZ_shiftl [in implementations.fast_integers]
flipA [in categories.dual]
fold_mor [in interfaces.sequences]
ForAllIf_proper [in theory.streams]
ForAll_proper [in theory.streams]
forget [in theory.forget_algebra]
Frac_dec_mult_inv [in implementations.field_of_fractions]
Frac_plus [in implementations.field_of_fractions]
Frac_mult [in implementations.field_of_fractions]
Frac_dec [in implementations.field_of_fractions]
Frac_0 [in implementations.field_of_fractions]
Frac_1 [in implementations.field_of_fractions]
Frac_opp [in implementations.field_of_fractions]
Frac_equiv [in implementations.field_of_fractions]
Frac_inject [in implementations.field_of_fractions]


H

heq_proper [in theory.ua_subvariety]


I

id_homomorphism [in theory.ua_homomorphisms]
id_morphism [in theory.setoids]
id_order_preserving [in orders.maps]
id_order_morphism [in orders.maps]
id_order_preserving_back [in orders.maps]
id_functor [in interfaces.functors]
id_transformation [in categories.functors]
id_semiring_morphism [in theory.rings]
id_morphism [in varieties.monoids]
id_morphism [in varieties.semigroups]
id_injective [in theory.jections]
impl [in theory.ua_subalgebraT]
impl [in theory.ua_subalgebra]
implementation [in varieties.semirings]
implementation [in varieties.empty]
injective_ne_0 [in theory.rings]
Injective_proper [in theory.jections]
injective_nats [in theory.rationals]
inject_nat_N [in implementations.stdlib_binary_naturals]
inject_bigN_bigQ [in implementations.fast_rationals]
inject_Z_bigQ [in implementations.fast_rationals]
inject_fastN_fastZ [in implementations.fast_integers]
inject_N_nat [in implementations.stdlib_binary_naturals]
inject_bigQ_frac_bigZ [in implementations.fast_rationals]
inject_nat_Z [in implementations.stdlib_binary_integers]
inject_bigZ_bigQ [in implementations.fast_rationals]
inject_N_Z [in implementations.stdlib_binary_integers]
inject_Z_Q [in implementations.stdlib_rationals]
inn_Str_nth_tl [in theory.series]
inn_tl [in theory.series]
intdom_nontrivial_apart [in theory.rings]
integers_to_integers_injective [in theory.integers]
integers_to_rationals_injective [in theory.rationals]
integer_initial_arrow [in interfaces.integers]
int_abs_proper [in theory.int_abs]
int_pow_base_1 [in theory.int_pow]
int_le [in orders.integers]
int_lt [in orders.integers]
int_pow_1 [in theory.int_pow]
int_pow_exp_lt_back [in theory.int_pow]
int_pow_inj [in theory.int_pow]
int_pow_pos [in theory.int_pow]
int_pow_ne_0 [in theory.int_pow]
int_pow_default [in theory.int_pow]
int_pow_nonneg [in theory.int_pow]
int_pow_exp_lt [in theory.int_pow]
int_pow_exp_le [in theory.int_pow]
int_pow_exp_le_back [in theory.int_pow]
in_domain_equivalence [in theory.ua_congruence]
iso_to_frac [in theory.rationals]
iso_equivalence [in theory.categories]
iso_setoid [in theory.categories]


L

le_0_4 [in orders.semirings]
le_total [in orders.orders]
le_0_1 [in orders.semirings]
le_0_3 [in orders.semirings]
le_0_2 [in orders.semirings]
lifted_e_proper [in theory.ua_congruence]
liftM [in theory.monads]
list_eq [in implementations.cons_list]
lookup_right [in theory.quote_monoid]
lookup_left [in theory.quote_monoid]
lt_0_4 [in orders.semirings]
lt_0_1 [in orders.semirings]
lt_trichotomy [in orders.orders]
lt_0_3 [in orders.semirings]
lt_0_2 [in orders.semirings]


M

map_op_proper [in theory.ua_mapped_operations]
map_proper [in theory.streams]
max_proper [in orders.minmax]
max_commutative [in orders.minmax]
max_associative [in orders.minmax]
Me [in theory.ua_term_monad]
min_associative [in orders.minmax]
min_commutative [in orders.minmax]
min_proper [in orders.minmax]
mono [in categories.setoids]
mono [in categories.product]
mono [in theory.forget_algebra]
monoid_morphism_proper [in theory.groups]
morphism_order_preserving [in orders.rationals]
morphism_order_preserving [in orders.naturals]
morphism_proper [in theory.setoids]
morphism_order_preserving [in orders.integers]
mult_0_l [in theory.rings]
mult_0_r [in theory.rings]
mult_inv_apart_zero [in theory.fields]
mult_ne_0 [in theory.rings]
mult_1_r [in theory.rings]
mult_inv_dec_field [in theory.dec_fields]
mult_1_l [in theory.rings]
mult_Streams_inc [in theory.series]
mult_Streams_dnn [in theory.series]
mult_apart_zero [in theory.fields]


N

natdistancecut_minus [in theory.nat_distance]
natdistance_default [in theory.nat_distance]
naturals_to_integers_injective [in theory.integers]
naturals_to_naturals_injective [in theory.naturals]
nat_le [in implementations.peano_naturals]
nat_plus [in implementations.peano_naturals]
nat_mult [in implementations.peano_naturals]
nat_nontrivial_apart [in theory.naturals]
nat_0 [in implementations.peano_naturals]
nat_pow_base_1 [in theory.nat_pow]
nat_nontrivial [in theory.naturals]
nat_pow_nonneg [in theory.nat_pow]
nat_lt [in implementations.peano_naturals]
nat_lt [in orders.naturals]
nat_cut_minus [in implementations.peano_naturals]
nat_pow_peano [in theory.nat_pow]
nat_dec [in implementations.peano_naturals]
nat_pow_ne_0 [in theory.nat_pow]
nat_equiv [in implementations.peano_naturals]
nat_distance_proper [in theory.nat_distance]
nat_le [in orders.naturals]
nat_le_dec [in implementations.peano_naturals]
nat_pow_pos [in theory.nat_pow]
nat_pow_apart_0 [in theory.nat_pow]
nat_pow_1 [in theory.nat_pow]
nat_1 [in implementations.peano_naturals]
ne_apart [in theory.strong_setoids]
NonNeg_lt [in implementations.nonneg_semiring_elements]
NonNeg_equiv_dec [in implementations.nonneg_semiring_elements]
NonNeg_le [in implementations.nonneg_semiring_elements]
NonNeg_0 [in implementations.nonneg_semiring_elements]
NonNeg_mult [in implementations.nonneg_semiring_elements]
NonNeg_plus [in implementations.nonneg_semiring_elements]
NonNeg_1 [in implementations.nonneg_semiring_elements]
NonNeg_inject [in implementations.nonneg_semiring_elements]
NonNeg_trivial_apart [in implementations.nonneg_semiring_elements]
NonNeg_le_dec [in implementations.nonneg_semiring_elements]
NonNeg_apart_dec [in implementations.nonneg_semiring_elements]
nonneg_dec_mult_inv_compat [in orders.dec_fields]
nonneg_plus_compat [in orders.semirings]
NonZero_mult [in implementations.nonzero_field_elements]
NonZero_1 [in implementations.nonzero_field_elements]
nqe_proper [in theory.ua_products]
NType_Integers.inject_NType_N [in implementations.NType_naturals]
NType_Integers.NType_lt [in implementations.NType_naturals]
NType_Integers.NType_le [in implementations.NType_naturals]
NType_Integers.NType_shiftl [in implementations.NType_naturals]
NType_Integers.inject_NType_Z [in implementations.NType_naturals]
NType_Integers.NType_1 [in implementations.NType_naturals]
NType_Integers.NType_equiv [in implementations.NType_naturals]
NType_Integers.NType_plus [in implementations.NType_naturals]
NType_Integers.NType_0 [in implementations.NType_naturals]
NType_Integers.NType_mult [in implementations.NType_naturals]
NType_Integers.inject_N_NType [in implementations.NType_naturals]
NType_Integers.NType_pow [in implementations.NType_naturals]
N_0 [in implementations.stdlib_binary_naturals]
N_1 [in implementations.stdlib_binary_naturals]
N_mult [in implementations.stdlib_binary_naturals]
N_le [in implementations.stdlib_binary_naturals]
N_plus [in implementations.stdlib_binary_naturals]
N_equiv [in implementations.stdlib_binary_naturals]
N_lt [in implementations.stdlib_binary_naturals]


O

obvious_sum_dst_l [in misc.util]
obvious_sum_src [in misc.util]
obvious_sum_dst_r [in misc.util]
op_closed_proper [in theory.ua_subalgebra]
order_preserving_back_proper [in orders.maps]
order_morphism_proper [in orders.maps]
order_embedding_proper [in orders.maps]
order_preserving_proper [in orders.maps]


P

pa [in categories.product]
pair_proper [in theory.setoids]
pdr_equiv [in misc.util]
plus_0_l [in theory.rings]
plus_0_r [in theory.rings]
poly_eq [in implementations.polynomials]
poly_one [in implementations.polynomials]
poly_zero [in implementations.polynomials]
posh_fmap [in interfaces.sequences]
Pos_shiftl [in implementations.positive_semiring_elements]
pos_plus_compat [in orders.semirings]
Pos_plus [in implementations.positive_semiring_elements]
Pos_inject [in implementations.positive_semiring_elements]
Pos_mult [in implementations.positive_semiring_elements]
Pos_1 [in implementations.positive_semiring_elements]
Pos_int_pow [in implementations.positive_semiring_elements]
pos_dec_mult_inv_compat [in orders.dec_fields]
powers_help_proper [in theory.series]
powers_proper [in theory.series]
prep_proper [in varieties.closed_terms]
Preservation_proper'' [in theory.ua_homomorphisms]
Preservation_proper [in theory.ua_homomorphisms]
preserves_pos [in orders.semirings]
preserves_nonneg [in orders.semirings]
product_e [in theory.ua_products]
product_algebra [in theory.ua_products]
product_equiv [in theory.setoids]
product_ops [in theory.ua_products]
product_variety [in theory.ua_products]
projection_morphism [in theory.setoids]
pseudo_order_embedding_ext [in orders.maps]


Q

QType_Rationals.QType_Zpow [in implementations.QType_rationals]
QType_Rationals.QType_0 [in implementations.QType_rationals]
QType_Rationals.QType_equiv [in implementations.QType_rationals]
QType_Rationals.QType_dec_mult_inv [in implementations.QType_rationals]
QType_Rationals.QType_lt [in implementations.QType_rationals]
QType_Rationals.inject_Q_QType [in implementations.QType_rationals]
QType_Rationals.QType_Npow [in implementations.QType_rationals]
QType_Rationals.QType_plus [in implementations.QType_rationals]
QType_Rationals.QType_1 [in implementations.QType_rationals]
QType_Rationals.QType_opp [in implementations.QType_rationals]
QType_Rationals.inject_QType_Q [in implementations.QType_rationals]
QType_Rationals.QType_le [in implementations.QType_rationals]
QType_Rationals.QType_mult [in implementations.QType_rationals]
quote_zero [in theory.quote_monoid]
quote_mult [in theory.quote_monoid]
quote_new_var [in theory.quote_monoid]
quote_old_var [in theory.quote_monoid]
Q_0 [in implementations.stdlib_rationals]
Q_opp [in implementations.stdlib_rationals]
Q_pow [in implementations.stdlib_rationals]
Q_shiftl [in implementations.stdlib_rationals]
Q_to_fracZ [in implementations.stdlib_rationals]
Q_lt [in implementations.stdlib_rationals]
Q_1 [in implementations.stdlib_rationals]
Q_le [in implementations.stdlib_rationals]
Q_plus [in implementations.stdlib_rationals]
Q_mult [in implementations.stdlib_rationals]
Q_mult_inv [in implementations.stdlib_rationals]
Q_eq [in implementations.stdlib_rationals]
Q_Npow [in implementations.stdlib_rationals]


R

rationals_lt [in orders.rationals]
rationals_le [in orders.rationals]
rec_impl_proper [in theory.ua_products]
ret_proper [in implementations.cons_list]
ringmult_is_semigroupop [in interfaces.canonical_names]
ringone_is_monoidunit [in interfaces.canonical_names]
ringplus_is_semigroupop [in interfaces.canonical_names]
ringzero_is_monoidunit [in interfaces.canonical_names]
Ring_Semi [in theory.rings]
ring_mult_left_cancel [in theory.rings]


S

semigroup_morphism_proper [in theory.groups]
semiring_morphism_proper [in theory.rings]
shiftl_inj [in theory.shiftl]
shiftl_nonneg [in theory.shiftl]
shiftl_base_0 [in theory.shiftl]
shiftl_ne_0 [in theory.shiftl]
shiftl_pos [in theory.shiftl]
shiftl_strong_inj [in theory.shiftl]
sigT_Setoid [in theory.setoids]
sig_type_trans [in interfaces.ua_basic]
sig_type_sym [in interfaces.ua_basic]
sig_Setoid [in theory.setoids]
sig_type_trans' [in interfaces.ua_basic]
sig_strong_setoid [in theory.strong_setoids]
simpleZ_abs [in implementations.natpair_integers]
slow_int_abs [in theory.int_abs]
slow_nat_le_dec [in orders.naturals]
slow_rat_dec [in theory.rationals]
sort_proper [in orders.minmax]
SRpair_lt [in implementations.semiring_pairs]
SRpair_0 [in implementations.semiring_pairs]
SRpair_le [in implementations.semiring_pairs]
SRpair_equiv [in implementations.semiring_pairs]
SRpair_opp [in implementations.semiring_pairs]
SRpair_plus [in implementations.semiring_pairs]
SRpair_trivial_apart [in implementations.semiring_pairs]
SRpair_1 [in implementations.semiring_pairs]
SRpair_dec [in implementations.semiring_pairs]
SRpair_apart [in implementations.semiring_pairs]
SRpair_mult [in implementations.semiring_pairs]
SRpair_le_dec [in implementations.semiring_pairs]
SRpair_inject [in implementations.semiring_pairs]
stream_eq [in theory.streams]
strictly_order_preserving_back_mor [in orders.maps]
strictly_order_preserving_inj [in orders.maps]
strict_po_apart_ne [in orders.orders]
strong_setoid_morphism_1 [in theory.strong_setoids]
strong_setoid_morphism_unary_2 [in theory.strong_setoids]
strong_left_cancellation_cancel [in theory.rings]
strong_right_cancellation_cancel [in theory.rings]
strong_morphism_proper [in theory.strong_setoids]
strong_injective_injective [in theory.strong_setoids]
structural_eq_refl [in varieties.open_terms]
structural_eq_refl [in varieties.closed_terms]
subalgebra [in theory.ua_subalgebra]
subalgebra [in theory.ua_subalgebraT]
Surjective_proper [in theory.jections]


T

to_frac_inverse [in theory.rationals]
to_nat [in implementations.nonneg_integers_naturals]


U

ua_vars_equiv [in interfaces.universal_algebra]
uniwit [in theory.adjunctions]


V

variety [in varieties.empty]
variety [in varieties.semirings]


W

with_vars.quote_old_var [in quote.classquote]
with_vars.obvious_sum_dst_l [in quote.classquote]
with_vars.quote_mult [in quote.classquote]
with_vars.obvious_sum_src [in quote.classquote]
with_vars.lookup_right [in quote.classquote]
with_vars.obvious_sum_dst_r [in quote.classquote]
with_vars.quote_zero [in quote.classquote]
with_vars.lookup_left [in quote.classquote]
with_vars.eval_proper [in quote.classquote]
with_vars.quote_new_var [in quote.classquote]


Z

zero_product_no_zero_divisors [in interfaces.canonical_names]
zero_product [in theory.integers]
zipWith_proper [in theory.streams]
ZPos_cut_minus [in implementations.nonneg_integers_naturals]
ZPos_to_nat_sr_morphism [in implementations.nonneg_integers_naturals]
ZType_Integers.ZType_Npow [in implementations.ZType_integers]
ZType_Integers.ZType_1 [in implementations.ZType_integers]
ZType_Integers.ZType_equiv [in implementations.ZType_integers]
ZType_Integers.ZType_plus [in implementations.ZType_integers]
ZType_Integers.ZType_pow [in implementations.ZType_integers]
ZType_Integers.ZType_shiftl [in implementations.ZType_integers]
ZType_Integers.ZType_0 [in implementations.ZType_integers]
ZType_Integers.ZType_div [in implementations.ZType_integers]
ZType_Integers.ZType_mult [in implementations.ZType_integers]
ZType_Integers.inject_ZType_Z [in implementations.ZType_integers]
ZType_Integers.ZType_opp [in implementations.ZType_integers]
ZType_Integers.ZType_le [in implementations.ZType_integers]
ZType_Integers.ZType_mod [in implementations.ZType_integers]
ZType_Integers.ZType_lt [in implementations.ZType_integers]
ZType_Integers.inject_Z_ZType [in implementations.ZType_integers]
Z_le [in implementations.stdlib_binary_integers]
Z_0 [in implementations.stdlib_binary_integers]
Z_plus [in implementations.stdlib_binary_integers]
Z_shiftl [in implementations.stdlib_binary_integers]
Z_1 [in implementations.stdlib_binary_integers]
Z_Npow [in implementations.stdlib_binary_integers]
z_to_ring [in implementations.natpair_integers]
Z_to_Npair [in implementations.stdlib_binary_integers]
Z_lt [in implementations.stdlib_binary_integers]
Z_opp [in implementations.stdlib_binary_integers]
Z_mult [in implementations.stdlib_binary_integers]
Z_Nshiftl [in implementations.stdlib_binary_integers]
Z_pow [in implementations.stdlib_binary_integers]
Z_equiv [in implementations.stdlib_binary_integers]


other

ηAdjunction_φAdjunction [in theory.adjunctions]
η_natural [in theory.adjunctions]
ηεAdjunction_ηAdjunction [in theory.adjunctions]
ηεAdjunction_φAdjunction [in theory.adjunctions]
φAdjunction_ηεAdjunction [in theory.adjunctions]
φAdjunction_ηAdjunction [in theory.adjunctions]



Projection Index

A

abgroup_commutative [in interfaces.abstract_algebra]
abgroup_group [in interfaces.abstract_algebra]
abs_sig [in interfaces.canonical_names]
algebra_proof [in categories.algebras]
algebra_equiv [in categories.algebras]
algebra_setoids [in interfaces.ua_basic]
algebra_op [in interfaces.ua_basic]
algebra_propers [in interfaces.ua_basic]
algebra_ops [in categories.algebras]
algebra_carriers [in categories.algebras]
antisymmetry [in interfaces.canonical_names]
apart [in interfaces.canonical_names]
apart_iff_total_lt [in interfaces.orders]
Arrow [in interfaces.canonical_names]
Arrows_inst [in categories.categories]
Arrows_inst [in categories.JMcat]
arrow_equiv [in interfaces.abstract_algebra]
associativity [in interfaces.canonical_names]


B

bad.naturals_initial [in interfaces.naturals]
biinduction [in interfaces.canonical_names]
bijective_surjective [in interfaces.abstract_algebra]
bijective_injective [in interfaces.abstract_algebra]
bind [in interfaces.monads]
bind_proper [in interfaces.monads]


C

CatComp_inst [in categories.categories]
CatComp_inst [in categories.JMcat]
Category_inst [in categories.JMcat]
Category_inst [in categories.categories]
CatId_inst [in categories.JMcat]
CatId_inst [in categories.categories]
cat_id [in interfaces.canonical_names]
coerce [in interfaces.canonical_names]
commonoid_commutative [in interfaces.abstract_algebra]
commonoid_mon [in interfaces.abstract_algebra]
commutativity [in interfaces.canonical_names]
comp [in interfaces.canonical_names]
comp_proper [in interfaces.abstract_algebra]
comp_assoc [in interfaces.abstract_algebra]
congruence_quotient [in theory.ua_congruence]
congruence_proper [in theory.ua_congruence]
cotransitive [in interfaces.canonical_names]
cut_minus_le [in interfaces.additional_operations]
cut_minus [in interfaces.additional_operations]
cut_minus_0 [in interfaces.additional_operations]


D

decfield_ring [in interfaces.abstract_algebra]
decfield_nontrivial [in interfaces.abstract_algebra]
decide [in interfaces.canonical_names]
decreasing_nonneg [in theory.series]
dec_mult_inv_0 [in interfaces.abstract_algebra]
dec_mult_inverse [in interfaces.abstract_algebra]
dec_mult_inv [in interfaces.canonical_names]
dec_mult_inv_proper [in interfaces.abstract_algebra]
den [in implementations.field_of_fractions]
den_ne_0 [in implementations.field_of_fractions]
distribute_l [in interfaces.canonical_names]
distribute_r [in interfaces.canonical_names]
div_mod [in interfaces.additional_operations]
div_euclid_proper [in interfaces.additional_operations]
div_euclid [in interfaces.additional_operations]
div_euclid_0 [in interfaces.additional_operations]


E

e [in categories.setoids]
entailment_premises [in interfaces.universal_algebra]
entailment_conclusion [in interfaces.universal_algebra]
equiv [in interfaces.canonical_names]
Equiv_inst [in categories.JMcat]
Equiv_inst [in categories.categories]
eta [in categories.functors]
et_sig [in interfaces.universal_algebra]
et_laws [in interfaces.universal_algebra]
eval_quote [in theory.quote_monoid]
expo [in implementations.dyadics]
extend [in interfaces.sequences]
extend_morphism [in interfaces.sequences]


F

field_plus_ext [in interfaces.abstract_algebra]
field_mult_ext [in interfaces.abstract_algebra]
field_strongsetoid [in interfaces.abstract_algebra]
field_ring [in interfaces.abstract_algebra]
field_nontrivial [in interfaces.abstract_algebra]
fmap [in interfaces.functors]
Fmap_inst [in categories.categories]
Fmap_inst [in categories.functors]
Fmap_inst [in categories.JMcat]
full_pseudo_srorder_pso [in interfaces.orders]
full_pseudo_srorder_le_iff_not_lt_flip [in interfaces.orders]
full_pseudo_order_pseudo [in interfaces.orders]
Functor_inst [in categories.JMcat]
functor_from [in interfaces.functors]
Functor_inst [in categories.functors]
functor_morphism [in interfaces.functors]
Functor_inst [in categories.categories]
functor_to [in interfaces.functors]


G

ginv_r [in interfaces.abstract_algebra]
ginv_l [in interfaces.abstract_algebra]
group_inv [in interfaces.canonical_names]
group_monoid [in interfaces.abstract_algebra]


H

hetero_symmetric [in interfaces.canonical_names]
homo_proper [in theory.ua_homomorphisms]
homo_target_algebra [in theory.ua_homomorphisms]
homo_source_algebra [in theory.ua_homomorphisms]


I

Ideal_NonEmpty [in theory.ring_ideals]
Ideal_closed_plus_opp [in theory.ring_ideals]
Ideal_closed_mult_r [in theory.ring_ideals]
Ideal_closed_mult_l [in theory.ring_ideals]
id_r [in interfaces.abstract_algebra]
id_l [in interfaces.abstract_algebra]
increasing_nonneg [in theory.series]
initial_arrow_unique [in theory.categories]
initial_arrow [in theory.categories]
inject [in interfaces.sequences]
injective [in interfaces.abstract_algebra]
injective_mor [in interfaces.abstract_algebra]
intdom_ring [in interfaces.abstract_algebra]
intdom_nontrivial [in interfaces.abstract_algebra]
intdom_nozeroes [in interfaces.abstract_algebra]
integers_to_ring_mor [in interfaces.integers]
integers_to_ring [in interfaces.integers]
integers_initial [in interfaces.integers]
integers_ring [in interfaces.integers]
int_as_nat [in interfaces.integers]
int_pow_S [in interfaces.additional_operations]
int_pow_base_0 [in interfaces.additional_operations]
int_pow_proper [in interfaces.additional_operations]
int_abs_sig [in interfaces.integers]
int_pow_0 [in interfaces.additional_operations]
inverse [in interfaces.canonical_names]
inv_proper [in interfaces.abstract_algebra]


L

le [in interfaces.canonical_names]
left_inverse [in interfaces.canonical_names]
left_identity [in interfaces.canonical_names]
left_absorb [in interfaces.canonical_names]
left_cancellation [in interfaces.abstract_algebra]
le_iff_not_lt_flip [in interfaces.orders]
lookup [in theory.quote_monoid]
lookup_correct [in theory.quote_monoid]
lt [in interfaces.canonical_names]
lt_iff_le_apart [in interfaces.orders]


M

makes_products [in theory.categories]
make_tuple [in theory.categories]
mant [in implementations.dyadics]
map_obj [in categories.JMcat]
map_obj [in categories.categories]
map_obj [in categories.functors]
mod_euclid_proper [in interfaces.additional_operations]
mod_euclid [in interfaces.additional_operations]
mod_euclid_rem [in interfaces.additional_operations]
mod_euclid_0 [in interfaces.additional_operations]
monmor_a [in interfaces.abstract_algebra]
monmor_sgmor [in interfaces.abstract_algebra]
monmor_b [in interfaces.abstract_algebra]
mono [in theory.categories]
monoid_left_id [in interfaces.abstract_algebra]
monoid_semigroup [in interfaces.abstract_algebra]
monoid_right_id [in interfaces.abstract_algebra]
mon_runit [in interfaces.monads]
mon_unit [in interfaces.canonical_names]
mon_lunit [in interfaces.monads]
mon_assoc [in interfaces.monads]
mon_setoid [in interfaces.monads]
mult_inv [in interfaces.canonical_names]
mult_inv_proper [in interfaces.abstract_algebra]
mult_inverse [in interfaces.abstract_algebra]


N

natural [in theory.categories]
naturals_to_semiring [in interfaces.naturals]
naturals_initial [in interfaces.naturals]
naturals_ring [in interfaces.naturals]
naturals_to_semiring_mor [in interfaces.naturals]
NaturalTransformation_inst [in categories.functors]
nat_pow_S [in interfaces.additional_operations]
nat_distance_sig [in interfaces.naturals]
nat_pow_proper [in interfaces.additional_operations]
nat_pow_0 [in interfaces.additional_operations]
neg [in implementations.semiring_pairs]
nonneg_mult_compat [in interfaces.orders]
non_empty [in misc.util]
no_zero_divisors [in interfaces.canonical_names]
num [in implementations.field_of_fractions]


O

obj [in categories.JMcat]
obj [in categories.categories]
obvious [in misc.util]
operation [in interfaces.ua_basic]
operation_type [in interfaces.ua_basic]
order_morphism_mor [in interfaces.orders]
order_iso_surjective [in interfaces.orders]
order_embedding_back [in interfaces.orders]
order_preserving_back_morphism [in interfaces.orders]
order_morphism_proper_b [in interfaces.orders]
order_embedding_preserving [in interfaces.orders]
order_preserving_morphism [in interfaces.orders]
order_preserving [in interfaces.orders]
order_preserving_back [in interfaces.orders]
order_iso_embedding [in interfaces.orders]
order_morphism_proper_a [in interfaces.orders]


P

pos [in implementations.semiring_pairs]
pos_mult_compat [in interfaces.orders]
pow [in interfaces.additional_operations]
po_proper [in interfaces.orders]
po_preorder [in interfaces.orders]
po_setoid [in interfaces.orders]
po_antisym [in interfaces.orders]
preserves [in theory.ua_homomorphisms]
preserves_comp [in interfaces.functors]
preserves_mon_unit [in interfaces.abstract_algebra]
preserves_sg_op [in interfaces.abstract_algebra]
preserves_id [in interfaces.functors]
product [in theory.categories]
product_factors [in theory.categories]
prop_holds [in misc.util]
pseudo_srorder_partial_minus [in interfaces.orders]
pseudo_srorder_pos_mult_compat [in interfaces.orders]
pseudo_srorder_mult_ext [in interfaces.orders]
pseudo_srorder_strict [in interfaces.orders]
pseudo_srorder_plus [in interfaces.orders]
pseudo_order_cotrans [in interfaces.orders]
pseudo_order_antisym [in interfaces.orders]
pseudo_order_setoid [in interfaces.orders]


Q

quote [in theory.quote_monoid]


R

ralgebra_action [in interfaces.canonical_names]
rationals_to_frac [in interfaces.rationals]
rationals_embed_ints [in interfaces.rationals]
rationals_frac [in interfaces.rationals]
rationals_frac_mor [in interfaces.rationals]
rationals_field [in interfaces.rationals]
ret [in interfaces.monads]
ret_proper [in interfaces.monads]
right_inverse [in interfaces.canonical_names]
right_absorb [in interfaces.canonical_names]
right_identity [in interfaces.canonical_names]
right_cancellation [in interfaces.abstract_algebra]
ring_mult [in interfaces.canonical_names]
ring_monoid [in interfaces.abstract_algebra]
ring_zero [in interfaces.canonical_names]
ring_group [in interfaces.abstract_algebra]
ring_mult_inverse [in interfaces.canonical_names]
ring_dist [in interfaces.abstract_algebra]
ring_plus [in interfaces.canonical_names]
ring_unit_mult_inverse [in interfaces.canonical_names]
ring_one [in interfaces.canonical_names]


S

scalar_mult [in interfaces.vectorspace]
semiringmor_a [in interfaces.abstract_algebra]
semiringmor_plus_mor [in interfaces.abstract_algebra]
semiringmor_b [in interfaces.abstract_algebra]
semiringmor_mult_mor [in interfaces.abstract_algebra]
semiring_plus_monoid [in interfaces.abstract_algebra]
semiring_mult_monoid [in interfaces.abstract_algebra]
semiring_left_absorb [in interfaces.abstract_algebra]
semiring_distr [in interfaces.abstract_algebra]
sequence_extend_makes_morphisms [in interfaces.sequences]
sequence_inject_natural [in interfaces.sequences]
sequence_fmap_id [in interfaces.sequences]
sequence_adjunction [in interfaces.sequences]
sequence_makes_monoids [in interfaces.sequences]
sequence_fmap_proper [in interfaces.sequences]
sequence_fmap_comp [in interfaces.sequences]
sequence_extend_morphism [in interfaces.sequences]
sequence_only_extend_commutes [in interfaces.sequences]
sequence_extend_commutes [in interfaces.sequences]
sequence_inject_morphism [in interfaces.sequences]
sequence_map_morphism [in interfaces.sequences]
setoidmor_a [in interfaces.abstract_algebra]
setoidmor_b [in interfaces.abstract_algebra]
setoid_eq [in interfaces.abstract_algebra]
setoid_proof [in categories.setoids]
sfmap [in interfaces.functors]
sfunctor_comp [in interfaces.functors]
sfunctor_morphism [in interfaces.functors]
sfunctor_makes_morphisms [in interfaces.functors]
sfunctor_makes_setoids [in interfaces.functors]
sfunctor_id [in interfaces.functors]
sgmor_setmor [in interfaces.abstract_algebra]
sgmor_b [in interfaces.abstract_algebra]
sgmor_a [in interfaces.abstract_algebra]
sg_op [in interfaces.canonical_names]
sg_op_proper [in interfaces.abstract_algebra]
sg_setoid [in interfaces.abstract_algebra]
sg_ass [in interfaces.abstract_algebra]
shiftl [in interfaces.additional_operations]
shiftl_S [in interfaces.additional_operations]
shiftl_0 [in interfaces.additional_operations]
shiftl_proper [in interfaces.additional_operations]
shiftr [in interfaces.additional_operations]
shiftr_proper [in interfaces.additional_operations]
shiftr_0 [in interfaces.additional_operations]
shiftr_S [in interfaces.additional_operations]
simple_distribute_r [in interfaces.canonical_names]
simple_associativity [in interfaces.canonical_names]
simple_distribute_l [in interfaces.canonical_names]
simple.approach_A.quote [in quote.classquote]
simple.approach_B.quote [in quote.classquote]
simple.approach_B.eval_quote [in quote.classquote]
sm_proper [in interfaces.abstract_algebra]
sorts [in interfaces.ua_basic]
srorder_partial_minus [in interfaces.orders]
srorder_plus [in interfaces.orders]
srorder_po [in interfaces.orders]
stable [in misc.util]
strictly_order_preserving_morphism [in interfaces.orders]
strictly_order_preserving_back [in interfaces.orders]
strictly_order_preserving_back_morphism [in interfaces.orders]
strictly_order_preserving [in interfaces.orders]
strict_po_po [in interfaces.orders]
strict_order_morphism_proper_a [in interfaces.orders]
strict_srorder_partial_minus [in interfaces.orders]
strict_srorder_so [in interfaces.orders]
strict_order_embedding_preserving [in interfaces.orders]
strict_order_embedding_back [in interfaces.orders]
strict_srorder_plus [in interfaces.orders]
strict_order_morphism_mor [in interfaces.orders]
strict_po_setoid [in interfaces.orders]
strict_order_morphism_proper_b [in interfaces.orders]
strict_po_trans [in interfaces.orders]
strict_setoid_order_setoid [in interfaces.orders]
strict_setoid_order_proper [in interfaces.orders]
strict_setoid_order_strict [in interfaces.orders]
strong_setoid_irreflexive [in interfaces.abstract_algebra]
strong_binary_setoidmor_c [in interfaces.abstract_algebra]
strong_semiringmor_sr_mor [in interfaces.abstract_algebra]
strong_extensionality [in interfaces.abstract_algebra]
strong_binary_setoidmor_a [in interfaces.abstract_algebra]
strong_setoid_cotrans [in interfaces.abstract_algebra]
strong_right_cancellation [in interfaces.abstract_algebra]
strong_semiringmor_strong_mor [in interfaces.abstract_algebra]
strong_setoidmor_b [in interfaces.abstract_algebra]
strong_binary_extensionality [in interfaces.abstract_algebra]
strong_left_cancellation [in interfaces.abstract_algebra]
strong_injective [in interfaces.abstract_algebra]
strong_binary_setoidmor_b [in interfaces.abstract_algebra]
strong_setoid_symmetric [in interfaces.abstract_algebra]
strong_setoidmor_a [in interfaces.abstract_algebra]
strong_injective_mor [in interfaces.abstract_algebra]
subset_proper [in theory.ua_subalgebraT]
subset_closed [in theory.ua_subalgebraT]
subset_closed [in theory.ua_subalgebra]
subset_proper [in theory.ua_subalgebra]
surjective [in interfaces.abstract_algebra]
surjective_mor [in interfaces.abstract_algebra]


T

T [in categories.setoids]
tight_apart [in interfaces.abstract_algebra]
total [in interfaces.canonical_names]
trichotomy [in interfaces.canonical_names]
trivial_apart [in interfaces.canonical_names]
tuple_proj [in theory.categories]


U

universal_arrow [in theory.categories]


V

variety_carriers [in categories.varieties]
variety_proof [in categories.varieties]
variety_laws [in interfaces.universal_algebra]
variety_algebra [in interfaces.universal_algebra]
variety_equiv [in categories.varieties]
variety_ops [in categories.varieties]
vs_field [in interfaces.vectorspace]
vs_assoc [in interfaces.vectorspace]
vs_abgroup [in interfaces.vectorspace]
vs_distr_r [in interfaces.vectorspace]
vs_left_identity [in interfaces.vectorspace]
vs_distr_l [in interfaces.vectorspace]


W

with_vars.obvious [in quote.classquote]
with_vars.quote [in quote.classquote]
with_vars.eval_quote [in quote.classquote]
with_vars.lookup [in quote.classquote]
with_vars.lookup_correct [in quote.classquote]


Z

zero_divisor [in interfaces.canonical_names]
zero_product [in interfaces.canonical_names]


other

η_adjunction_natural [in theory.categories]
η_adjunction_right_functor [in theory.categories]
η_adjunction_left_functor [in theory.categories]
η_adjunction_universal [in theory.categories]
ηε_adjunction_ε_natural [in theory.categories]
ηε_adjunction_right_functor [in theory.categories]
ηε_adjunction_η_natural [in theory.categories]
ηε_adjunction_identity_at_F [in theory.categories]
ηε_adjunction_identity_at_G [in theory.categories]
ηε_adjunction_left_functor [in theory.categories]
φ_adjunction_left_functor [in theory.categories]
φ_adjunction_bijective [in theory.categories]
φ_adjunction_right_functor [in theory.categories]
φ_adjunction_natural_left [in theory.categories]
φ_adjunction_natural_right [in theory.categories]



Record Index

A

AbGroup [in interfaces.abstract_algebra]
Abs [in interfaces.canonical_names]
Algebra [in interfaces.ua_basic]
AlgebraOps [in interfaces.ua_basic]
AntiSymmetric [in interfaces.canonical_names]
Apart [in interfaces.canonical_names]
Arrow [in categories.categories]
Arrow [in categories.functors]
Arrow [in categories.JMcat]
Arrows [in interfaces.canonical_names]
Associative [in interfaces.canonical_names]


B

bad.Naturals [in interfaces.naturals]
Biinduction [in interfaces.canonical_names]
Bijective [in interfaces.abstract_algebra]


C

CatComp [in interfaces.canonical_names]
Category [in interfaces.abstract_algebra]
CatId [in interfaces.canonical_names]
ClosedSubset [in theory.ua_subalgebra]
ClosedSubset [in theory.ua_subalgebraT]
Coerce [in interfaces.canonical_names]
Commutative [in interfaces.canonical_names]
CommutativeMonoid [in interfaces.abstract_algebra]
Congruence [in theory.ua_congruence]
CoTransitive [in interfaces.canonical_names]
CutMinus [in interfaces.additional_operations]
CutMinusSpec [in interfaces.additional_operations]


D

DecField [in interfaces.abstract_algebra]
Decision [in interfaces.canonical_names]
DecMultInv [in interfaces.canonical_names]
DecreasingNonNegative [in theory.series]
Distribute [in interfaces.canonical_names]
DivEuclid [in interfaces.additional_operations]
Dyadic [in implementations.dyadics]


E

ElimProduct [in theory.categories]
Entailment [in interfaces.universal_algebra]
EquationalTheory [in interfaces.universal_algebra]
Equiv [in interfaces.canonical_names]
EuclidSpec [in interfaces.additional_operations]
ExtendToSeq [in interfaces.sequences]


F

Field [in interfaces.abstract_algebra]
Fmap [in interfaces.functors]
Frac [in implementations.field_of_fractions]
FullPseudoOrder [in interfaces.orders]
FullPseudoSemiRingOrder [in interfaces.orders]
Functor [in interfaces.functors]


G

Group [in interfaces.abstract_algebra]
GroupInv [in interfaces.canonical_names]


H

HasProducts [in theory.categories]
HeteroAssociative [in interfaces.canonical_names]
HeteroSymmetric [in interfaces.canonical_names]
HomoMorphism [in theory.ua_homomorphisms]


I

Ideal [in theory.ring_ideals]
IncreasingNonNegative [in theory.series]
Initial [in theory.categories]
InitialArrow [in theory.categories]
Injective [in interfaces.abstract_algebra]
InjectToSeq [in interfaces.sequences]
IntAbs [in interfaces.integers]
IntAsNat [in interfaces.integers]
Integers [in interfaces.integers]
IntegersToRing [in interfaces.integers]
IntegralDomain [in interfaces.abstract_algebra]
IntPowSpec [in interfaces.additional_operations]
IntroProduct [in theory.categories]
InVariety [in interfaces.universal_algebra]
Inverse [in interfaces.canonical_names]


L

Le [in interfaces.canonical_names]
LeftAbsorb [in interfaces.canonical_names]
LeftCancellation [in interfaces.abstract_algebra]
LeftHeteroDistribute [in interfaces.canonical_names]
LeftIdentity [in interfaces.canonical_names]
LeftInverse [in interfaces.canonical_names]
Lookup [in theory.quote_monoid]
Lt [in interfaces.canonical_names]


M

ModEuclid [in interfaces.additional_operations]
Monad [in interfaces.monads]
MonadBind [in interfaces.monads]
MonadReturn [in interfaces.monads]
Mono [in theory.categories]
Monoid [in interfaces.abstract_algebra]
MonoidUnit [in interfaces.canonical_names]
Monoid_Morphism [in interfaces.abstract_algebra]
MultInv [in interfaces.canonical_names]


N

NatDistance [in interfaces.naturals]
NatPowSpec [in interfaces.additional_operations]
Naturals [in interfaces.naturals]
NaturalsToSemiRing [in interfaces.naturals]
NaturalTransformation [in theory.categories]
NonEmpty [in misc.util]
NoZeroDivisors [in interfaces.canonical_names]


O

Object [in categories.functors]
Object [in categories.setoids]
Object [in categories.JMcat]
Object [in categories.categories]
Object [in categories.algebras]
Object [in categories.varieties]
Obvious [in misc.util]
OrderEmbedding [in interfaces.orders]
OrderIsomorphism [in interfaces.orders]
OrderPreserving [in interfaces.orders]
OrderPreservingBack [in interfaces.orders]
Order_Morphism [in interfaces.orders]


P

PartialOrder [in interfaces.orders]
PoshSequence [in interfaces.sequences]
Pow [in interfaces.additional_operations]
Producer [in theory.categories]
Product [in theory.categories]
PropHolds [in misc.util]
PseudoOrder [in interfaces.orders]
PseudoSemiRingOrder [in interfaces.orders]


Q

Quote [in theory.quote_monoid]


R

RalgebraAction [in interfaces.canonical_names]
Rationals [in interfaces.rationals]
RationalsToFrac [in interfaces.rationals]
RightAbsorb [in interfaces.canonical_names]
RightCancellation [in interfaces.abstract_algebra]
RightHeteroDistribute [in interfaces.canonical_names]
RightIdentity [in interfaces.canonical_names]
RightInverse [in interfaces.canonical_names]
Ring [in interfaces.abstract_algebra]
RingMult [in interfaces.canonical_names]
RingMultInverse [in interfaces.canonical_names]
RingOne [in interfaces.canonical_names]
RingPlus [in interfaces.canonical_names]
RingUnit [in interfaces.canonical_names]
RingZero [in interfaces.canonical_names]


S

ScalarMult [in interfaces.vectorspace]
SemiGroup [in interfaces.abstract_algebra]
SemiGroupOp [in interfaces.canonical_names]
SemiGroup_Morphism [in interfaces.abstract_algebra]
SemiRing [in interfaces.abstract_algebra]
SemiRingOrder [in interfaces.orders]
SemiRing_Morphism [in interfaces.abstract_algebra]
Sequence [in interfaces.sequences]
Setoid [in interfaces.abstract_algebra]
Setoid_Morphism [in interfaces.abstract_algebra]
SFmap [in interfaces.functors]
SFunctor [in interfaces.functors]
ShiftL [in interfaces.additional_operations]
ShiftLSpec [in interfaces.additional_operations]
ShiftR [in interfaces.additional_operations]
ShiftRSpec [in interfaces.additional_operations]
Signature [in interfaces.ua_basic]
simple.approach_A.Quote [in quote.classquote]
simple.approach_B.Quote [in quote.classquote]
SRpair [in implementations.semiring_pairs]
Stable [in misc.util]
StrictlyOrderPreserving [in interfaces.orders]
StrictlyOrderPreservingBack [in interfaces.orders]
StrictOrderEmbedding [in interfaces.orders]
StrictOrder_Morphism [in interfaces.orders]
StrictPartialOrder [in interfaces.orders]
StrictSemiRingOrder [in interfaces.orders]
StrictSetoidOrder [in interfaces.orders]
StrongInjective [in interfaces.abstract_algebra]
StrongLeftCancellation [in interfaces.abstract_algebra]
StrongRightCancellation [in interfaces.abstract_algebra]
StrongSemiRing_Morphism [in interfaces.abstract_algebra]
StrongSetoid [in interfaces.abstract_algebra]
StrongSetoid_BinaryMorphism [in interfaces.abstract_algebra]
StrongSetoid_Morphism [in interfaces.abstract_algebra]
Surjective [in interfaces.abstract_algebra]


T

TotalRelation [in interfaces.canonical_names]
Trichotomy [in interfaces.canonical_names]
TrivialApart [in interfaces.canonical_names]


U

UniversalArrow [in theory.categories]


V

VectorSpace [in interfaces.vectorspace]


W

with_vars.Quote [in quote.classquote]
with_vars.Lookup [in quote.classquote]
with_vars.Obvious [in quote.classquote]


Z

ZeroDivisor [in interfaces.canonical_names]
ZeroProduct [in interfaces.canonical_names]


other

ηAdjunction [in theory.categories]
ηεAdjunction [in theory.categories]
φAdjunction [in theory.categories]



Lemma Index

A

abs_nonpos_plus [in theory.abs]
abs_nonneg [in theory.abs]
abs_nonneg_plus [in theory.abs]
abs_mult [in theory.abs]
abs_nonpos [in theory.abs]
abs_opp [in theory.abs]
abs_0 [in theory.abs]
abs_1 [in theory.abs]
agree_on_nat [in implementations.natpair_integers]
algebra_projection_morphisms [in theory.ua_products]
alt_Build_Rationals [in theory.rationals]
alt_injective [in theory.jections]
apart_0_proper [in theory.fields]
apart_total_lt [in orders.orders]
applications_rect [in interfaces.universal_algebra]
arrows_between_isomorphic_objects [in theory.categories]
arrow_unique [in varieties.closed_terms]


B

back [in theory.jections]
back_and_forth [in theory.ua_congruence]
between_pos [in orders.rings]
between_nonneg [in orders.rings]
bigQ_div_bigQq [in implementations.fast_rationals]
bigQ_div_bigQq_alt [in implementations.fast_rationals]
biinduction_iff [in misc.util]
bijective_applied [in theory.jections]
bool_decide_rel_true [in misc.util]
bool_decide_true [in misc.util]
bool_decide_false [in misc.util]
bool_decide_rel_false [in misc.util]


C

cancel_left [in theory.jections]
cancel_left' [in theory.jections]
component_equality_to_product [in theory.ua_products]
compose_lt [in orders.semirings]
compose_le [in orders.semirings]
concat_app [in implementations.cons_list]
cut_minus_min3 [in theory.cut_minus]
cut_minus_opp [in theory.cut_minus]
cut_minus_plus_distr [in theory.cut_minus]
cut_minus_zero_plus_toggle [in theory.cut_minus]
cut_minus_plus_l_rev [in theory.cut_minus]
cut_minus_plus_toggle3 [in theory.cut_minus]
cut_minus_nonneg [in theory.cut_minus]
cut_minus_plus_toggle1 [in theory.cut_minus]
cut_minus_rightabsorb [in theory.cut_minus]
cut_minus_rightidentity [in theory.cut_minus]
cut_minus_plus_r_rev [in theory.cut_minus]
cut_minus_diag [in theory.cut_minus]
cut_minus_plus_toggle2 [in theory.cut_minus]
cut_minus_leftabsorb [in theory.cut_minus]
cut_minus_min2 [in theory.cut_minus]
cut_minus_ring_minus [in theory.cut_minus]
cut_minus_mult_distr_r [in theory.cut_minus]
cut_minus_zeros_le [in theory.cut_minus]
cut_minus_le_trans [in theory.cut_minus]
cut_minus_min1 [in theory.cut_minus]
cut_minus_mult_distr_l [in theory.cut_minus]


D

decode_morphism_and_ops [in varieties.groups]
decode_morphism_and_ops [in varieties.rings]
decode_morphism_and_ops [in varieties.monoids]
decode_morphism_and_ops [in varieties.semirings]
decode_morphism_and_ops [in varieties.semigroups]
decompose_lt [in orders.semirings]
decompose_le [in orders.semirings]
dec_mult_inv_ne_0_iff [in theory.dec_fields]
dec_mult_inv_1 [in theory.dec_fields]
dec_mult_inv_swap_l [in theory.dec_fields]
dec_mult_inv_distr [in theory.dec_fields]
dec_mult_inv_correct [in theory.dec_fields]
dec_mult_inv_swap_r [in theory.dec_fields]
dec_mult_inv_involutive [in theory.dec_fields]
dec_mult_inv_opp [in theory.dec_fields]
dec_quotients [in theory.dec_fields]
dec_mult_inv_zero [in theory.dec_fields]
dec_mult_inv_to_mult_inv [in theory.dec_fields]
distribute_sum [in theory.sequences]
dnn_hd_nonneg [in theory.series]
dnn_Str_nth_nonneg [in theory.series]
dnn_alt [in theory.series]
DtoQ_slow_preserves_opp [in implementations.dyadics]
DtoQ_slow_preserves_1 [in implementations.dyadics]
DtoQ_slow_correct [in implementations.dyadics]
DtoQ_slow_preserves_plus [in implementations.dyadics]
DtoQ_slow_preserves_mult [in implementations.dyadics]
DtoQ_slow_preserves_0 [in implementations.dyadics]
DtoQ_correct [in implementations.dyadics]
dy_eq_dec_aux_neg [in implementations.dyadics]
dy_eq_dec_aux [in implementations.dyadics]
dy_le_dec_aux [in implementations.dyadics]


E

eAlgebra_eSub [in theory.ua_congruence]
encode_algebra_only [in varieties.semigroups]
encode_morphism_only [in varieties.rings]
encode_morphism_and_ops [in varieties.groups]
encode_algebra_only [in varieties.rings]
encode_morphism_only [in varieties.semigroups]
encode_morphism_and_ops [in varieties.rings]
encode_morphism_only [in varieties.monoids]
encode_algebra_only [in varieties.monoids]
encode_morphism_and_ops [in varieties.monoids]
encode_morphism_only [in varieties.groups]
encode_algebra_only [in varieties.groups]
encode_morphism_and_ops [in varieties.semigroups]
equal_by_normal [in theory.quote_monoid]
equal_dec_quotients [in theory.dec_fields]
equal_quotients [in theory.fields]
equal_by_one_quotient [in theory.dec_fields]
equal_because_sole [in theory.adjunctions]
equal_by_zero_sum [in theory.rings]
eq_le [in orders.orders]
eq_le_flip [in orders.orders]
eq_not_lt [in orders.orders]
eSub_eAlgebra [in theory.ua_congruence]
eval_is_close [in varieties.closed_terms]
eval_map_var [in interfaces.universal_algebra]
EventuallyForAll_tl [in theory.streams]
EventuallyForAll_Str_nth_tl [in theory.streams]
extend_comp [in theory.sequences]
extend_inject [in theory.sequences]


F

field_div_0_l [in theory.fields]
field_div_diag [in theory.fields]
first_iso [in theory.ua_congruence]
flip_neg_mult_l [in orders.semirings]
flip_le_dec_mult_inv_r [in orders.dec_fields]
flip_nonpos_mult_r [in orders.semirings]
flip_nonneg_opp [in orders.rings]
flip_neg_minus [in orders.rings]
flip_lt_opp [in orders.rings]
flip_le_minus_l [in orders.rings]
flip_bijection_pseudoinstance [in theory.jections]
flip_le_opp [in orders.rings]
flip_le_minus_r [in orders.rings]
flip_lt_minus_r [in orders.rings]
flip_opp_zero [in theory.rings]
flip_nonpos_minus [in orders.rings]
flip_neg_mult_r [in orders.semirings]
flip_lt_dec_mult_inv_r [in orders.dec_fields]
flip_le_dec_mult_inv [in orders.dec_fields]
flip_opp_ne_0 [in theory.rings]
flip_nonpos_mult_l [in orders.semirings]
flip_lt_minus_l [in orders.rings]
flip_lt_dec_mult_inv_l [in orders.dec_fields]
flip_pos_opp [in orders.rings]
flip_neg_opp [in orders.rings]
flip_nonpos_opp [in orders.rings]
flip_lt_dec_mult_inv [in orders.dec_fields]
flip_pos_minus [in orders.rings]
flip_nonneg_minus [in orders.rings]
flip_le_dec_mult_inv_l [in orders.dec_fields]
flip_bijection [in theory.jections]
fmap_alt [in theory.sequences]
fold_inject [in theory.sequences]
fold_map [in theory.sequences]
ForAll_True [in theory.streams]
ForAll_tl [in theory.streams]
Frac_nonzero_num [in implementations.field_of_fractions]
Frac_dec_mult_num_den [in implementations.field_of_fractions]
from_ring_order [in orders.rings]
from_pseudo_ring_order [in orders.rings]
from_nat_stmt [in theory.naturals]
from_full_pseudo_ring_order [in orders.rings]
from_strict_ring_order [in orders.rings]
full_pseudo_order_preserving [in orders.maps]
full_pseudo_order_preserving_back [in orders.maps]


G

geneq_sym [in theory.ua_term_monad]
geneq_trans [in theory.ua_term_monad]
ge_1_mult_le_compat_r [in orders.semirings]
ge_1_gt_1_mult_compat [in orders.semirings]
ge_1_mult_compat [in orders.semirings]
ge_1_mult_le_compat_l [in orders.semirings]
gt_1_mult_lt_compat_r [in orders.semirings]
gt_1_ge_1_mult_compat [in orders.semirings]
gt_1_mult_lt_compat_l [in orders.semirings]


H

heq_eval [in theory.ua_subvariety]
heq_eval_const [in theory.ua_subvariety]
HomoMorphism_Proper [in theory.ua_homomorphisms]


I

image_proper [in theory.ua_congruence]
induction [in orders.integers]
induction [in theory.naturals]
induction_nonneg [in orders.integers]
initials_unique' [in theory.categories]
initials_unique [in theory.categories]
injective_preserves_0 [in theory.rings]
injective_ne_1 [in theory.rings]
inject_epi [in theory.sequences]
inject_bigQ_frac_bigZ_correct [in implementations.fast_rationals]
inn_Str_nth [in theory.series]
integers_le_plus [in orders.integers]
integer_initial [in interfaces.integers]
int_abs_1 [in theory.int_abs]
int_pow_mult [in theory.int_pow]
int_pow_opp_alt [in theory.int_pow]
int_abs_0 [in theory.int_abs]
int_abs_0_alt [in theory.int_abs]
int_pow_nat_pow [in theory.int_pow]
int_pow_2 [in theory.int_pow]
int_abs_nat [in theory.int_abs]
int_abs_nonneg_mult [in theory.int_abs]
int_abs_nonneg [in theory.int_abs]
int_abs_opp_nat [in theory.int_abs]
int_pow_opp [in theory.int_pow]
int_pow_exp_plus [in theory.int_pow]
int_abs_uniq [in theory.int_abs]
int_pow_ge_1 [in theory.int_pow]
int_pow_mult_inv [in theory.int_pow]
int_pow_exp_mult [in theory.int_pow]
int_pow_4 [in theory.int_pow]
int_pow_S_nonneg [in theory.int_pow]
int_abs_opp [in theory.int_abs]
int_abs_ne_0 [in theory.int_abs]
int_abs_nonneg_plus [in theory.int_abs]
int_pow_gt_1 [in theory.int_pow]
int_abs_neg_is_pos [in theory.int_abs]
int_pow_3 [in theory.int_pow]
invert_homomorphism [in theory.ua_homomorphisms]
inv_0 [in theory.groups]
inv_involutive [in theory.groups]
iso_is_rationals [in theory.rationals]


L

laws [in varieties.semirings]
laws [in theory.ua_subvariety]
laws_hold [in theory.ua_products]
laws_hold [in varieties.open_terms]
laws_hold [in varieties.closed_terms]
left_cancellation_ne_0 [in theory.rings]
le_iff_lt_plus_1 [in orders.integers]
le_1_2 [in orders.semirings]
le_3_4 [in orders.semirings]
le_not_lt_flip [in orders.orders]
le_2_4 [in orders.semirings]
le_2_3 [in orders.semirings]
le_lt_trans [in orders.orders]
le_1_4 [in orders.semirings]
le_or_lt [in orders.orders]
le_equiv_lt [in orders.orders]
le_iff_lt_plus_1 [in orders.naturals]
le_1_3 [in orders.semirings]
le_flip [in orders.orders]
list_map [in implementations.ne_list]
lt_antisym [in orders.orders]
lt_2_3 [in orders.semirings]
lt_le_trans [in orders.orders]
lt_apart_flip [in orders.orders]
lt_1_4 [in orders.semirings]
lt_2_4 [in orders.semirings]
lt_iff_plus_1_le [in orders.integers]
lt_iff_plus_1_le [in orders.naturals]
lt_1_3 [in orders.semirings]
lt_3_4 [in orders.semirings]
lt_ne_flip [in orders.orders]
lt_flip [in orders.orders]
lt_iff_le_ne [in orders.orders]
lt_1_2 [in orders.semirings]
lt_apart [in orders.orders]
lt_ne [in orders.orders]
lt_le [in orders.orders]
lt_not_le_flip [in orders.orders]


M

map_iso [in theory.ua_mapped_operations]
max_ub_r [in orders.minmax]
max_diag [in orders.minmax]
max_l [in orders.minmax]
max_ub_l [in orders.minmax]
max_r [in orders.minmax]
min_lb_l [in orders.minmax]
min_r [in orders.minmax]
min_lb_r [in orders.minmax]
min_diag [in orders.minmax]
min_l [in orders.minmax]
morphisms_involutive [in theory.rationals]
morphisms_involutive [in theory.naturals]
morphisms_involutive [in theory.integers]
mor_from_sr_to_alg [in varieties.setoids]
mor_from_sr_to_alg [in varieties.semirings]
mult_inv_irrelevant [in theory.fields]
mult_inv_distr [in implementations.nonzero_field_elements]
mult_lt_compat [in orders.semirings]
mult_inv_proper_alt [in theory.fields]
mult_apart_zero_r [in theory.fields]
mult_le_compat [in orders.semirings]
mult_inv_distr_alt [in theory.fields]
mult_apart_zero_l [in theory.fields]
mult_inverse_alt [in theory.fields]


N

naturals_nonneg [in orders.naturals]
natural_le_plus [in orders.naturals]
natural_initial [in interfaces.naturals]
nat_pow_base_0 [in theory.nat_pow]
nat_pow_3 [in theory.nat_pow]
nat_pow_exp_mult [in theory.nat_pow]
nat_pow_exp_plus [in theory.nat_pow]
nat_pow_base_mult [in theory.nat_pow]
nat_pow_2 [in theory.nat_pow]
nat_pow_ge_1 [in theory.nat_pow]
nat_distance_unique_respectful [in theory.nat_distance]
nat_pow_4 [in theory.nat_pow]
nat_distance_unique [in theory.nat_distance]
neg_dec_mult_inv_compat [in orders.dec_fields]
neg_mult [in orders.semirings]
neg_mult_decompose [in orders.semirings]
neg_plus_compat [in orders.semirings]
neg_pos_mult [in orders.semirings]
ne_0_ge_1 [in orders.naturals]
ne_total_lt [in orders.orders]
nonneg_minus_compat_back [in orders.rings]
nonneg_nonpos_mult [in orders.semirings]
nonneg_plus_le_compat_l [in orders.semirings]
nonneg_plus_lt_compat_l [in orders.semirings]
nonneg_minus_compat [in orders.rings]
nonneg_plus_lt_compat_r [in orders.semirings]
nonneg_mant [in implementations.dyadics]
nonneg_plus_le_compat_r [in orders.semirings]
nonpos_nonneg_mult [in orders.semirings]
nonpos_mult [in orders.semirings]
nonpos_plus_compat [in orders.semirings]
nonpos_dec_mult_inv_compat [in orders.dec_fields]
nonpos_mant [in implementations.dyadics]
not_le_1_0 [in orders.semirings]
not_lt_le_flip [in orders.orders]
not_symmetry [in misc.util]
not_le_ne [in orders.orders]
not_le_2_0 [in orders.semirings]
not_le_not_lt [in orders.orders]
not_lt_apart_lt_flip [in orders.orders]
not_le_lt_flip [in orders.orders]
nqe_always [in theory.ua_products]
NtoZ_uniq [in implementations.natpair_integers]
NType_Integers.NType_two_2 [in implementations.NType_naturals]
NType_Integers.NType_succ_1_plus [in implementations.NType_naturals]
NType_Integers.NType_semiring_theory [in implementations.NType_naturals]
nz_one_plus_zero [in theory.naturals]


O

one_sum [in theory.naturals]
opp_0 [in theory.rings]
opp_mult_distr_l [in theory.rings]
opp_to_semiring [in orders.naturals]
opp_to_sr_le_to_sr [in orders.naturals]
opp_zero_prod_l [in theory.rings]
opp_zero_prod_r [in theory.rings]
opp_to_semiring_nonpos [in orders.naturals]
opp_swap_r [in theory.rings]
opp_involutive [in theory.rings]
opp_mult_opp [in theory.rings]
opp_distr [in theory.rings]
opp_mult [in theory.rings]
opp_swap_l [in theory.rings]
opp_mult_distr_r [in theory.rings]
order_preserving_back_flip_pos [in orders.maps]
order_preserving_back_pos [in orders.maps]
order_preserving_back_flip [in orders.maps]
order_preserving_flip [in orders.maps]
order_preserving_flip_nonneg [in orders.maps]
order_preserving_nonneg [in orders.maps]


P

Permutation_ne_tl_length [in implementations.ne_list]
Pinv [in theory.ring_ideals]
plus_le_lt_compat [in orders.semirings]
plus_lt_compat [in orders.semirings]
plus_le_compat [in orders.semirings]
plus_le_compat_l [in orders.semirings]
plus_lt_compat_l [in orders.semirings]
plus_lt_le_compat [in orders.semirings]
plus_mult_distr_l [in theory.rings]
plus_le_compat_r [in orders.semirings]
plus_opp_l [in theory.rings]
plus_opp_r [in theory.rings]
plus_lt_compat_r [in orders.semirings]
plus_mult_distr_r [in theory.rings]
pos_neg_mult [in orders.semirings]
pos_plus_lt_compat_r [in orders.semirings]
pos_plus_le_lt_compat_l [in orders.semirings]
pos_minus_compat [in orders.rings]
pos_plus_le_lt_compat_r [in orders.semirings]
pos_plus_lt_compat_l [in orders.semirings]
pos_mult_decompose [in orders.semirings]
Pplus [in theory.ring_ideals]
preservation [in theory.ua_products]
Preservation_proper' [in theory.ua_homomorphisms]
preserves_cut_minus [in theory.cut_minus]
preserves_lt_1 [in orders.semirings]
preserves_nat_pow_exp [in theory.nat_pow]
preserves_2 [in theory.rings]
preserves_powers_help [in theory.series]
preserves_mult_inv [in theory.fields]
preserves_inv [in theory.groups]
preserves_le_1 [in orders.semirings]
preserves_opp [in theory.rings]
preserves_0 [in theory.rings]
preserves_int_pow_exp [in theory.int_pow]
preserves_4 [in theory.rings]
preserves_max [in orders.minmax]
preserves_shiftl_exp [in theory.shiftl]
preserves_minus [in theory.rings]
preserves_nonpos [in orders.semirings]
preserves_abs [in theory.abs]
preserves_ge_opp1 [in orders.rings]
preserves_int_pow [in theory.int_pow]
preserves_ge_1 [in orders.semirings]
preserves_dec_mult_inv [in theory.dec_fields]
preserves_mult [in theory.rings]
preserves_positives [in theory.series]
preserves_plus [in theory.rings]
preserves_factorials [in theory.series]
preserves_powers [in theory.series]
preserves_1 [in theory.rings]
preserves_nat_pow [in theory.nat_pow]
preserves_min [in orders.minmax]
preserves_gt_1 [in orders.semirings]
preserves_neg [in orders.semirings]
preserves_shiftl [in theory.shiftl]
preserves_3 [in theory.rings]
preserves_le_opp1 [in orders.rings]
preserving_preserves_nonneg [in orders.semirings]
preserving_back_preserves_nonneg [in orders.rings]
products_unique [in theory.categories]
projected_strict_order [in orders.maps]
projected_pseudo_order [in orders.maps]
projected_full_pseudo_ring_order [in orders.rings]
projected_full_pseudo_order [in orders.maps]
projected_setoid [in theory.setoids]
projected_strong_setoid [in theory.strong_setoids]
projected_ring_order [in orders.rings]
projected_strict_ring_order [in orders.rings]
projected_srorder [in orders.semirings]
projected_ring [in theory.rings]
projected_partial_order [in orders.maps]
projected_total_order [in orders.maps]
projected_strict_setoid_order [in orders.maps]
projected_pseudo_ring_order [in orders.rings]
pseudo_order_lt_apart_flip [in orders.orders]
pseudo_order_embedding_inj [in orders.maps]
pseudo_order_lt_apart [in orders.orders]
pseudo_order_lt_ext [in orders.orders]
pseudo_order_cotrans_twice [in orders.orders]
P0 [in theory.ring_ideals]


Q

QType_Rationals.anyQ_field_theory [in implementations.QType_rationals]
quote_equality [in theory.quote_monoid]
quotients [in implementations.nonzero_field_elements]
quotient_variety [in theory.ua_congruence]


R

rationals_decompose_pos_den [in orders.rationals]
rationals_decompose [in theory.rationals]
rationals_decompose_le [in orders.rationals]
reflexive [in misc.JMrelation]
right_cancellation_ne_0 [in theory.rings]
right_cancel_from_left [in theory.rings]


S

same_morphism [in theory.naturals]
same_morphism [in implementations.natpair_integers]
same_morphism [in theory.integers]
sg_inv_distr [in theory.groups]
shiftl_le_flip_l [in theory.shiftl]
shiftl_opp_1_to_half [in theory.shiftl]
shiftl_spec_from_int_pow [in interfaces.additional_operations]
shiftl_opp [in theory.shiftl]
shiftl_le_flip_r [in theory.shiftl]
shiftl_opp_to_mult_inv_nat_pow [in theory.shiftl]
shiftl_opp_nat_pow [in theory.shiftl]
shiftl_int_pow [in theory.shiftl]
shiftl_base_nat_pow [in theory.shiftl]
shiftl_exp_plus [in theory.shiftl]
shiftl_reverse [in theory.shiftl]
shiftl_mult_r [in theory.shiftl]
shiftl_mult_l [in theory.shiftl]
shiftl_base_1_to_int_pow [in theory.shiftl]
shiftl_spec_from_nat_pow [in interfaces.additional_operations]
shiftl_base_1_int_pow [in theory.shiftl]
shiftl_order [in theory.shiftl]
shiftl_opp_1_half [in theory.shiftl]
shiftl_nat_pow_alt [in theory.shiftl]
shiftl_opp_1_to_fourth [in theory.shiftl]
shiftl_opp_1_fourth [in theory.shiftl]
shiftl_to_int_pow [in theory.shiftl]
shiftl_1 [in theory.shiftl]
shiftl_nat_pow [in theory.shiftl]
shiftl_base_plus [in theory.shiftl]
shiftl_2 [in theory.shiftl]
sig_type_refl [in interfaces.ua_basic]
simple.approach_B.example [in quote.classquote]
simple.approach_A.example [in quote.classquote]
simple.approach_B.do_quote [in quote.classquote]
square [in theory.ua_congruence]
square_nonneg [in orders.semirings]
square_pos [in orders.semirings]
SRpair_splits [in implementations.semiring_pairs]
stdlib_semiring_theory [in theory.rings]
stdlib_ring_theory [in theory.rings]
stream_eq_Str_nth [in theory.streams]
strictly_order_preserving_flip [in orders.maps]
strictly_order_preserving_flip_pos [in orders.maps]
strictly_order_preserving_back_flip [in orders.maps]
strictly_order_preserving_pos [in orders.maps]
strong_right_cancel_from_left [in theory.rings]
strong_binary_setoid_morphism_commutative [in theory.strong_setoids]
strong_injective_preserves_0 [in theory.fields]
strong_binary_setoid_morphism_both_coordinates [in theory.strong_setoids]
Str_nth_positives [in theory.series]
Str_nth_positives_help [in theory.series]
Str_nth_powers [in theory.series]
Str_nth_everyOther [in theory.series]
Str_nth_tl_everyOther [in theory.series]
Str_nth_powers_help [in theory.series]
Str_nth_factorials [in theory.series]
Str_nth_powers_int_pow [in theory.series]
Str_nth_factorials_help [in theory.series]
Str_nth_powers_help_int_pow [in theory.series]
subst_eval [in varieties.closed_terms]
surjective_applied [in theory.jections]
surjective_applied' [in theory.jections]
symmetric [in misc.JMrelation]
S_nat_1_plus [in implementations.peano_naturals]
S_nat_plus_1 [in implementations.peano_naturals]


T

tails_are_shorter [in implementations.ne_list]
tl_length [in implementations.ne_list]
to_ring_injective [in theory.integers]
to_ring_unique [in theory.integers]
to_semiring_involutive [in theory.naturals]
to_ring_twice [in theory.integers]
to_frac_unique [in theory.rationals]
to_rationals_unique [in theory.rationals]
to_semiring_injective [in theory.naturals]
to_semiring_nonneg [in orders.naturals]
to_rationals_unique_alt [in theory.rationals]
to_ring_self [in theory.integers]
to_rationals_involutive [in theory.rationals]
to_semiring_self [in theory.naturals]
to_semiring_unique_alt [in theory.naturals]
to_ring_unique_alt [in theory.integers]
to_semiring_twice [in theory.naturals]
to_semiring_unique [in theory.naturals]
to_ring_involutive [in theory.integers]
transfer_statement [in theory.ua_transference]
transfer_eval' [in theory.ua_transference]
transfer_statement_and_vars [in theory.ua_transference]
transfer_eval [in theory.ua_transference]
transitive [in misc.JMrelation]
tuple_round_trip [in theory.categories]
two_level_rect [in implementations.ne_list]


U

units_dont_divide_zero [in theory.rings]
unJM [in misc.JMrelation]


W

with_vars.bla [in quote.classquote]
with_vars.quote_equality [in quote.classquote]
with_vars.eval_map_var [in quote.classquote]
with_vars.sum_assoc [in quote.classquote]
with_vars.monkey [in quote.classquote]


Z

zero_sum [in theory.naturals]
zero_product_aux [in implementations.natpair_integers]
ZtoQ_shift [in implementations.dyadics]
ZType_Integers.ZType_two_2 [in implementations.ZType_integers]
ZType_Integers.ZType_ring_theory [in implementations.ZType_integers]
ZType_Integers.ZType_succ_1_plus [in implementations.ZType_integers]


other

φ_adjunction_natural_left_inv [in theory.adjunctions]
φ_in_terms_of_ε [in theory.adjunctions]
φ_adjunction_natural_right_inv [in theory.adjunctions]
φ_in_terms_of_η [in theory.adjunctions]



Section Index

A

adjunction [in theory.categories]
algebras [in theory.ua_products]
alt_Build_Rationals [in theory.rationals]
another_semiring_strict [in orders.semirings]
another_semiring [in orders.semirings]
another_full_pseudo_ring_order [in orders.rings]
another_rationals [in theory.rationals]
another_category [in categories.empty]
another_ring_order [in orders.rings]
another_integers [in theory.rationals]
another_strict_ring_order [in orders.rings]
another_pseudo_ring_order [in orders.rings]


C

cancellation [in interfaces.abstract_algebra]
cancellation [in theory.rings]
categorical [in theory.ua_products]
categorical.for_a_given_c [in theory.ua_products]
compose_functors [in interfaces.functors]
composition [in orders.maps]
compositions [in theory.jections]
contents [in implementations.polynomials]
contents [in theory.int_abs]
contents [in theory.ua_transference]
contents [in theory.quote_monoid]
contents [in implementations.field_of_fractions]
contents [in theory.nat_distance]
contents [in categories.categories]
contents [in categories.product]
contents [in theory.dec_fields]
contents [in varieties.open_terms]
contents [in varieties.closed_terms]
contents [in categories.functors]
contents [in theory.ua_homomorphisms]
contents [in implementations.natpair_integers]
contents [in categories.dual]
contents [in theory.hom_functor]
contents [in theory.ua_congruence]
contents [in theory.abs]
contents [in theory.integers]
contents [in theory.monoid_normalization]
contents [in implementations.ne_list]
contents [in theory.sequences]
contents [in theory.naturals]
contents [in implementations.nonzero_field_elements]
contents [in categories.JMcat]
contents [in categories.algebras]
contents [in theory.monads]
contents [in theory.forget_variety]
contents [in categories.varieties]
contents [in theory.ua_term_monad]
contents [in orders.minmax]
contents [in categories.setoids]
contents [in theory.categories]
contents [in theory.forget_algebra]
contents [in theory.ua_subvariety]
contents [in orders.dec_fields]
contents [in implementations.cons_list]
contents [in theory.ua_mapped_operations]
contents [in theory.strong_setoids]
contents.arrow_setoid [in categories.functors]
contents.associativity [in categories.categories]
contents.borrowed_from_nat [in theory.naturals]
contents.equality [in theory.ua_term_monad]
contents.factors [in categories.product]
contents.for_another_ring [in implementations.natpair_integers]
contents.for_nice_e [in theory.ua_congruence]
contents.for_another_object [in varieties.closed_terms]
contents.for_another_ring.for_another_morphism [in implementations.natpair_integers]
contents.homo [in theory.ua_homomorphisms]
contents.homo.with_f [in theory.ua_homomorphisms]
contents.initiality [in theory.categories]
contents.isomorphy [in theory.categories]
contents.Lookup [in theory.quote_monoid]
contents.map_op [in theory.ua_mapped_operations]
contents.more_arrows [in categories.JMcat]
contents.more_arrows [in categories.categories]
contents.product [in categories.setoids]
contents.products [in theory.categories]
contents.products.def [in theory.categories]
contents.Quote [in theory.quote_monoid]
cut_minus_properties [in theory.cut_minus]
cut_minus_default [in theory.cut_minus]
cut_minus_properties.min [in theory.cut_minus]


D

decode_operations [in varieties.monoids]
decode_operations [in varieties.groups]
decode_operations [in varieties.semigroups]
decode_operations [in varieties.rings]
dec_setoid [in theory.strong_setoids]
dec_partial_order [in orders.orders]
dec_semiring_order [in orders.semirings]
dec_setoid_morphisms [in theory.strong_setoids]
default_order [in orders.integers]
default_order [in orders.rationals]
default_shiftl_integers [in theory.shiftl]
default_order [in orders.naturals]
default_shiftl_naturals [in theory.shiftl]
dyadics [in implementations.dyadics]
dyadics.DtoQ [in implementations.dyadics]
dyadics.DtoQ_slow [in implementations.dyadics]
dyadics.embed_rationals [in implementations.dyadics]
dyadics.with_rationals [in implementations.dyadics]


E

encode_variety_and_ops [in varieties.monoids]
encode_variety_and_ops [in varieties.semigroups]
encode_with_ops [in varieties.rings]
encode_variety_and_ops [in varieties.groups]
exp_preservation [in theory.nat_pow]
exp_preservation [in theory.shiftl]
exp_preservation [in theory.int_pow]


F

field_properties [in theory.fields]
first_iso [in theory.ua_congruence]
for_signature.Vars [in interfaces.universal_algebra]
for_signature [in interfaces.universal_algebra]
for_signature.applications_ind [in interfaces.universal_algebra]
for_another_semiring [in implementations.peano_naturals]
for_ηAdjunction [in theory.adjunctions]
for_ηεAdjunction [in theory.adjunctions]
for_φAdjunction [in theory.adjunctions]
for_signature.eval [in interfaces.universal_algebra]
from_full_pseudo_ring_order [in orders.rings]
from_instance [in varieties.semirings]
from_instance [in varieties.setoids]
from_strict_ring_order [in orders.rings]
from_stdlib_semiring_theory [in theory.rings]
from_stdlib_ring_theory [in theory.rings]
from_another_ring [in theory.rings]
from_pseudo_ring_order [in orders.rings]
from_variety [in varieties.setoids]
from_stdlib_field_theory [in theory.dec_fields]
from_ring_order [in orders.rings]
full_pseudo_order [in orders.orders]
full_pseudo_semiring_order [in orders.semirings]
full_pseudo_strictly_preserving [in orders.maps]
functors [in categories.dual]
functor_class [in interfaces.functors]


G

groupmor_props [in theory.groups]
group_props [in theory.groups]


I

ideal_congruence [in theory.ring_ideals]
id_functor [in interfaces.functors]
initial_maps [in interfaces.naturals]
initial_maps [in interfaces.integers]
integers_order.another_ring [in orders.integers]
integers_order [in orders.integers]
integral_domain_props [in theory.rings]
intfrac_rationals [in implementations.intfrac_rationals]
int_pow_properties [in theory.int_pow]
int_pow [in implementations.positive_semiring_elements]
int_pow_default [in theory.int_pow]
in_domain [in theory.ua_congruence]
isomorphic_image_is_rationals [in theory.rationals]
is_field [in theory.dec_fields]


J

jections [in interfaces.abstract_algebra]


K

kernel_is_ideal [in theory.ring_ideals]


L

laws [in varieties.rings]
laws [in varieties.groups]
laws [in varieties.semigroups]
laws [in varieties.semirings]
laws [in varieties.monoids]


M

more [in theory.streams]
more_shiftl_dec_field [in theory.shiftl]
more_morphisms [in theory.strong_setoids]
morphisms [in implementations.field_of_fractions]
morphisms [in theory.dec_fields]
morphisms [in theory.fields]
morphisms [in theory.strong_setoids]
morphism_classes [in interfaces.abstract_algebra]
morphism_composition [in theory.rings]


N

naturals_order.another_ring [in orders.naturals]
naturals_order [in orders.naturals]
naturals_order.another_semiring [in orders.naturals]
NaturalTransformation [in theory.categories]
natural_transformations_id_comp [in categories.functors]
nat_pow_properties [in theory.nat_pow]
nat_pow_default [in theory.nat_pow]
nonneg_integers_naturals [in implementations.nonneg_integers_naturals]
nonneg_semiring_elements [in implementations.nonneg_semiring_elements]


O

object [in categories.product]
obvious [in misc.util]
ops [in interfaces.monads]
ops_from_alg_to_sr [in varieties.semirings]
order_preserving [in theory.cut_minus]
order_unique [in orders.naturals]
order_maps [in interfaces.orders]
order_preserving [in theory.abs]
order_preserving [in orders.minmax]
order_preserving_ops [in orders.maps]
other_results [in orders.naturals]
other_results [in orders.integers]


P

packed [in theory.ua_packed]
packed.forallArgs [in theory.ua_packed]
partial_order [in orders.orders]
pointwise_dependent_relation [in misc.util]
positive_semiring_elements [in implementations.positive_semiring_elements]
positive_semiring_elements.shiftl [in implementations.positive_semiring_elements]
practical [in interfaces.sequences]
preservation [in theory.series]
preservation [in theory.shiftl]
preservation [in theory.int_pow]
preservation [in theory.nat_pow]
product [in theory.setoids]
propers [in orders.maps]
pseudo_semiring_order [in orders.semirings]
pseudo_order [in orders.orders]
pseudo_injective [in orders.maps]


R

rationals_and_another_rationals [in orders.rationals]
rationals_order_isomorphic [in orders.rationals]
rationals_to_frac [in interfaces.rationals]
rationals_and_integers [in orders.rationals]
retract_is_int.for_another_ring [in theory.integers]
retract_is_nat.for_another_semirings [in theory.naturals]
retract_is_nat [in theory.naturals]
retract_is_int [in theory.integers]
ringmor_props [in theory.rings]
ring_props [in theory.rings]
ring_order [in orders.rings]


S

semiringmor_props [in theory.rings]
semiring_pairs.with_semiring_order [in implementations.semiring_pairs]
semiring_props [in theory.rings]
semiring_pairs.with_strict_semiring_order [in implementations.semiring_pairs]
semiring_pairs.with_full_pseudo_semiring_order [in implementations.semiring_pairs]
semiring_order [in orders.semirings]
semiring_pairs [in implementations.semiring_pairs]
semiring_folds [in theory.sequences]
series [in theory.series]
series.every_other [in theory.series]
series.factorials [in theory.series]
series.mult [in theory.series]
series.positives [in theory.series]
series.powers [in theory.series]
series.powers.with_nat_pow [in theory.series]
series.powers.with_int_pow [in theory.series]
setoid_morphisms [in interfaces.abstract_algebra]
setoid_functor [in interfaces.functors]
setoid_binary_morphisms [in interfaces.abstract_algebra]
setoid_functor_as_posh_functor [in theory.functors]
shiftl [in theory.shiftl]
shiftl_dec_field [in theory.shiftl]
shiftl_field [in theory.shiftl]
simple_product [in theory.setoids]
simple.approach_B.instances [in quote.classquote]
simple.approach_A.instances [in quote.classquote]
specializable [in interfaces.integers]
specialized [in varieties.monoids]
specialized [in varieties.semigroups]
streams [in theory.streams]
strictly_order_preserving [in orders.maps]
strictly_order_preserving_dec [in orders.maps]
strict_semiring_order [in orders.semirings]
strict_partial_order [in orders.orders]
strict_order [in orders.orders]
strict_ring_order [in orders.rings]
strong_cancellation [in theory.rings]
structure [in interfaces.monads]
subalgebras [in theory.ua_subalgebraT]
subalgebras [in theory.ua_subalgebra]


U

UniversalArrow [in theory.categories]
upper_classes [in interfaces.abstract_algebra]


V

varieties [in theory.ua_products]


W

with_vars.inspect [in quote.classquote]
with_sorts [in interfaces.ua_basic]
with_vars.Quote [in quote.classquote]
with_vars.Lookup [in quote.classquote]
with_vars.obvious [in quote.classquote]



Constructor Index

A

abs_sig [in interfaces.canonical_names]
algebra_op [in interfaces.ua_basic]
antisymmetry [in interfaces.canonical_names]
apart [in interfaces.canonical_names]
App [in interfaces.universal_algebra]
AppliedOp [in theory.ua_packed]
AppliedVar [in theory.ua_packed]
arrow [in categories.functors]
arrow [in categories.categories]
arrow [in categories.JMcat]
Arrow [in interfaces.canonical_names]
associativity [in interfaces.canonical_names]


B

biinduction [in interfaces.canonical_names]
bind [in interfaces.monads]


C

C [in implementations.semiring_pairs]
cat_id [in interfaces.canonical_names]
coerce [in interfaces.canonical_names]
commutativity [in interfaces.canonical_names]
Comp [in theory.monoid_normalization]
comp [in interfaces.canonical_names]
Conj [in interfaces.universal_algebra]
cons [in implementations.ne_list]
cotransitive [in interfaces.canonical_names]
cut_minus [in interfaces.additional_operations]


D

decide [in interfaces.canonical_names]
decreasing_nonneg [in theory.series]
dec_mult_inv [in interfaces.canonical_names]
Disj [in interfaces.universal_algebra]
distribute_l [in interfaces.canonical_names]
distribute_r [in interfaces.canonical_names]
div_euclid [in interfaces.additional_operations]
dyadic [in implementations.dyadics]


E

Eq [in interfaces.universal_algebra]
equiv [in interfaces.canonical_names]
Ext [in interfaces.universal_algebra]
extend [in interfaces.sequences]
ext_if [in theory.streams]
e_mult_assoc [in varieties.groups]
e_sym [in varieties.closed_terms]
e_mult_1_l [in varieties.monoids]
e_mult_assoc [in varieties.semigroups]
e_vars [in varieties.open_terms]
e_sub [in varieties.open_terms]
e_trans [in varieties.closed_terms]
e_refl [in varieties.open_terms]
e_law [in varieties.open_terms]
e_plus_0_l [in varieties.rings]
e_law [in varieties.closed_terms]
e_sym [in varieties.open_terms]
e_plus_assoc [in varieties.rings]
e_distr_r [in varieties.semirings]
e_mult_comm [in varieties.semirings]
e_mult_1_l [in varieties.groups]
e_mult_0_l [in varieties.semirings]
e_sub [in varieties.closed_terms]
e_plus_comm [in varieties.semirings]
e_mult_1_r [in varieties.monoids]
e_mult_assoc [in varieties.semirings]
e_plus_assoc [in varieties.semirings]
e_mult_1_r [in varieties.groups]
e_mult_inv_r [in varieties.groups]
e_distr_l [in varieties.rings]
e_distr [in varieties.rings]
e_mult_assoc [in varieties.monoids]
e_mult_inv_l [in varieties.groups]
e_mult_comm [in varieties.rings]
e_mult_0_l [in varieties.rings]
e_mult_1_l [in varieties.semirings]
e_plus_0_l [in varieties.semirings]
e_trans [in varieties.open_terms]
e_plus_opp_l [in varieties.rings]
e_distr_l [in varieties.semirings]
e_mult_1_l [in varieties.rings]
e_refl [in varieties.closed_terms]
e_plus_comm [in varieties.rings]
e_mult_assoc [in varieties.rings]
e_plus_opp_r [in varieties.rings]


F

finite [in interfaces.canonical_names]
fmap [in interfaces.functors]
frac [in implementations.field_of_fractions]


G

group_inv [in interfaces.canonical_names]


H

hetero_symmetric [in interfaces.canonical_names]


I

Impl [in interfaces.universal_algebra]
increasing_nonneg [in theory.series]
infinite [in interfaces.canonical_names]
initial_arrow_unique [in theory.categories]
initial_arrow [in theory.categories]
inject [in interfaces.sequences]
integers_to_ring [in interfaces.integers]
int_as_nat [in interfaces.integers]
int_abs_sig [in interfaces.integers]
inv [in varieties.groups]
inverse [in interfaces.canonical_names]


L

le [in interfaces.canonical_names]
left_inverse [in interfaces.canonical_names]
left_identity [in interfaces.canonical_names]
left_absorb [in interfaces.canonical_names]
left_cancellation [in interfaces.abstract_algebra]
lt [in interfaces.canonical_names]


M

makes_products [in theory.categories]
make_tuple [in theory.categories]
mod_euclid [in interfaces.additional_operations]
mono [in theory.categories]
mon_unit [in interfaces.canonical_names]
MoreArguments [in theory.ua_packed]
mult [in varieties.semigroups]
mult [in varieties.semirings]
mult [in varieties.groups]
mult [in varieties.rings]
mult [in varieties.monoids]
mult_inv [in interfaces.canonical_names]


N

natural [in theory.categories]
naturals_to_semiring [in interfaces.naturals]
nat_distance_sig [in interfaces.naturals]
NoMoreArguments [in theory.ua_packed]
non_empty [in misc.util]
no_zero_divisors [in interfaces.canonical_names]


O

object [in categories.functors]
object [in categories.JMcat]
object [in categories.setoids]
object [in categories.varieties]
object [in categories.algebras]
object [in categories.categories]
obvious [in misc.util]
one [in varieties.semirings]
one [in implementations.ne_list]
one [in varieties.rings]
one [in varieties.monoids]
one [in varieties.groups]
Op [in interfaces.universal_algebra]
opp [in varieties.rings]


P

plus [in varieties.semirings]
plus [in varieties.rings]
pow [in interfaces.additional_operations]
product [in theory.categories]
product_factors [in theory.categories]
prop_holds [in misc.util]


R

ralgebra_action [in interfaces.canonical_names]
rationals_to_frac [in interfaces.rationals]
relate [in misc.JMrelation]
ret [in interfaces.monads]
right_inverse [in interfaces.canonical_names]
right_absorb [in interfaces.canonical_names]
right_identity [in interfaces.canonical_names]
right_cancellation [in interfaces.abstract_algebra]
ring_mult [in interfaces.canonical_names]
ring_zero [in interfaces.canonical_names]
ring_mult_inverse [in interfaces.canonical_names]
ring_plus [in interfaces.canonical_names]
ring_unit_mult_inverse [in interfaces.canonical_names]
ring_one [in interfaces.canonical_names]


S

scalar_mult [in interfaces.vectorspace]
setoid_eq [in interfaces.abstract_algebra]
sfmap [in interfaces.functors]
sg_op [in interfaces.canonical_names]
shiftl [in interfaces.additional_operations]
shiftr [in interfaces.additional_operations]
simple_associativity [in interfaces.canonical_names]
simple.approach_A.quote [in quote.classquote]
simple.Mult [in quote.classquote]
simple.One [in quote.classquote]
simple.Plus [in quote.classquote]
simple.Zero [in quote.classquote]
stable [in misc.util]
stream_eq_coind [in theory.streams]
strong_right_cancellation [in interfaces.abstract_algebra]
strong_left_cancellation [in interfaces.abstract_algebra]


T

total [in interfaces.canonical_names]
trichotomy [in interfaces.canonical_names]
trivial_apart [in interfaces.canonical_names]
tuple_proj [in theory.categories]


U

Unit [in theory.monoid_normalization]
universal_arrow [in theory.categories]


V

Var [in theory.monoid_normalization]
Var [in interfaces.universal_algebra]


W

with_vars.Var [in quote.classquote]
with_vars.obvious [in quote.classquote]
with_vars.Zero [in quote.classquote]
with_vars.Mult [in quote.classquote]


Z

zero [in varieties.semirings]
zero [in varieties.rings]
zero_divisor [in interfaces.canonical_names]
zero_product [in interfaces.canonical_names]



Notation Index

N

_ === _ [in interfaces.universal_algebra]
_ -=> _ [in interfaces.universal_algebra]
_ ::: _ [in implementations.ne_list]


O

_ -=> _ [in interfaces.universal_algebra]


other

_ = _ (type_scope) [in interfaces.canonical_names]
_ ≠ _ (type_scope) [in interfaces.canonical_names]
_ ⪥ _ (type_scope) [in interfaces.canonical_names]
_ < _ < _ [in interfaces.canonical_names]
_ >> _ [in interfaces.monads]
_ ∸ _ [in interfaces.additional_operations]
_ ≤ _ ≤ _ [in interfaces.canonical_names]
_ / _ [in interfaces.canonical_names]
_ ◎ _ [in interfaces.canonical_names]
_ ≡ _ [in interfaces.canonical_names]
_ ⇛ _ [in theory.categories]
_ ≪ _ [in interfaces.additional_operations]
_ ⟶ _ [in interfaces.canonical_names]
_ ↾ _ [in interfaces.canonical_names]
_ ∞ [in interfaces.canonical_names]
_ ⁻ [in interfaces.canonical_names]
_ - _ [in interfaces.canonical_names]
_ ≢ _ [in interfaces.canonical_names]
_ ₀ [in interfaces.canonical_names]
_ · _ [in interfaces.vectorspace]
_ ₊ [in interfaces.canonical_names]
_ // _ [in interfaces.canonical_names]
_ ⁺ [in interfaces.canonical_names]
_ ← _ ; _ [in interfaces.monads]
_ & _ [in interfaces.canonical_names]
_ >>= _ [in interfaces.monads]
_ $ _ [in implementations.dyadics]
_ ^ _ [in interfaces.additional_operations]
_ < _ ≤ _ [in interfaces.canonical_names]
_ `div` _ [in interfaces.additional_operations]
_ ≤ _ < _ [in interfaces.canonical_names]
_ `mod` _ [in interfaces.additional_operations]
_ ⁻¹ [in interfaces.canonical_names]
_ < _ [in interfaces.canonical_names]
_ ≫ _ [in interfaces.additional_operations]
_ * _ [in interfaces.canonical_names]
_ + _ [in interfaces.canonical_names]
_ ≤ _ [in interfaces.canonical_names]
' _ [in interfaces.canonical_names]
(& _ ) [in interfaces.canonical_names]
(&) [in interfaces.canonical_names]
( _ &) [in interfaces.canonical_names]
( _ ≡) [in interfaces.canonical_names]
( _ =) [in interfaces.canonical_names]
( _ *.) [in interfaces.canonical_names]
( _ ≢) [in interfaces.canonical_names]
( _ <) [in interfaces.canonical_names]
( _ ≪) [in interfaces.additional_operations]
( _ ◎) [in interfaces.canonical_names]
( _ +) [in interfaces.canonical_names]
( _ ⪥) [in interfaces.canonical_names]
( _ ·) [in interfaces.vectorspace]
( _ ^) [in interfaces.additional_operations]
( _ ≤) [in interfaces.canonical_names]
( _ ≠) [in interfaces.canonical_names]
(+ _ ) [in interfaces.canonical_names]
(+) [in interfaces.canonical_names]
(-) [in interfaces.canonical_names]
(.* _ ) [in interfaces.canonical_names]
(.*.) [in interfaces.canonical_names]
(/) [in interfaces.canonical_names]
(//) [in interfaces.canonical_names]
(< _ ) [in interfaces.canonical_names]
(<) [in interfaces.canonical_names]
(= _ ) [in interfaces.canonical_names]
(=) [in interfaces.canonical_names]
(^ _ ) [in interfaces.additional_operations]
(^) [in interfaces.additional_operations]
(→) [in interfaces.canonical_names]
(∸) [in interfaces.additional_operations]
(≠ _ ) [in interfaces.canonical_names]
(≠) [in interfaces.canonical_names]
(≡ _ ) [in interfaces.canonical_names]
(≡) [in interfaces.canonical_names]
(≢ _ ) [in interfaces.canonical_names]
(≢) [in interfaces.canonical_names]
(≤ _ ) [in interfaces.canonical_names]
(≤) [in interfaces.canonical_names]
(≪ _ ) [in interfaces.additional_operations]
(≪) [in interfaces.additional_operations]
(≫) [in interfaces.additional_operations]
(◎ _ ) [in interfaces.canonical_names]
(◎) [in interfaces.canonical_names]
(⪥ _ ) [in interfaces.canonical_names]
(⪥) [in interfaces.canonical_names]
(· _ ) [in interfaces.vectorspace]
(·) [in interfaces.vectorspace]
- 3 [in interfaces.canonical_names]
- 2 [in interfaces.canonical_names]
- _ [in interfaces.canonical_names]
- 1 [in interfaces.canonical_names]
- 4 [in interfaces.canonical_names]
/ _ [in interfaces.canonical_names]
// _ [in interfaces.canonical_names]
0 [in interfaces.canonical_names]
1 [in interfaces.canonical_names]
2 [in interfaces.canonical_names]
3 [in interfaces.canonical_names]
4 [in interfaces.canonical_names]



Abbreviation Index

A

App [in theory.quote_monoid]
App [in theory.monoid_normalization]
Applied [in theory.monoid_normalization]
ArrowsAssociative [in interfaces.canonical_names]


C

carrier [in theory.ua_products]
carriers [in varieties.setoids]


D

DtoQ_slow' [in implementations.dyadics]
DtoQ_slow' [in implementations.dyadics]
DtoQ' [in implementations.dyadics]
DtoStdQ [in implementations.dyadics]
Dyadic [in implementations.dyadics]


E

E [in categories.empty]
eval [in theory.quote_monoid]
eval [in theory.monoid_normalization]


I

ith_obj [in categories.product]
i_to_r [in orders.integers]
i_to_r [in orders.rationals]
i_to_r [in orders.rationals]


L

ListPermutation [in implementations.ne_list]


M

msig [in theory.monoid_normalization]
msig [in theory.quote_monoid]


N

ne_list [in interfaces.ua_basic]
notations.ne_list [in implementations.ne_list]
n_to_sr [in orders.naturals]
n_to_sr [in orders.rationals]
n_to_sr [in implementations.natpair_integers]
n_to_sr [in implementations.natpair_integers]


O

Op [in theory.quote_monoid]
Op [in theory.monoid_normalization]
OpenTerm [in varieties.open_terms]
OpType [in interfaces.universal_algebra]
OpType [in theory.ua_homomorphisms]
op_type [in theory.ua_congruence]


Q

QtoFrac [in theory.rationals]


S

StdQ [in implementations.dyadics]
StdQtoQ [in implementations.dyadics]


T

TargetObject [in theory.forget_algebra]
Term [in theory.quote_monoid]
toR [in implementations.peano_naturals]


U

uaTerm [in theory.monoid_normalization]


V

vv [in theory.ua_congruence]


X

x [in varieties.monoids]
x [in varieties.semirings]
x [in varieties.groups]
x [in varieties.semigroups]
x [in varieties.rings]
x' [in theory.naturals]


Y

y [in varieties.groups]
y [in varieties.semirings]
y [in varieties.rings]
y [in varieties.semigroups]
y [in varieties.monoids]
y' [in theory.naturals]


Z

z [in varieties.rings]
z [in varieties.monoids]
Z [in implementations.natpair_integers]
z [in varieties.groups]
z [in varieties.semigroups]
z [in varieties.semirings]
ZtoQ [in theory.rationals]
ZtoStdQ [in implementations.dyadics]
z_to_r [in implementations.natpair_integers]
z' [in theory.naturals]


other

Φ [in theory.ua_congruence]



Inductive Index

A

Abs [in interfaces.canonical_names]
AlgebraOps [in interfaces.ua_basic]
AntiSymmetric [in interfaces.canonical_names]
Apart [in interfaces.canonical_names]
Applied [in theory.ua_packed]
Arguments [in theory.ua_packed]
Arrows [in interfaces.canonical_names]
Associative [in interfaces.canonical_names]


B

Biinduction [in interfaces.canonical_names]


C

CatComp [in interfaces.canonical_names]
CatId [in interfaces.canonical_names]
Coerce [in interfaces.canonical_names]
Commutative [in interfaces.canonical_names]
CoTransitive [in interfaces.canonical_names]
CutMinus [in interfaces.additional_operations]


D

Decision [in interfaces.canonical_names]
DecMultInv [in interfaces.canonical_names]
DecreasingNonNegative [in theory.series]
DivEuclid [in interfaces.additional_operations]


E

e [in varieties.closed_terms]
ee [in varieties.open_terms]
ElimProduct [in theory.categories]
Equiv [in interfaces.canonical_names]
ExtendToSeq [in interfaces.sequences]


F

Fmap [in interfaces.functors]
ForAllIf [in theory.streams]


G

GroupInv [in interfaces.canonical_names]


H

HasProducts [in theory.categories]
HeteroAssociative [in interfaces.canonical_names]
HeteroSymmetric [in interfaces.canonical_names]


I

IncreasingNonNegative [in theory.series]
Initial [in theory.categories]
InitialArrow [in theory.categories]
InjectToSeq [in interfaces.sequences]
IntAbs [in interfaces.integers]
IntAsNat [in interfaces.integers]
IntegersToRing [in interfaces.integers]
IntroProduct [in theory.categories]
Inverse [in interfaces.canonical_names]


L

L [in implementations.ne_list]
Laws [in varieties.monoids]
Laws [in varieties.rings]
Laws [in varieties.groups]
Laws [in varieties.semigroups]
Laws [in varieties.semirings]
Le [in interfaces.canonical_names]
LeftAbsorb [in interfaces.canonical_names]
LeftCancellation [in interfaces.abstract_algebra]
LeftHeteroDistribute [in interfaces.canonical_names]
LeftIdentity [in interfaces.canonical_names]
LeftInverse [in interfaces.canonical_names]
Lt [in interfaces.canonical_names]


M

ModEuclid [in interfaces.additional_operations]
MonadBind [in interfaces.monads]
MonadReturn [in interfaces.monads]
Mono [in theory.categories]
MonoidUnit [in interfaces.canonical_names]
MultInv [in interfaces.canonical_names]


N

NatDistance [in interfaces.naturals]
NaturalsToSemiRing [in interfaces.naturals]
NaturalTransformation [in theory.categories]
NonEmpty [in misc.util]
NoZeroDivisors [in interfaces.canonical_names]


O

Obvious [in misc.util]
op [in varieties.rings]
op [in varieties.groups]
op [in varieties.monoids]
op [in varieties.semigroups]
op [in varieties.semirings]


P

PosInf [in interfaces.canonical_names]
Pow [in interfaces.additional_operations]
Producer [in theory.categories]
Product [in theory.categories]
PropHolds [in misc.util]


R

R [in misc.JMrelation]
RalgebraAction [in interfaces.canonical_names]
RationalsToFrac [in interfaces.rationals]
RightAbsorb [in interfaces.canonical_names]
RightCancellation [in interfaces.abstract_algebra]
RightHeteroDistribute [in interfaces.canonical_names]
RightIdentity [in interfaces.canonical_names]
RightInverse [in interfaces.canonical_names]
RingMult [in interfaces.canonical_names]
RingMultInverse [in interfaces.canonical_names]
RingOne [in interfaces.canonical_names]
RingPlus [in interfaces.canonical_names]
RingUnit [in interfaces.canonical_names]
RingZero [in interfaces.canonical_names]


S

ScalarMult [in interfaces.vectorspace]
SemiGroupOp [in interfaces.canonical_names]
Setoid [in interfaces.abstract_algebra]
SFmap [in interfaces.functors]
ShiftL [in interfaces.additional_operations]
ShiftR [in interfaces.additional_operations]
simple.approach_A.Quote [in quote.classquote]
simple.Expr [in quote.classquote]
Stable [in misc.util]
Statement [in interfaces.universal_algebra]
Stream_eq_coind [in theory.streams]
StrongLeftCancellation [in interfaces.abstract_algebra]
StrongRightCancellation [in interfaces.abstract_algebra]


T

Term [in interfaces.universal_algebra]
Term [in theory.monoid_normalization]
TotalRelation [in interfaces.canonical_names]
Trichotomy [in interfaces.canonical_names]
TrivialApart [in interfaces.canonical_names]


U

UniversalArrow [in theory.categories]


W

with_vars.Obvious [in quote.classquote]
with_vars.Expr [in quote.classquote]


Z

ZeroDivisor [in interfaces.canonical_names]
ZeroProduct [in interfaces.canonical_names]



Definition Index

A

abs [in interfaces.canonical_names]
all [in implementations.polynomials]
ApartZero [in interfaces.canonical_names]
app [in implementations.ne_list]
applications [in interfaces.universal_algebra]
apply_args [in theory.ua_packed]
app_tree [in interfaces.universal_algebra]
app_tree [in varieties.closed_terms]
app_tree [in varieties.open_terms]
arrow [in categories.varieties]
arrow [in categories.algebras]
associativity_arrows [in categories.categories]


B

back [in theory.ua_congruence]
better_args [in theory.ua_packed]
better_Applied_rect [in theory.ua_packed]
bool_decide_rel [in misc.util]
bool_decide [in misc.util]
boring_eval_entailment [in interfaces.universal_algebra]


C

carrier [in theory.ua_products]
carrier [in theory.ua_subalgebra]
carrier [in theory.ua_subalgebraT]
close [in interfaces.universal_algebra]
close_op [in theory.ua_subalgebraT]
close_op [in theory.ua_subalgebra]
close_op_proper [in theory.ua_subalgebraT]
close_op_proper [in theory.ua_subalgebra]
concat [in implementations.cons_list]
curry [in theory.ua_packed]
curry_decode [in theory.ua_packed]
curry_decode0 [in theory.ua_packed]


D

decide_rel [in misc.util]
decode [in theory.ua_packed]
decode0 [in theory.ua_packed]
dec_lt [in orders.orders]
DN [in misc.util]
dnn_Str_nth [in theory.series]
DtoQ [in implementations.dyadics]
DtoQ_slow [in implementations.dyadics]


E

e [in categories.product]
Empty_map [in categories.empty]
entailment_as_conjunctive_statement [in interfaces.universal_algebra]
entailment_as_statement [in interfaces.universal_algebra]
EqEntailment [in interfaces.universal_algebra]
eval [in interfaces.universal_algebra]
eval_in_other [in varieties.closed_terms]
eval_quote' [in theory.quote_monoid]
eval_stmt [in interfaces.universal_algebra]
EventuallyForAll [in theory.streams]
everyOther [in theory.series]
ex [in theory.quote_monoid]
ext_equiv [in interfaces.canonical_names]


F

factor [in categories.product]
factorials [in theory.series]
factorials_help [in theory.series]
fac_help [in theory.series]
fmap_op [in categories.dual]
fold [in interfaces.sequences]
foldr [in implementations.ne_list]
foldr1 [in implementations.ne_list]
forallArgs [in theory.ua_packed]
forallSplit [in theory.ua_packed]
forget [in varieties.semigroups]
forget [in varieties.monoids]
forget [in varieties.groups]
forget [in theory.forget_variety]
forth [in theory.ua_congruence]
Frac_lift [in implementations.field_of_fractions]
from_stdlib_semiring_theory [in theory.rings]
from_ua [in theory.monoid_normalization]
from_stdlib_field_theory [in theory.dec_fields]
from_stdlib_ring_theory [in theory.rings]


G

g [in implementations.natpair_integers]
geneq [in theory.ua_term_monad]
gen_bind [in theory.ua_term_monad]


H

head [in implementations.ne_list]
head_arg [in theory.ua_packed]
heq [in theory.ua_subvariety]
homFrom [in theory.hom_functor]


I

Identity [in interfaces.universal_algebra]
identity_as_eq [in interfaces.universal_algebra]
identity_as_entailment [in interfaces.universal_algebra]
Identity0 [in interfaces.universal_algebra]
id_lr_arrows [in categories.categories]
id_nat_trans [in theory.categories]
iffT [in misc.util]
image [in theory.ua_congruence]
initial [in theory.categories]
internal_simplify [in theory.monoid_normalization]
int_abs [in interfaces.integers]
in_domain [in theory.ua_congruence]
iso [in theory.categories]
isos_unique [in theory.categories]
isoT [in theory.categories]
iso_arrows [in theory.categories]
is_iso [in theory.categories]
is_ne_0 [in theory.rings]
is_nonneg [in theory.rings]
is_pos [in theory.rings]
is_sole [in misc.util]


K

kernel [in theory.ring_ideals]


L

last [in implementations.ne_list]
Laws [in varieties.setoids]
Laws [in varieties.empty]
liftM2 [in theory.monads]
lt_dec [in orders.orders]
lt_dec_slow [in orders.orders]


M

M [in theory.ua_term_monad]
map [in implementations.ne_list]
map_var [in interfaces.universal_algebra]
map_op [in theory.ua_mapped_operations]
map_setoid [in theory.functors]
max [in orders.minmax]
measure [in theory.monoid_normalization]
merge [in theory.quote_monoid]
min [in orders.minmax]
mkIdentity0 [in interfaces.universal_algebra]
morph [in varieties.closed_terms]
mult_Streams [in theory.series]


N

natural_initial_arrow [in interfaces.naturals]
nat_distance [in interfaces.naturals]
NonNeg [in interfaces.canonical_names]
NonPos [in interfaces.canonical_names]
NonZero_inject [in implementations.nonzero_field_elements]
novars [in theory.quote_monoid]
no_vars [in interfaces.universal_algebra]
Npair_to_Z [in implementations.stdlib_binary_integers]
nqe [in theory.ua_products]


O

object [in varieties.monoids]
Object [in varieties.empty]
object [in varieties.setoids]
Object [in varieties.semigroups]
object [in varieties.rings]
object [in theory.forget_algebra]
object [in varieties.groups]
object [in varieties.semirings]
Object [in varieties.rings]
object [in varieties.semigroups]
object [in varieties.empty]
Object [in categories.product]
Object [in varieties.monoids]
Object [in varieties.groups]
Object [in varieties.semirings]
of_nat [in implementations.nonneg_integers_naturals]
op [in varieties.empty]
op [in varieties.setoids]
OpenTerm0 [in varieties.open_terms]
OpType [in interfaces.ua_basic]
op_type_equiv [in interfaces.ua_basic]
op_closed [in theory.ua_subalgebra]
op_type [in interfaces.ua_basic]
op_closed_proper [in theory.ua_subalgebraT]
op_closed [in theory.ua_subalgebraT]


P

Permutation [in implementations.ne_list]
PofSplit [in theory.ua_packed]
pointwise_dependent_relation [in misc.util]
poly [in implementations.polynomials]
poly_eq_zero [in implementations.polynomials]
poly_constant [in implementations.polynomials]
poly_mult_cr [in implementations.polynomials]
Pos [in interfaces.canonical_names]
posh_free [in interfaces.sequences]
posh_inject [in interfaces.sequences]
posh_extend [in interfaces.sequences]
positives [in theory.series]
positives_help [in theory.series]
powers [in theory.series]
powers_help [in theory.series]
Preservation [in theory.ua_homomorphisms]
product [in theory.sequences]
prod_equiv [in theory.setoids]
proj [in theory.ua_subalgebra]
project [in categories.product]
proper_arrows [in categories.categories]
Pvars [in theory.ua_subvariety]


Q

quote' [in theory.quote_monoid]
quot_obj [in theory.ua_congruence]


R

rationals_to_rationals [in theory.rationals]
rec_impl [in theory.ua_products]
refl_arrows [in theory.categories]
replicate_Sn [in implementations.ne_list]
result [in interfaces.ua_basic]
retract_is_int_to_ring [in theory.integers]
retract_is_nat [in theory.naturals]
retract_is_int [in theory.integers]
retract_is_nat_to_sr [in theory.naturals]


S

sig [in varieties.semirings]
sig [in varieties.monoids]
sig [in varieties.setoids]
sig [in varieties.empty]
sig [in varieties.semigroups]
sig [in varieties.rings]
sig [in varieties.groups]
sigT_equiv [in interfaces.canonical_names]
sig_apart [in interfaces.canonical_names]
sig_equiv [in interfaces.canonical_names]
simple.eval [in quote.classquote]
simplify [in theory.monoid_normalization]
singlevar [in theory.quote_monoid]
single_sorted_signature [in interfaces.ua_basic]
sort [in orders.minmax]
stdlib_field_theory [in theory.dec_fields]
subobject [in theory.ua_congruence]
sum [in theory.sequences]
sym_arrows [in categories.categories]


T

T [in interfaces.universal_algebra]
tail [in implementations.ne_list]
tails [in implementations.ne_list]
tail_args [in theory.ua_packed]
take [in implementations.ne_list]
Term0 [in interfaces.universal_algebra]
theory [in varieties.monoids]
theory [in varieties.setoids]
theory [in varieties.groups]
theory [in varieties.semigroups]
theory [in varieties.rings]
theory [in varieties.empty]
theory [in varieties.semirings]
the_object [in varieties.closed_terms]
the_object [in varieties.open_terms]
the_arrow [in varieties.closed_terms]
to_ua [in theory.monoid_normalization]
to_list [in implementations.ne_list]
trans_arrows [in categories.categories]
T0 [in interfaces.universal_algebra]


U

uncurry [in misc.util]
univwit [in theory.adjunctions]


V

Vars [in interfaces.universal_algebra]
Vars [in theory.quote_monoid]


W

with_vars.novars [in quote.classquote]
with_vars.eval_quote' [in quote.classquote]
with_vars.Vars [in quote.classquote]
with_vars.eval [in quote.classquote]
with_vars.quote' [in quote.classquote]
with_vars.map_var [in quote.classquote]
with_vars.Value [in quote.classquote]
with_vars.merge [in quote.classquote]
with_vars.singlevar [in quote.classquote]



Module Index

B

bad [in interfaces.naturals]
BigN_Integers [in implementations.fast_naturals]
BigQ_Rationals [in implementations.fast_rationals]
BigZ_Integers [in implementations.fast_integers]


N

notations [in interfaces.universal_algebra]
notations [in implementations.ne_list]
NType_Integers.axioms [in implementations.NType_naturals]
NType_Integers [in implementations.NType_naturals]


O

op_type_notations [in interfaces.universal_algebra]


Q

QType_Rationals [in implementations.QType_rationals]
QType_Rationals.props [in implementations.QType_rationals]


S

simple [in quote.classquote]
simple.approach_B [in quote.classquote]
simple.approach_A [in quote.classquote]


U

ua [in theory.quote_monoid]
ua [in interfaces.sequences]


W

with_vars [in quote.classquote]


Z

ZType_Integers.axioms [in implementations.ZType_integers]
ZType_Integers [in implementations.ZType_integers]



Variable Index

A

algebras.u [in theory.ua_products]


C

carriers [in varieties.empty]
contents.ab_ba [in theory.ua_transference]
contents.ab_proper [in theory.ua_transference]
contents.arrow_setoid.e_trans [in categories.functors]
contents.arrow_setoid.e_sym [in categories.functors]
contents.arrow_setoid.e_refl [in categories.functors]
contents.associativity.a [in categories.categories]
contents.associativity.b [in categories.categories]
contents.associativity.c [in categories.categories]
contents.associativity.w [in categories.categories]
contents.associativity.x [in categories.categories]
contents.associativity.y [in categories.categories]
contents.associativity.z [in categories.categories]
contents.ba_proper [in theory.ua_transference]
contents.ba_ab [in theory.ua_transference]
contents.borrowed_from_nat.two_vars [in theory.naturals]
contents.borrowed_from_nat.three_vars [in theory.naturals]
contents.borrowed_from_nat.no_vars [in theory.naturals]
contents.ClosedTerm [in varieties.closed_terms]
contents.ClosedTerm0 [in varieties.closed_terms]
contents.epA [in theory.ua_transference]
contents.epB [in theory.ua_transference]
contents.et [in categories.varieties]
contents.et [in varieties.open_terms]
contents.et [in theory.forget_variety]
contents.et [in varieties.closed_terms]
contents.factors.C [in categories.product]
contents.factors.ith_functor [in categories.product]
contents.factors.X [in categories.product]
contents.for_nice_e.eAlgebra [in theory.ua_congruence]
contents.for_another_ring.preserves_1 [in implementations.natpair_integers]
contents.for_nice_e.lifted_normal [in theory.ua_congruence]
contents.for_another_ring.preserves_mult [in implementations.natpair_integers]
contents.for_another_ring.preserves_0 [in implementations.natpair_integers]
contents.for_another_object.other [in varieties.closed_terms]
contents.for_nice_e.lifted_e [in theory.ua_congruence]
contents.for_nice_e.Q [in theory.ua_congruence]
contents.for_another_ring.preserves_plus [in implementations.natpair_integers]
contents.for_nice_e.eSub [in theory.ua_congruence]
contents.hint [in theory.ua_congruence]
contents.hintje [in theory.forget_algebra]
contents.hint' [in theory.ua_congruence]
contents.more_arrows.e_trans [in categories.JMcat]
contents.more_arrows.e_sym [in categories.categories]
contents.more_arrows.e_sym [in categories.JMcat]
contents.more_arrows.e_trans [in categories.categories]
contents.more_arrows.e_refl [in categories.JMcat]
contents.more_arrows.e_refl [in categories.categories]
contents.obj_iso [in categories.categories]
contents.product_object [in categories.product]
contents.sig [in varieties.open_terms]
contents.sign [in theory.ua_term_monad]
contents.sign [in categories.algebras]
contents.sign [in theory.forget_algebra]
contents.Sorts [in theory.ua_mapped_operations]
contents.structural_eq [in varieties.open_terms]
contents.structural_eq [in varieties.closed_terms]
contents.TargetArrows [in theory.forget_algebra]
contents.σ [in theory.ua_homomorphisms]


F

for_another_semiring.f_preserves_plus [in implementations.peano_naturals]
for_φAdjunction.η [in theory.adjunctions]
for_φAdjunction.hint' [in theory.adjunctions]
for_signature.σ [in interfaces.universal_algebra]
for_φAdjunction.hint'' [in theory.adjunctions]
for_φAdjunction.ε [in theory.adjunctions]
for_another_semiring.f_preserves_mult [in implementations.peano_naturals]
for_ηAdjunction.hint [in theory.adjunctions]
for_ηεAdjunction.hint [in theory.adjunctions]
for_φAdjunction.hint''' [in theory.adjunctions]
for_ηAdjunction.hint' [in theory.adjunctions]
for_ηεAdjunction.hint'''' [in theory.adjunctions]
for_φAdjunction.hint''''' [in theory.adjunctions]
for_ηεAdjunction.hint' [in theory.adjunctions]
for_ηAdjunction.hint'' [in theory.adjunctions]
for_ηεAdjunction.hint''''' [in theory.adjunctions]
for_another_semiring.f_preserves_0 [in implementations.peano_naturals]
for_ηεAdjunction.hint'' [in theory.adjunctions]
for_φAdjunction.hint'''' [in theory.adjunctions]
for_ηAdjunction.hint''' [in theory.adjunctions]
for_ηεAdjunction.hint''' [in theory.adjunctions]
for_ηεAdjunction.φ [in theory.adjunctions]
for_φAdjunction.hint [in theory.adjunctions]
for_ηAdjunction.φ [in theory.adjunctions]
for_another_semiring.f_preserves_1 [in implementations.peano_naturals]


I

ideal_congruence.hint [in theory.ring_ideals]
ideal_congruence.ideal [in theory.ring_ideals]
initial_maps.Int [in interfaces.integers]
initial_maps.A [in interfaces.naturals]
integers_order.another_ring.f_preserves_nonneg [in orders.integers]
integers_order.another_ring.f_preserves_nonneg_back [in orders.integers]


P

product.product [in theory.setoids]


R

rationals_and_another_rationals.f_preserves_nonneg [in orders.rationals]


S

semiring_pairs.SRpair_mult_proper_r [in implementations.semiring_pairs]
shiftl.shiftl_strict_order_embedding [in theory.shiftl]


V

varieties.carrier_e [in theory.ua_products]


W

with_sorts.Sorts [in interfaces.ua_basic]
with_vars.inspect.x [in quote.classquote]
with_vars.inspect.y [in quote.classquote]
with_sorts.carrier [in interfaces.ua_basic]



Library Index

A

abs
abstract_algebra
additional_operations
adjunctions
algebras


C

canonical_names
categories
categories
classquote
closed_terms
cons_list
cut_minus


D

dec_fields
dec_fields
dual
dyadics


E

empty
empty


F

fast_integers
fast_rationals
fast_naturals
fields
field_of_fractions
forget_variety
forget_algebra
functors
functors
functors


G

groups
groups


H

hom_functor


I

integers
integers
integers
intfrac_rationals
int_abs
int_pow


J

jections
JMcat
JMrelation


M

maps
minmax
monads
monads
monoids
monoid_normalization


N

natpair_integers
naturals
naturals
naturals
nat_pow
nat_distance
ne_list
nonneg_integers_naturals
nonneg_semiring_elements
nonzero_field_elements
NType_naturals


O

open_terms
orders
orders


P

peano_naturals
polynomials
positive_semiring_elements
product


Q

QType_rationals
quote_monoid


R

rationals
rationals
rationals
rings
rings
rings
ring_ideals


S

semigroups
semirings
semirings
semiring_pairs
sequences
sequences
series
setoids
setoids
setoids
setoid_tactics
shiftl
stdlib_binary_integers
stdlib_rationals
stdlib_binary_naturals
streams
strong_setoids


U

ua_term_monad
ua_packed
ua_mapped_operations
ua_congruence
ua_subvariety
ua_subalgebra
ua_basic
ua_products
ua_homomorphisms
ua_transference
ua_subalgebraT
unit
universal_algebra
util


V

varieties
vectorspace


W

workarounds
workaround_tactics


Z

ZType_integers



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 (2748 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 (464 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 (376 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 (175 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 (546 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 (261 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 (183 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 (103 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 (64 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 (111 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 (237 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 (19 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 (100 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 (109 entries)

This page has been generated by coqdoc