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 (69505 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 (1943 entries)
Binder 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 (39748 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 (379 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 (3958 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 (91 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 (13542 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 (480 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 (45 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 (134 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 (452 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 (1344 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 (1014 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 (6127 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 (248 entries)

M (notation)

_ ^f (ring_scope) [in mathcomp.algebra.mxpoly]
_ ^f (ring_scope) [in mathcomp.algebra.matrix]
_ ^f (ring_scope) [in mathcomp.algebra.poly]
_ ^f (ring_scope) [in mathcomp.algebra.mxpoly]
_ ^f (ring_scope) [in mathcomp.algebra.mxalgebra]
_ ^f (ring_scope) [in mathcomp.algebra.matrix]
_ ^f (ring_scope) [in mathcomp.algebra.poly]
_ ^f (ring_scope) [in mathcomp.algebra.poly]
_ ^f (ring_scope) [in mathcomp.algebra.poly]
_ ^f (ring_scope) [in mathcomp.algebra.matrix]
_ ^f (ring_scope) [in mathcomp.algebra.mxpoly]
_ ^f (ring_scope) [in mathcomp.algebra.matrix]
_ *m: _ (ring_scope) [in mathcomp.algebra.matrix]
_ %:M (ring_scope) [in mathcomp.algebra.matrix]
\tr _ (ring_scope) [in mathcomp.algebra.matrix]
'Z ( _ ) (matrix_set_scope) [in mathcomp.algebra.mxalgebra]
'C ( _ ) (matrix_set_scope) [in mathcomp.algebra.mxalgebra]
_ * _ (matrix_set_scope) [in mathcomp.algebra.mxalgebra]
\tr _ (ring_scope) [in mathcomp.algebra.matrix]
_ *m _ (ring_scope) [in mathcomp.algebra.matrix]
_ %:M (ring_scope) [in mathcomp.algebra.matrix]
_ \in _ [in mathcomp.algebra.mxalgebra]
_ ^T (ring_scope) [in mathcomp.algebra.matrix]
_ <= _ ?< if _ (ring_scope) [in mathcomp.algebra.interval]
[ arg maxr_ ( _ > _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
[ arg maxr_ ( _ > _ in _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
[ arg maxr_ ( _ > _ | _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
[ arg minr_ ( _ < _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
[ arg minr_ ( _ < _ in _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
[ arg minr_ ( _ < _ | _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
@ lerif_rootC_AGM (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_Re_Creal (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_normC_Re_Creal (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_AGM2 (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_mean_square (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_AGM2_scaled (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_mean_square_scaled (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_AGM (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_lerif_AGM2 (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_lerif_mean_square (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_AGM_scaled (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_lerif_AGM2_scaled (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_lerif_mean_square_scaled (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_pprod (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_nmul (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_pmul (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_lerif_norm (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_0_sum (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_sum (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_add (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_subRL (fun_scope) [in mathcomp.algebra.ssrnum]
@ lerif_subLR (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_ltrgt0P (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_ger0P (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_ltrgtP (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_lerNgt (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_ltrNge (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_ltrP (fun_scope) [in mathcomp.algebra.ssrnum]
@ real_lerP (fun_scope) [in mathcomp.algebra.ssrnum]
`| _ | (ring_scope) [in mathcomp.algebra.ssrnum]
_ * _ [in mathcomp.ssreflect.bigop]
*%M [in mathcomp.ssreflect.bigop]
_ * _ [in mathcomp.ssreflect.bigop]
*%M [in mathcomp.ssreflect.bigop]
1 [in mathcomp.ssreflect.bigop]
[ add_law _ of _ ] (form_scope) [in mathcomp.ssreflect.bigop]
[ mul_law of _ ] (form_scope) [in mathcomp.ssreflect.bigop]
[ com_law of _ ] (form_scope) [in mathcomp.ssreflect.bigop]
[ law of _ ] (form_scope) [in mathcomp.ssreflect.bigop]
@ mulm_addr (fun_scope) [in mathcomp.ssreflect.bigop]
@ mulm_addl (fun_scope) [in mathcomp.ssreflect.bigop]
_ ^f [in mathcomp.algebra.ssrint]
_ ^ _ [in mathcomp.algebra.matrix]



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 (69505 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 (1943 entries)
Binder 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 (39748 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 (379 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 (3958 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 (91 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 (13542 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 (480 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 (45 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 (134 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 (452 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 (1344 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 (1014 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 (6127 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 (248 entries)