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 (3486 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 (293 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 (51 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 (312 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 (100 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 (435 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 (611 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (149 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 (99 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 (76 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 (117 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 (111 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 (108 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 (962 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 (62 entries)

P (lemma)

pair_equal_spec [in Corelib.Init.Datatypes]
pair_andP [in Corelib.ssr.ssrbool]
PartialOrder_inverse [in Corelib.Classes.RelationClasses]
PartialOrder_StrictOrder [in Corelib.Classes.CMorphisms]
PartialOrder_StrictOrder [in Corelib.Classes.Morphisms]
PartialOrder_inverse [in Corelib.Classes.CRelationClasses]
pcan_in_comp [in Corelib.ssr.ssrbool]
pcan_in_inj [in Corelib.ssr.ssrbool]
pcan_pcomp [in Corelib.ssr.ssrfun]
pcan_inj [in Corelib.ssr.ssrfun]
plus_Sn_m [in Corelib.Init.Peano]
plus_n_Sm [in Corelib.Init.Peano]
plus_O_n [in Corelib.Init.Peano]
plus_n_O [in Corelib.Init.Peano]
pointwise_pointwise [in Corelib.Classes.CMorphisms]
pointwise_pointwise [in Corelib.Classes.Morphisms]
pred_Sn [in Corelib.Init.Peano]
Prim2SF_inj [in Corelib.Floats.FloatAxioms]
prod_sigT_prod [in Corelib.Init.Specif]
proj1 [in Corelib.Init.Logic]
proj2 [in Corelib.Init.Logic]
proper_sym_arrow_iffT_2 [in Corelib.Classes.CMorphisms]
proper_sym_impl_iff_2 [in Corelib.Classes.CMorphisms]
proper_sym_arrow_iffT [in Corelib.Classes.CMorphisms]
proper_sym_impl_iff [in Corelib.Classes.CMorphisms]
proper_sym_flip_2 [in Corelib.Classes.CMorphisms]
proper_sym_flip [in Corelib.Classes.CMorphisms]
proper_normalizes_proper [in Corelib.Classes.CMorphisms]
proper_eq [in Corelib.Classes.CMorphisms]
proper_proper_proxy [in Corelib.Classes.CMorphisms]
proper_sym_impl_iff_2 [in Corelib.Classes.Morphisms]
proper_sym_impl_iff [in Corelib.Classes.Morphisms]
proper_sym_flip_2 [in Corelib.Classes.Morphisms]
proper_sym_flip [in Corelib.Classes.Morphisms]
proper_normalizes_proper [in Corelib.Classes.Morphisms]
proper_eq [in Corelib.Classes.Morphisms]
proper_proper_proxy [in Corelib.Classes.Morphisms]
prop_congr [in Corelib.ssr.ssrbool]



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 (3486 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 (293 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 (51 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 (312 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 (100 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 (435 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 (611 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (149 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 (99 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 (76 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 (117 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 (111 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 (108 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 (962 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 (62 entries)