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) |