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

## other

'M[ _ ] ( _ ) (abelem_scope) [notation, in mathcomp.character.mxabelem]'rV[ _ ] ( _ ) (abelem_scope) [notation, in mathcomp.character.mxabelem]

'M ( _ ) (abelem_scope) [notation, in mathcomp.character.mxabelem]

'rV ( _ ) (abelem_scope) [notation, in mathcomp.character.mxabelem]

'dim _ (abelem_scope) [notation, in mathcomp.character.mxabelem]

_ * _ (action_scope) [notation, in mathcomp.solvable.primitive_action]

[ Aut _ ] (action_scope) [notation, in mathcomp.fingroup.action]

'Q (action_scope) [notation, in mathcomp.fingroup.action]

'JG (action_scope) [notation, in mathcomp.fingroup.action]

'Js (action_scope) [notation, in mathcomp.fingroup.action]

'J (action_scope) [notation, in mathcomp.fingroup.action]

'Rs (action_scope) [notation, in mathcomp.fingroup.action]

'R (action_scope) [notation, in mathcomp.fingroup.action]

'P (action_scope) [notation, in mathcomp.fingroup.action]

_ \o _ (action_scope) [notation, in mathcomp.fingroup.action]

<< _ >> (action_scope) [notation, in mathcomp.fingroup.action]

_ %% _ (action_scope) [notation, in mathcomp.fingroup.action]

_ / _ (action_scope) [notation, in mathcomp.fingroup.action]

_ ^? (action_scope) [notation, in mathcomp.fingroup.action]

<[ _ ] > (action_scope) [notation, in mathcomp.fingroup.action]

_ \ _ (action_scope) [notation, in mathcomp.fingroup.action]

_ ^* (action_scope) [notation, in mathcomp.fingroup.action]

'Zm (action_scope) [notation, in mathcomp.character.mxabelem]

'MR _ (action_scope) [notation, in mathcomp.character.mxabelem]

'Cl (action_scope) [notation, in mathcomp.character.mxrepresentation]

'U (action_scope) [notation, in mathcomp.algebra.finalg]

_ != _ %[mod _ ] (algC_scope) [notation, in mathcomp.field.algnum]

_ == _ %[mod _ ] (algC_scope) [notation, in mathcomp.field.algnum]

_ %| _ (algC_scope) [notation, in mathcomp.field.algnum]

_ %| _ (algC_expanded_scope) [notation, in mathcomp.field.algnum]

_ @: _ (aspace_scope) [notation, in mathcomp.field.fieldext]

_ * _ (aspace_scope) [notation, in mathcomp.field.fieldext]

'C_ ( _ ) ( _ ) (aspace_scope) [notation, in mathcomp.field.fieldext]

'C_ _ ( _ ) (aspace_scope) [notation, in mathcomp.field.fieldext]

'C_ ( _ ) [ _ ] (aspace_scope) [notation, in mathcomp.field.fieldext]

'C_ _ [ _ ] (aspace_scope) [notation, in mathcomp.field.fieldext]

_ :&: _ (aspace_scope) [notation, in mathcomp.field.fieldext]

<< _ ; _ >> (aspace_scope) [notation, in mathcomp.field.falgebra]

<< _ & _ >> (aspace_scope) [notation, in mathcomp.field.falgebra]

<< _ >> (aspace_scope) [notation, in mathcomp.field.falgebra]

'Z ( _ ) (aspace_scope) [notation, in mathcomp.field.falgebra]

'C ( _ ) (aspace_scope) [notation, in mathcomp.field.falgebra]

'C [ _ ] (aspace_scope) [notation, in mathcomp.field.falgebra]

{ : _ } (aspace_scope) [notation, in mathcomp.field.falgebra]

1 (aspace_scope) [notation, in mathcomp.field.falgebra]

\big [ _ / _ ]_ ( _ in _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ in _ | _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ < _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ < _ | _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ : _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ : _ | _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ _ _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ | _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ <= _ < _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ <= _ < _ | _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ <- _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

\big [ _ / _ ]_ ( _ <- _ | _ ) _ (big_scope) [notation, in mathcomp.ssreflect.bigop]

_ \proper _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]

_ \subset _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]

[ disjoint _ & _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]

_ != _ :> _ (bool_scope) [notation, in mathcomp.ssreflect.eqtype]

_ != _ (bool_scope) [notation, in mathcomp.ssreflect.eqtype]

_ == _ :> _ (bool_scope) [notation, in mathcomp.ssreflect.eqtype]

_ == _ (bool_scope) [notation, in mathcomp.ssreflect.eqtype]

_ ^: _ (cfun_scope) [notation, in mathcomp.character.inertia]

_ ^ _ (cfun_scope) [notation, in mathcomp.character.inertia]

_ %% _ (cfun_scope) [notation, in mathcomp.character.classfun]

_ / _ (cfun_scope) [notation, in mathcomp.character.classfun]

#[ _ ] (cfun_scope) [notation, in mathcomp.character.classfun]

_ ^* (cfun_scope) [notation, in mathcomp.character.classfun]

1 (cfun_scope) [notation, in mathcomp.character.classfun]

'Z ( _ ) (cfun_scope) [notation, in mathcomp.character.character]

'o ( _ ) (cfun_scope) [notation, in mathcomp.character.character]

_ .[ _ ] (cfun_scope) [notation, in mathcomp.character.character]

_ > _ (coq_nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ >= _ (coq_nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ < _ (coq_nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ <= _ (coq_nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ * _ (coq_nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ - _ (coq_nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ + _ (coq_nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

#[ _ ] (C_scope) [notation, in mathcomp.field.algnum]

_ - _ (distn_scope) [notation, in mathcomp.algebra.ssrint]

_ =P _ :> _ (eq_scope) [notation, in mathcomp.ssreflect.eqtype]

_ =P _ (eq_scope) [notation, in mathcomp.ssreflect.eqtype]

[ equiv_rel of _ ] (form_scope) [notation, in mathcomp.ssreflect.generic_quotient]

[ finMixin of _ by <:%/ ] (form_scope) [notation, in mathcomp.ssreflect.generic_quotient]

[ countMixin of _ by <:%/ ] (form_scope) [notation, in mathcomp.ssreflect.generic_quotient]

[ choiceMixin of _ by <:%/ ] (form_scope) [notation, in mathcomp.ssreflect.generic_quotient]

[ eqMixin of _ by <:%/ ] (form_scope) [notation, in mathcomp.ssreflect.generic_quotient]

[ subType _ of _ by %/ ] (form_scope) [notation, in mathcomp.ssreflect.generic_quotient]

[ eqQuotType _ of _ ] (form_scope) [notation, in mathcomp.ssreflect.generic_quotient]

[ quotType of _ ] (form_scope) [notation, in mathcomp.ssreflect.generic_quotient]

[ tuple _ | _ < _ ] (form_scope) [notation, in mathcomp.ssreflect.tuple]

[ tuple ] (form_scope) [notation, in mathcomp.ssreflect.tuple]

[ tuple _ ; .. ; _ ] (form_scope) [notation, in mathcomp.ssreflect.tuple]

[ tnth _ _ ] (form_scope) [notation, in mathcomp.ssreflect.tuple]

[ tuple of _ ] (form_scope) [notation, in mathcomp.ssreflect.tuple]

{ tuple _ of _ } (form_scope) [notation, in mathcomp.ssreflect.tuple]

[ <-> _ ; _ ; .. ; _ ] (form_scope) [notation, in mathcomp.ssreflect.seq]

[ subCountType of _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]

[ countMixin of _ by <: ] (form_scope) [notation, in mathcomp.ssreflect.choice]

[ choiceMixin of _ by <: ] (form_scope) [notation, in mathcomp.ssreflect.choice]

[ transitive ^ _ _ , on _ | _ ] (form_scope) [notation, in mathcomp.solvable.primitive_action]

[ primitive _ , on _ | _ ] (form_scope) [notation, in mathcomp.solvable.primitive_action]

[ unitRingQuotType _ & _ of _ ] (form_scope) [notation, in mathcomp.algebra.ring_quotient]

[ ringQuotType _ & _ of _ ] (form_scope) [notation, in mathcomp.algebra.ring_quotient]

[ zmodQuotType _ , _ & _ of _ ] (form_scope) [notation, in mathcomp.algebra.ring_quotient]

{ acts _ , on group _ | _ } (form_scope) [notation, in mathcomp.fingroup.action]

[ groupAction of _ ] (form_scope) [notation, in mathcomp.fingroup.action]

[ faithful _ , on _ | _ ] (form_scope) [notation, in mathcomp.fingroup.action]

[ transitive _ , on _ | _ ] (form_scope) [notation, in mathcomp.fingroup.action]

{ acts _ , on _ | _ } (form_scope) [notation, in mathcomp.fingroup.action]

[ acts _ , on _ | _ ] (form_scope) [notation, in mathcomp.fingroup.action]

[ action of _ ] (form_scope) [notation, in mathcomp.fingroup.action]

[ group of _ ] (form_scope) [notation, in mathcomp.fingroup.fingroup]

[ morphism of _ ] (form_scope) [notation, in mathcomp.fingroup.morphism]

[ morphism _ of _ ] (form_scope) [notation, in mathcomp.fingroup.morphism]

[ finMixin of _ by <: ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ subFinType of _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ : _ in _ | _ & _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ in _ | _ & _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ : _ in _ | _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ in _ | _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ : _ in _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ in _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ : _ | _ & _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ | _ & _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ : _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ : _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ : _ | _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ pick _ | _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]

[ eqMixin of _ by <: ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]

[ newType for _ by _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]

[ newType for _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]

[ newType for _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]

[ subType of _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]

[ subType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]

[ subType for _ by _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]

[ subType for _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]

[ subType for _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]

[ aspace of _ for _ ] (form_scope) [notation, in mathcomp.field.falgebra]

[ aspace of _ ] (form_scope) [notation, in mathcomp.field.falgebra]

@ coprime_expr (fun_scope) [notation, in mathcomp.ssreflect.div]

@ coprime_expl (fun_scope) [notation, in mathcomp.ssreflect.div]

@ coprimez_expr (fun_scope) [notation, in mathcomp.algebra.intdiv]

@ coprimez_expl (fun_scope) [notation, in mathcomp.algebra.intdiv]

@ itv_intersectionA (fun_scope) [notation, in mathcomp.algebra.interval]

@ itv_intersectionC (fun_scope) [notation, in mathcomp.algebra.interval]

@ itv_intersectionii (fun_scope) [notation, in mathcomp.algebra.interval]

@ itv_intersectioni1 (fun_scope) [notation, in mathcomp.algebra.interval]

@ itv_intersection1i (fun_scope) [notation, in mathcomp.algebra.interval]

@ itv_intersection (fun_scope) [notation, in mathcomp.algebra.interval]

@ sqrn_sub (fun_scope) [notation, in mathcomp.ssreflect.ssrnat]

@ odd_opp (fun_scope) [notation, in mathcomp.ssreflect.ssrnat]

@ iter_add (fun_scope) [notation, in mathcomp.ssreflect.ssrnat]

@ decr_inj_in (fun_scope) [notation, in mathcomp.ssreflect.ssrnat]

@ decr_inj (fun_scope) [notation, in mathcomp.ssreflect.ssrnat]

@ incr_inj_in (fun_scope) [notation, in mathcomp.ssreflect.ssrnat]

@ incr_inj (fun_scope) [notation, in mathcomp.ssreflect.ssrnat]

@ homo_inj_lt_in (fun_scope) [notation, in mathcomp.ssreflect.ssrnat]

@ homo_inj_lt (fun_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ .-support (fun_scope) [notation, in mathcomp.ssreflect.finfun]

[ ffun => _ ] (fun_scope) [notation, in mathcomp.ssreflect.finfun]

[ ffun _ => _ ] (fun_scope) [notation, in mathcomp.ssreflect.finfun]

[ ffun _ : _ => _ ] (fun_scope) [notation, in mathcomp.ssreflect.finfun]

@ map_mx_sub (fun_scope) [notation, in mathcomp.algebra.matrix]

@ scalar_mx_comm (fun_scope) [notation, in mathcomp.algebra.matrix]

_ ^* (fun_scope) [notation, in mathcomp.fingroup.action]

@ polyC_mulrz (fun_scope) [notation, in mathcomp.algebra.ssrint]

@ subseq_order_path (fun_scope) [notation, in mathcomp.ssreflect.path]

@ leq_index (fun_scope) [notation, in mathcomp.ssreflect.path]

@ ltn_index (fun_scope) [notation, in mathcomp.ssreflect.path]

@ sorted_le_nth (fun_scope) [notation, in mathcomp.ssreflect.path]

@ sorted_lt_nth (fun_scope) [notation, in mathcomp.ssreflect.path]

@ eq_sorted_irr (fun_scope) [notation, in mathcomp.ssreflect.path]

@ eq_sorted (fun_scope) [notation, in mathcomp.ssreflect.path]

@ primes_exp (fun_scope) [notation, in mathcomp.ssreflect.prime]

@ primes_mul (fun_scope) [notation, in mathcomp.ssreflect.prime]

[ rel _ _ in _ ] (fun_scope) [notation, in mathcomp.ssreflect.ssrbool]

[ rel _ _ in _ | _ ] (fun_scope) [notation, in mathcomp.ssreflect.ssrbool]

[ rel _ _ in _ & _ ] (fun_scope) [notation, in mathcomp.ssreflect.ssrbool]

[ rel _ _ in _ & _ | _ ] (fun_scope) [notation, in mathcomp.ssreflect.ssrbool]

[ rel _ _ : _ | _ ] (fun_scope) [notation, in mathcomp.ssreflect.ssrbool]

[ rel _ _ | _ ] (fun_scope) [notation, in mathcomp.ssreflect.ssrbool]

@ limg_add (fun_scope) [notation, in mathcomp.algebra.vector]

@ arg_maxP (fun_scope) [notation, in mathcomp.ssreflect.fintype]

@ arg_minP (fun_scope) [notation, in mathcomp.ssreflect.fintype]

@ derivn_sub (fun_scope) [notation, in mathcomp.algebra.poly]

@ lead_coef_opp (fun_scope) [notation, in mathcomp.algebra.poly]

@ polyC_inv (fun_scope) [notation, in mathcomp.algebra.poly]

@ polyC_mul (fun_scope) [notation, in mathcomp.algebra.poly]

@ polyC_muln (fun_scope) [notation, in mathcomp.algebra.poly]

@ polyC_sub (fun_scope) [notation, in mathcomp.algebra.poly]

@ polyC_opp (fun_scope) [notation, in mathcomp.algebra.poly]

@ polyC_add (fun_scope) [notation, in mathcomp.algebra.poly]

[ predX _ & _ ] (fun_scope) [notation, in mathcomp.ssreflect.eqtype]

[ eta _ with _ , .. , _ ] (fun_scope) [notation, in mathcomp.ssreflect.eqtype]

[ fun _ => _ with _ , .. , _ ] (fun_scope) [notation, in mathcomp.ssreflect.eqtype]

[ fun _ : _ => _ with _ , .. , _ ] (fun_scope) [notation, in mathcomp.ssreflect.eqtype]

_ |-> _ (fun_delta_scope) [notation, in mathcomp.ssreflect.eqtype]

[ predD1 _ & _ ] (fun_scope) [notation, in mathcomp.ssreflect.eqtype]

[ predU1 _ & _ ] (fun_scope) [notation, in mathcomp.ssreflect.eqtype]

@ mulsmx_addr (fun_scope) [notation, in mathcomp.algebra.mxalgebra]

@ mulsmx_addl (fun_scope) [notation, in mathcomp.algebra.mxalgebra]

_ %% _ (gFun_scope) [notation, in mathcomp.solvable.gfunctor]

_ \o _ (gFun_scope) [notation, in mathcomp.solvable.gfunctor]

[ Aut _ ] (groupAction_scope) [notation, in mathcomp.fingroup.action]

'Q (groupAction_scope) [notation, in mathcomp.fingroup.action]

'J (groupAction_scope) [notation, in mathcomp.fingroup.action]

_ \o _ (groupAction_scope) [notation, in mathcomp.fingroup.action]

_ %% _ (groupAction_scope) [notation, in mathcomp.fingroup.action]

_ / _ (groupAction_scope) [notation, in mathcomp.fingroup.action]

<[ _ ] > (groupAction_scope) [notation, in mathcomp.fingroup.action]

_ \ _ (groupAction_scope) [notation, in mathcomp.fingroup.action]

'Zm (groupAction_scope) [notation, in mathcomp.character.mxabelem]

'MR _ (groupAction_scope) [notation, in mathcomp.character.mxabelem]

'U (groupAction_scope) [notation, in mathcomp.algebra.finalg]

'Alt_ _ (Group_scope) [notation, in mathcomp.solvable.alt]

'Alt_ _ (group_scope) [notation, in mathcomp.solvable.alt]

'Sym_ _ (Group_scope) [notation, in mathcomp.solvable.alt]

'Sym_ _ (group_scope) [notation, in mathcomp.solvable.alt]

_ / _ (Group_scope) [notation, in mathcomp.fingroup.quotient]

_ / _ (group_scope) [notation, in mathcomp.fingroup.quotient]

'Z[ _ ] (group_scope) [notation, in mathcomp.character.vcharacter]

'Z[ _ , _ ] (group_scope) [notation, in mathcomp.character.vcharacter]

_ ^` ( _ ) (Group_scope) [notation, in mathcomp.solvable.commutator]

_ ^` ( _ ) (group_scope) [notation, in mathcomp.solvable.commutator]

'Gal ( _ / _ ) (Group_scope) [notation, in mathcomp.field.galois]

'Gal ( _ / _ ) (group_scope) [notation, in mathcomp.field.galois]

'GL_ _ ( _ ) (Group_scope) [notation, in mathcomp.algebra.matrix]

'GL_ _ [ _ ] (Group_scope) [notation, in mathcomp.algebra.matrix]

'GL_ _ ( _ ) (group_scope) [notation, in mathcomp.algebra.matrix]

'GL_ _ [ _ ] (group_scope) [notation, in mathcomp.algebra.matrix]

_ \char _ (group_scope) [notation, in mathcomp.fingroup.automorphism]

[ Aut _ ] (group_scope) [notation, in mathcomp.fingroup.automorphism]

[ Aut _ ] (Group_scope) [notation, in mathcomp.fingroup.automorphism]

'I_ _ [ _ ] (Group_scope) [notation, in mathcomp.character.inertia]

'I_ _ [ _ ] (group_scope) [notation, in mathcomp.character.inertia]

'I[ _ ] (Group_scope) [notation, in mathcomp.character.inertia]

'I[ _ ] (group_scope) [notation, in mathcomp.character.inertia]

'C_ ( _ | _ ) [ _ ] (Group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( | _ ) [ _ ] (Group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( _ | _ ) ( _ ) (Group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( | _ ) ( _ ) (Group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( _ | _ ) [ _ ] (group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( | _ ) [ _ ] (group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( _ | _ ) ( _ ) (group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( | _ ) ( _ ) (group_scope) [notation, in mathcomp.fingroup.action]

'N_ _ ( _ | _ ) (Group_scope) [notation, in mathcomp.fingroup.action]

'N ( _ | _ ) (Group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( _ ) [ _ | _ ] (Group_scope) [notation, in mathcomp.fingroup.action]

'C_ _ [ _ | _ ] (Group_scope) [notation, in mathcomp.fingroup.action]

'C [ _ | _ ] (Group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( _ ) ( _ | _ ) (Group_scope) [notation, in mathcomp.fingroup.action]

'C_ _ ( _ | _ ) (Group_scope) [notation, in mathcomp.fingroup.action]

'C ( _ | _ ) (Group_scope) [notation, in mathcomp.fingroup.action]

'N_ _ ( _ | _ ) (group_scope) [notation, in mathcomp.fingroup.action]

'N ( _ | _ ) (group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( _ ) [ _ | _ ] (group_scope) [notation, in mathcomp.fingroup.action]

'C_ _ [ _ | _ ] (group_scope) [notation, in mathcomp.fingroup.action]

'C [ _ | _ ] (group_scope) [notation, in mathcomp.fingroup.action]

'C_ ( _ ) ( _ | _ ) (group_scope) [notation, in mathcomp.fingroup.action]

'C_ _ ( _ | _ ) (group_scope) [notation, in mathcomp.fingroup.action]

'C ( _ | _ ) (group_scope) [notation, in mathcomp.fingroup.action]

'Fix_ ( _ | _ ) [ _ ] (group_scope) [notation, in mathcomp.fingroup.action]

'Fix_ _ [ _ ] (group_scope) [notation, in mathcomp.fingroup.action]

'Fix_ ( _ | _ ) ( _ ) (group_scope) [notation, in mathcomp.fingroup.action]

'Fix_ ( _ ) ( _ ) (group_scope) [notation, in mathcomp.fingroup.action]

'Fix_ _ ( _ ) (group_scope) [notation, in mathcomp.fingroup.action]

[ min _ | _ & _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ min _ of _ | _ & _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ min _ | _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ min _ of _ | _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ max _ | _ & _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ max _ of _ | _ & _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ max _ | _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ max _ of _ | _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

'C_ ( _ ) [ _ ] (Group_scope) [notation, in mathcomp.fingroup.fingroup]

'C_ _ [ _ ] (Group_scope) [notation, in mathcomp.fingroup.fingroup]

'C_ ( _ ) ( _ ) (Group_scope) [notation, in mathcomp.fingroup.fingroup]

'C_ _ ( _ ) (Group_scope) [notation, in mathcomp.fingroup.fingroup]

'N_ _ ( _ ) (Group_scope) [notation, in mathcomp.fingroup.fingroup]

'C [ _ ] (Group_scope) [notation, in mathcomp.fingroup.fingroup]

'C ( _ ) (Group_scope) [notation, in mathcomp.fingroup.fingroup]

'N ( _ ) (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ in _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ in _ | _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ < _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ < _ | _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ : _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ : _ | _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ _ _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ | _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ <= _ < _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ <= _ < _ | _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ <- _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ <- _ | _ ) _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

_ * _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

_ <*> _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

[ ~: _ , _ , .. , _ ] (Group_scope) [notation, in mathcomp.fingroup.fingroup]

<[ _ ] > (Group_scope) [notation, in mathcomp.fingroup.fingroup]

<< _ >> (Group_scope) [notation, in mathcomp.fingroup.fingroup]

_ :&: _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

[ subg _ ] (Group_scope) [notation, in mathcomp.fingroup.fingroup]

[ subg _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ :^ _ (Group_scope) [notation, in mathcomp.fingroup.fingroup]

[ ~: _ , _ , .. , _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ <*> _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

#[ _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

<[ _ ] > (group_scope) [notation, in mathcomp.fingroup.fingroup]

<< _ >> (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ set : _ ] (Group_scope) [notation, in mathcomp.fingroup.fingroup]

[ 1 _ ] (Group_scope) [notation, in mathcomp.fingroup.fingroup]

1 (Group_scope) [notation, in mathcomp.fingroup.fingroup]

'C_ ( _ ) [ _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

'C_ _ [ _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

'C [ _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

'C_ ( _ ) ( _ ) (group_scope) [notation, in mathcomp.fingroup.fingroup]

'C_ _ ( _ ) (group_scope) [notation, in mathcomp.fingroup.fingroup]

'C ( _ ) (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ <| _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

'N_ _ ( _ ) (group_scope) [notation, in mathcomp.fingroup.fingroup]

'N ( _ ) (group_scope) [notation, in mathcomp.fingroup.fingroup]

#| _ : _ | (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ :^: _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ ^: _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ :^ _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ :* _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ *: _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ ^# (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ 1 ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ 1 _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ in _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ in _ | _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ < _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ < _ | _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ : _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ : _ | _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ _ _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ | _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ <= _ < _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ <= _ < _ | _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ <- _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

\prod_ ( _ <- _ | _ ) _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

[ ~ _ , _ , .. , _ ] (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ ^ _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ ^- _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ ^+ _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ ^-1 (group_scope) [notation, in mathcomp.fingroup.fingroup]

_ * _ (group_scope) [notation, in mathcomp.fingroup.fingroup]

1 (group_scope) [notation, in mathcomp.fingroup.fingroup]

'O_{ _ , .. , _ } ( _ ) (Group_scope) [notation, in mathcomp.solvable.pgroup]

'O_{ _ , .. , _ } ( _ ) (group_scope) [notation, in mathcomp.solvable.pgroup]

'O_ _ ( _ ) (Group_scope) [notation, in mathcomp.solvable.pgroup]

'O_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.pgroup]

'Syl_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.pgroup]

_ .-Sylow ( _ ) (group_scope) [notation, in mathcomp.solvable.pgroup]

_ .-Hall ( _ ) (group_scope) [notation, in mathcomp.solvable.pgroup]

_ .`_ _ (group_scope) [notation, in mathcomp.solvable.pgroup]

_ .-elt (group_scope) [notation, in mathcomp.solvable.pgroup]

_ .-subgroup ( _ ) (group_scope) [notation, in mathcomp.solvable.pgroup]

_ .-group (group_scope) [notation, in mathcomp.solvable.pgroup]

[ Frobenius _ = _ ><| _ ] (group_scope) [notation, in mathcomp.solvable.frobenius]

[ Frobenius _ ] (group_scope) [notation, in mathcomp.solvable.frobenius]

[ Frobenius _ with kernel _ ] (group_scope) [notation, in mathcomp.solvable.frobenius]

[ Frobenius _ with complement _ ] (group_scope) [notation, in mathcomp.solvable.frobenius]

'e_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]

'R_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]

'n_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]

[ splits _ , over _ ] (group_scope) [notation, in mathcomp.fingroup.gproduct]

[ complements to _ in _ ] (group_scope) [notation, in mathcomp.fingroup.gproduct]

'Q_ _ (Group_scope) [notation, in mathcomp.solvable.extremal]

'Q_ _ (group_scope) [notation, in mathcomp.solvable.extremal]

'SD_ _ (Group_scope) [notation, in mathcomp.solvable.extremal]

'SD_ _ (group_scope) [notation, in mathcomp.solvable.extremal]

'D_ _ (Group_scope) [notation, in mathcomp.solvable.extremal]

'D_ _ (group_scope) [notation, in mathcomp.solvable.extremal]

'Mod_ _ (Group_scope) [notation, in mathcomp.solvable.extremal]

'Mod_ _ (group_scope) [notation, in mathcomp.solvable.extremal]

'Mho^ _ ( _ ) (Group_scope) [notation, in mathcomp.solvable.abelian]

'Mho^ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

'Ohm_ _ ( _ ) (Group_scope) [notation, in mathcomp.solvable.abelian]

'Ohm_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

'r_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

'r ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

'm ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

'E*_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

'E ^ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

'E_ _ ^ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

'E_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

_ .-abelem (group_scope) [notation, in mathcomp.solvable.abelian]

'Ldiv_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.abelian]

'Ldiv_ _ (group_scope) [notation, in mathcomp.solvable.abelian]

_ .-series (group_scope) [notation, in mathcomp.solvable.gseries]

_ .-chief (group_rel_scope) [notation, in mathcomp.solvable.gseries]

_ .-central (group_rel_scope) [notation, in mathcomp.solvable.gseries]

_ .-stable (group_rel_scope) [notation, in mathcomp.solvable.gseries]

_ .-invariant (group_rel_scope) [notation, in mathcomp.solvable.gseries]

_ <|<| _ (group_scope) [notation, in mathcomp.solvable.gseries]

_ \homg _ (group_scope) [notation, in mathcomp.fingroup.morphism]

_ @: _ (Group_scope) [notation, in mathcomp.fingroup.morphism]

_ @*^-1 _ (Group_scope) [notation, in mathcomp.fingroup.morphism]

_ @* _ (Group_scope) [notation, in mathcomp.fingroup.morphism]

'ker_ _ _ (Group_scope) [notation, in mathcomp.fingroup.morphism]

'ker _ (Group_scope) [notation, in mathcomp.fingroup.morphism]

'injm _ (group_scope) [notation, in mathcomp.fingroup.morphism]

_ @*^-1 _ (group_scope) [notation, in mathcomp.fingroup.morphism]

_ @* _ (group_scope) [notation, in mathcomp.fingroup.morphism]

'ker_ _ _ (group_scope) [notation, in mathcomp.fingroup.morphism]

'ker _ (group_scope) [notation, in mathcomp.fingroup.morphism]

'dom _ (group_scope) [notation, in mathcomp.fingroup.morphism]

{ morphism _ >-> _ } (group_scope) [notation, in mathcomp.fingroup.morphism]

'Z ( _ ) (Group_scope) [notation, in mathcomp.solvable.center]

'Z ( _ ) (group_scope) [notation, in mathcomp.solvable.center]

'D^ _ * Q (Group_scope) [notation, in mathcomp.solvable.extraspecial]

'D^ _ * Q (group_scope) [notation, in mathcomp.solvable.extraspecial]

'D^ _ (Group_scope) [notation, in mathcomp.solvable.extraspecial]

'D^ _ (group_scope) [notation, in mathcomp.solvable.extraspecial]

_ ^{1+2* _ } (Group_scope) [notation, in mathcomp.solvable.extraspecial]

_ ^{1+2* _ } (group_scope) [notation, in mathcomp.solvable.extraspecial]

_ ^{1+2} (Group_scope) [notation, in mathcomp.solvable.extraspecial]

_ ^{1+2} (group_scope) [notation, in mathcomp.solvable.extraspecial]

_ \isog Grp ( _ : _ ) (group_scope) [notation, in mathcomp.fingroup.presentation]

_ \homg Grp ( _ : _ ) (group_scope) [notation, in mathcomp.fingroup.presentation]

_ \isog Grp _ (group_scope) [notation, in mathcomp.fingroup.presentation]

_ \homg Grp _ (group_scope) [notation, in mathcomp.fingroup.presentation]

_ : _ (group_presentation) [notation, in mathcomp.fingroup.presentation]

( _ , _ , .. , _ ) (group_presentation) [notation, in mathcomp.fingroup.presentation]

_ = _ = _ (group_presentation) [notation, in mathcomp.fingroup.presentation]

_ = _ (group_presentation) [notation, in mathcomp.fingroup.presentation]

[ ~ _ , _ , .. , _ ] (group_presentation) [notation, in mathcomp.fingroup.presentation]

_ ^- _ (group_presentation) [notation, in mathcomp.fingroup.presentation]

_ ^-1 (group_presentation) [notation, in mathcomp.fingroup.presentation]

_ ^ _ (group_presentation) [notation, in mathcomp.fingroup.presentation]

_ ^+ _ (group_presentation) [notation, in mathcomp.fingroup.presentation]

_ * _ (group_presentation) [notation, in mathcomp.fingroup.presentation]

1 (group_presentation) [notation, in mathcomp.fingroup.presentation]

'SCN_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.maximal]

'SCN ( _ ) (group_scope) [notation, in mathcomp.solvable.maximal]

'F ( _ ) (Group_scope) [notation, in mathcomp.solvable.maximal]

'F ( _ ) (group_scope) [notation, in mathcomp.solvable.maximal]

'Phi ( _ ) (Group_scope) [notation, in mathcomp.solvable.maximal]

'Phi ( _ ) (group_scope) [notation, in mathcomp.solvable.maximal]

'Z_ _ ( _ ) (Group_scope) [notation, in mathcomp.solvable.nilpotent]

'L_ _ ( _ ) (Group_scope) [notation, in mathcomp.solvable.nilpotent]

'Z_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.nilpotent]

'L_ _ ( _ ) (group_scope) [notation, in mathcomp.solvable.nilpotent]

_ != _ %[mod _ ] (int_scope) [notation, in mathcomp.algebra.intdiv]

_ <> _ %[mod _ ] (int_scope) [notation, in mathcomp.algebra.intdiv]

_ == _ %[mod _ ] (int_scope) [notation, in mathcomp.algebra.intdiv]

_ = _ %[mod _ ] (int_scope) [notation, in mathcomp.algebra.intdiv]

_ %| _ (int_scope) [notation, in mathcomp.algebra.intdiv]

_ %% _ (int_scope) [notation, in mathcomp.algebra.intdiv]

_ %/ _ (int_scope) [notation, in mathcomp.algebra.intdiv]

_ %:Z (int_scope) [notation, in mathcomp.algebra.ssrint]

[ 1 _ ] (irrType_scope) [notation, in mathcomp.character.mxrepresentation]

_ ^-1 (lfun_scope) [notation, in mathcomp.algebra.vector]

_ \o _ (lfun_scope) [notation, in mathcomp.algebra.vector]

\1 (lfun_scope) [notation, in mathcomp.algebra.vector]

_ ^-1 (lrfun_scope) [notation, in mathcomp.field.galois]

_ \o _ (lrfun_scope) [notation, in mathcomp.field.falgebra]

\1 (lrfun_scope) [notation, in mathcomp.field.falgebra]

'Z ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

'C_ ( _ ) ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

'C_ _ ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

'C ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ * _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ \in _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ in _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ in _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ < _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ < _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ : _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ : _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ _ _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ <= _ < _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ <= _ < _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ <- _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\bigcap_ ( _ <- _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ in _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ in _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ < _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ < _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ : _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ : _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ _ _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ <= _ < _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ <= _ < _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ <- _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

\sum_ ( _ <- _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ :\: _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ :&: _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ + _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ :=: _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ == _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ < _ < _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ <= _ < _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ < _ <= _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ <= _ <= _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ < _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ <= _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

_ ^C (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

<< _ >> (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]

'C ( _ , _ ) (nat_scope) [notation, in mathcomp.ssreflect.binomial]

_ ^_ _ (nat_scope) [notation, in mathcomp.ssreflect.binomial]

_ %| _ (nat_scope) [notation, in mathcomp.ssreflect.div]

_ != _ %[mod _ ] (nat_scope) [notation, in mathcomp.ssreflect.div]

_ <> _ %[mod _ ] (nat_scope) [notation, in mathcomp.ssreflect.div]

_ == _ %[mod _ ] (nat_scope) [notation, in mathcomp.ssreflect.div]

_ = _ %[mod _ ] (nat_scope) [notation, in mathcomp.ssreflect.div]

_ %% _ (nat_scope) [notation, in mathcomp.ssreflect.div]

_ %/ _ (nat_scope) [notation, in mathcomp.ssreflect.div]

[ Num of _ ] (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ <= _ ?= iff _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ ./2 (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ .*2 (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ .*2 (nat_rec_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ `! (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ ^ _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ ^ _ (nat_rec_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ * _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ * _ (nat_rec_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ < _ < _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ <= _ < _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ < _ <= _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ <= _ <= _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ > _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ >= _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ < _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ <= _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ - _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ - _ (nat_rec_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ + _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ + _ (nat_rec_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ .-2 (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ .-1 (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ .+4 (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ .+3 (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ .+2 (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

_ .+1 (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]

`| _ | (nat_scope) [notation, in mathcomp.algebra.ssrint]

_ `_ _ (nat_scope) [notation, in mathcomp.ssreflect.prime]

_ .-nat (nat_scope) [notation, in mathcomp.ssreflect.prime]

_ ^' (nat_scope) [notation, in mathcomp.ssreflect.prime]

\p i ( _ ) (nat_scope) [notation, in mathcomp.ssreflect.prime]

\pi ( _ ) (nat_scope) [notation, in mathcomp.ssreflect.prime]

\dim _ (nat_scope) [notation, in mathcomp.algebra.vector]

[ arg max_ ( _ > _ ) _ ] (nat_scope) [notation, in mathcomp.ssreflect.fintype]

[ arg max_ ( _ > _ in _ ) _ ] (nat_scope) [notation, in mathcomp.ssreflect.fintype]

[ arg max_ ( _ > _ | _ ) _ ] (nat_scope) [notation, in mathcomp.ssreflect.fintype]

[ arg min_ ( _ < _ ) _ ] (nat_scope) [notation, in mathcomp.ssreflect.fintype]

[ arg min_ ( _ < _ in _ ) _ ] (nat_scope) [notation, in mathcomp.ssreflect.fintype]

[ arg min_ ( _ < _ | _ ) _ ] (nat_scope) [notation, in mathcomp.ssreflect.fintype]

#| _ | (nat_scope) [notation, in mathcomp.ssreflect.fintype]

\max_ ( _ in _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ in _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ < _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ < _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ <= _ < _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ <= _ < _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ : _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ : _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ _ _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ <- _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\max_ ( _ <- _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ in _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ in _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ < _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ < _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ : _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ : _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ _ _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ <= _ < _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ <= _ < _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ <- _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\prod_ ( _ <- _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ in _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ in _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ < _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ < _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ : _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ : _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ _ _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ <= _ < _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ <= _ < _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ <- _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\sum_ ( _ <- _ | _ ) _ (nat_scope) [notation, in mathcomp.ssreflect.bigop]

\dim_ _ _ (nat_scope) [notation, in mathcomp.field.falgebra]

\rank _ (nat_scope) [notation, in mathcomp.algebra.mxalgebra]

_ : _ (nt_group_presentation) [notation, in mathcomp.fingroup.presentation]

`] -oo , +oo [ (order_scope) [notation, in mathcomp.algebra.interval]

`] _ , +oo [ (order_scope) [notation, in mathcomp.algebra.interval]

`[ _ , +oo [ (order_scope) [notation, in mathcomp.algebra.interval]

`] -oo , _ [ (order_scope) [notation, in mathcomp.algebra.interval]

`] -oo , _ ] (order_scope) [notation, in mathcomp.algebra.interval]

`] _ , _ [ (order_scope) [notation, in mathcomp.algebra.interval]

`[ _ , _ [ (order_scope) [notation, in mathcomp.algebra.interval]

`] _ , _ ] (order_scope) [notation, in mathcomp.algebra.interval]

`[ _ , _ ] (order_scope) [notation, in mathcomp.algebra.interval]

+oo (order_scope) [notation, in mathcomp.algebra.interval]

-oo (order_scope) [notation, in mathcomp.algebra.interval]

_ <> _ %[mod_eq _ ] (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

_ != _ %[mod_eq _ ] (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

_ = _ %[mod_eq _ ] (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

_ == _ %[mod_eq _ ] (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

{eq_quot _ } (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

{pi _ } (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

{pi_ _ _ } (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

_ <> _ %[mod _ ] (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

_ != _ %[mod _ ] (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

_ = _ %[mod _ ] (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

_ == _ %[mod _ ] (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

\pi (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

\pi_ _ (quotient_scope) [notation, in mathcomp.ssreflect.generic_quotient]

_ <> _ %[mod_ideal _ ] (quotient_scope) [notation, in mathcomp.algebra.ring_quotient]

_ != _ %[mod_ideal _ ] (quotient_scope) [notation, in mathcomp.algebra.ring_quotient]

_ = _ %[mod_ideal _ ] (quotient_scope) [notation, in mathcomp.algebra.ring_quotient]

_ == _ %[mod_ideal _ ] (quotient_scope) [notation, in mathcomp.algebra.ring_quotient]

_ / _ (rat_scope) [notation, in mathcomp.algebra.rat]

_ - _ (rat_scope) [notation, in mathcomp.algebra.rat]

_ ^-1 (rat_scope) [notation, in mathcomp.algebra.rat]

_ * _ (rat_scope) [notation, in mathcomp.algebra.rat]

- _ (rat_scope) [notation, in mathcomp.algebra.rat]

_ + _ (rat_scope) [notation, in mathcomp.algebra.rat]

1 (rat_scope) [notation, in mathcomp.algebra.rat]

0 (rat_scope) [notation, in mathcomp.algebra.rat]

'omega_ _ [ _ ] (ring_scope) [notation, in mathcomp.character.integral_char]

'K_ _ (ring_scope) [notation, in mathcomp.character.integral_char]

_ <= _ ?< if _ (ring_scope) [notation, in mathcomp.algebra.interval]

`] -oo , +oo [ (ring_scope) [notation, in mathcomp.algebra.interval]

`] _ , +oo [ (ring_scope) [notation, in mathcomp.algebra.interval]

`[ _ , +oo [ (ring_scope) [notation, in mathcomp.algebra.interval]

`] -oo , _ [ (ring_scope) [notation, in mathcomp.algebra.interval]

`] -oo , _ ] (ring_scope) [notation, in mathcomp.algebra.interval]

`] _ , _ [ (ring_scope) [notation, in mathcomp.algebra.interval]

`[ _ , _ [ (ring_scope) [notation, in mathcomp.algebra.interval]

`] _ , _ ] (ring_scope) [notation, in mathcomp.algebra.interval]

`[ _ , _ ] (ring_scope) [notation, in mathcomp.algebra.interval]

_ ^@ (ring_scope) [notation, in mathcomp.field.algebraics_fundamentals]

_ ^ _ (ring_scope) [notation, in mathcomp.field.algebraics_fundamentals]

\adj _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\det _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\tr _ (ring_scope) [notation, in mathcomp.algebra.matrix]

_ *m _ (ring_scope) [notation, in mathcomp.algebra.matrix]

_ %:M (ring_scope) [notation, in mathcomp.algebra.matrix]

_ ^T (ring_scope) [notation, in mathcomp.algebra.matrix]

\row_ _ _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\row_ ( _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\col_ _ _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\col_ ( _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\matrix_ _ _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\matrix_ ( _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\matrix_ ( _ , _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\matrix_ ( _ , _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\matrix_ ( _ < _ , _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]

\matrix[ _ ]_ ( _ , _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]

'Ind (ring_scope) [notation, in mathcomp.character.classfun]

'Ind[ _ ] (ring_scope) [notation, in mathcomp.character.classfun]

'Ind[ _ , _ ] (ring_scope) [notation, in mathcomp.character.classfun]

'Res (ring_scope) [notation, in mathcomp.character.classfun]

'Res[ _ ] (ring_scope) [notation, in mathcomp.character.classfun]

'Res[ _ , _ ] (ring_scope) [notation, in mathcomp.character.classfun]

'CF ( _ , _ ) (ring_scope) [notation, in mathcomp.character.classfun]

'[ _ ] (ring_scope) [notation, in mathcomp.character.classfun]

'[ _ ]_ _ (ring_scope) [notation, in mathcomp.character.classfun]

'[ _ , _ ] (ring_scope) [notation, in mathcomp.character.classfun]

'[ _ , _ ]_ _ (ring_scope) [notation, in mathcomp.character.classfun]

'CF ( _ , _ ) (ring_scope) [notation, in mathcomp.character.classfun]

'1_ _ (ring_scope) [notation, in mathcomp.character.classfun]

_ ^ _ (ring_scope) [notation, in mathcomp.algebra.ssrint]

_ %:~R (ring_scope) [notation, in mathcomp.algebra.ssrint]

_ *~ _ (ring_scope) [notation, in mathcomp.algebra.ssrint]

*~%R (ring_scope) [notation, in mathcomp.algebra.ssrint]

_ <> _ :> in t (ring_scope) [notation, in mathcomp.algebra.ssrint]

_ != _ :> in t (ring_scope) [notation, in mathcomp.algebra.ssrint]

_ == _ :> in t (ring_scope) [notation, in mathcomp.algebra.ssrint]

_ = _ :> in t (ring_scope) [notation, in mathcomp.algebra.ssrint]

_ %:Z (ring_scope) [notation, in mathcomp.algebra.ssrint]

_ .[ _ , _ ] (ring_scope) [notation, in mathcomp.algebra.polyXY]

_ ^:P (ring_scope) [notation, in mathcomp.algebra.polyXY]

'Y (ring_scope) [notation, in mathcomp.algebra.polyXY]

_ ^ _ (ring_scope) [notation, in mathcomp.algebra.polyXY]

_ %:Q (ring_scope) [notation, in mathcomp.algebra.rat]

\prod_ ( _ in _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ in _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ < _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ : _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ : _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ _ _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ <= _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ <= _ < _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ <- _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\prod_ ( _ <- _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ in _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ in _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ < _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ : _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ : _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ _ _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ <= _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ <= _ < _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ <- _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\sum_ ( _ <- _ | _ ) _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ \o* _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ \*o _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ \*: _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ \- _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ \+ _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

\0 (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ %:A (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ *: _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ / _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ ^- _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ ^-1 (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ ^+ _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ * _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

[ char _ ] (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ %:R (ring_scope) [notation, in mathcomp.algebra.ssralg]

- 1 (ring_scope) [notation, in mathcomp.algebra.ssralg]

1 (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ `_ _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ *- _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ *+ _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ - _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

_ + _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

- _ (ring_scope) [notation, in mathcomp.algebra.ssralg]

-%R (ring_scope) [notation, in mathcomp.algebra.ssralg]

0 (ring_scope) [notation, in mathcomp.algebra.ssralg]

'chi[ _ ]_ _ (ring_scope) [notation, in mathcomp.character.character]

'chi_ _ (ring_scope) [notation, in mathcomp.character.character]

_ \Po _ (ring_scope) [notation, in mathcomp.algebra.poly]

_ ^:P (ring_scope) [notation, in mathcomp.algebra.poly]

_ ^`N ( _ ) (ring_scope) [notation, in mathcomp.algebra.poly]

_ ^` ( _ ) (ring_scope) [notation, in mathcomp.algebra.poly]

_ ^` (ring_scope) [notation, in mathcomp.algebra.poly]

_ .-primitive_root (ring_scope) [notation, in mathcomp.algebra.poly]

_ .-unity_root (ring_scope) [notation, in mathcomp.algebra.poly]

_ .[ _ ] (ring_scope) [notation, in mathcomp.algebra.poly]

'X^ _ (ring_scope) [notation, in mathcomp.algebra.poly]

'X (ring_scope) [notation, in mathcomp.algebra.poly]

_ %:P (ring_scope) [notation, in mathcomp.algebra.poly]

\poly_ ( _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.poly]

_ / _ (section_scope) [notation, in mathcomp.solvable.jordanholder]

[ seq _ : _ | _ <- _ , _ <- _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ : _ | _ : _ <- _ , _ : _ <- _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ | _ : _ <- _ , _ : _ <- _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ | _ <- _ , _ <- _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ : _ | _ : _ <- _ & _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ : _ | _ : _ <- _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ : _ | _ <- _ & _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ : _ | _ <- _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ | _ : _ <- _ & _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ | _ : _ <- _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ | _ <- _ & _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ | _ <- _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ <- _ | _ & _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ <- _ | _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

_ ++ _ (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ :: _ ; _ ; .. ; _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ :: _ , _ , .. , _ & _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ :: _ & _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ :: _ ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ :: ] (seq_scope) [notation, in mathcomp.ssreflect.seq]

_ :: _ (seq_scope) [notation, in mathcomp.ssreflect.seq]

[ seq _ , _ ] (seq_scope) [notation, in mathcomp.ssreflect.fintype]

[ seq _ | _ : _ ] (seq_scope) [notation, in mathcomp.ssreflect.fintype]

[ seq _ | _ : _ in _ ] (seq_scope) [notation, in mathcomp.ssreflect.fintype]

[ seq _ | _ in _ ] (seq_scope) [notation, in mathcomp.ssreflect.fintype]

\bigcap_ ( _ in _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ in _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ < _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ < _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ : _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ : _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ _ _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ <= _ < _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ <= _ < _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ <- _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcap_ ( _ <- _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ in _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ in _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ < _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ < _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ : _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ : _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ _ _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ <= _ < _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ <= _ < _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ <- _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

\bigcup_ ( _ <- _ | _ ) _ (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ , _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ , _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ in _ , _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ in _ , _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ , _ in _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ , _ in _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ , _ : _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ , _ : _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ in _ , _ : _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ in _ , _ : _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ , _ : _ in _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ , _ : _ in _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ in _ , _ : _ in _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ in _ , _ : _ in _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ in _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ : _ in _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ in _ , _ in _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ in _ , _ in _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ in _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ in _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

_ @2: ( _ , _ ) (set_scope) [notation, in mathcomp.ssreflect.finset]

_ @: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ @^-1: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ ::&: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ :\ _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ :\: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set ~ _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

~: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ :&: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ ; _ ; .. ; _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

_ |: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ :|: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ : _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set : _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ : _ in _ | _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ in _ | _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ in _ | _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ : _ in _ | _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ : _ | _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ : _ in _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ in _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ | _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ set _ : _ | _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

_ :=P: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ :!=: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ :==: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ :<>: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ :=: _ (set_scope) [notation, in mathcomp.ssreflect.finset]

_ .-dtuple ( _ ) (set_scope) [notation, in mathcomp.solvable.primitive_action]

'forall 'X_ _ , _ (term_scope) [notation, in mathcomp.algebra.ssralg]

'exists 'X_ _ , _ (term_scope) [notation, in mathcomp.algebra.ssralg]

~ _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ ==> _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ \/ _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ /\ _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ != _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ == _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ ^+ _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ / _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ ^-1 (term_scope) [notation, in mathcomp.algebra.ssralg]

_ *+ _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ * _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ - _ (term_scope) [notation, in mathcomp.algebra.ssralg]

- _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ + _ (term_scope) [notation, in mathcomp.algebra.ssralg]

_ %:T (term_scope) [notation, in mathcomp.algebra.ssralg]

1 (term_scope) [notation, in mathcomp.algebra.ssralg]

0 (term_scope) [notation, in mathcomp.algebra.ssralg]

_ %:R (term_scope) [notation, in mathcomp.algebra.ssralg]

'X_ _ (term_scope) [notation, in mathcomp.algebra.ssralg]

{ perm _ } (type_scope) [notation, in mathcomp.fingroup.perm]

_ .-tuple (type_scope) [notation, in mathcomp.ssreflect.tuple]

_ ^ _ (type_scope) [notation, in mathcomp.ssreflect.finfun]

{ dffun _ } (type_scope) [notation, in mathcomp.ssreflect.finfun]

{ ffun _ } (type_scope) [notation, in mathcomp.ssreflect.finfun]

'F_ _ (type_scope) [notation, in mathcomp.algebra.zmodp]

'Z_ _ (type_scope) [notation, in mathcomp.algebra.zmodp]

{ set _ } (type_scope) [notation, in mathcomp.ssreflect.finset]

{ 'GL_ _ ( _ ) } (type_scope) [notation, in mathcomp.algebra.matrix]

{ 'GL_ _ [ _ ] } (type_scope) [notation, in mathcomp.algebra.matrix]

'M_ ( _ ) (type_scope) [notation, in mathcomp.algebra.matrix]

'M_ _ (type_scope) [notation, in mathcomp.algebra.matrix]

'cV_ _ (type_scope) [notation, in mathcomp.algebra.matrix]

'rV_ _ (type_scope) [notation, in mathcomp.algebra.matrix]

'M_ ( _ , _ ) (type_scope) [notation, in mathcomp.algebra.matrix]

'M[ _ ]_ ( _ ) (type_scope) [notation, in mathcomp.algebra.matrix]

'M[ _ ]_ _ (type_scope) [notation, in mathcomp.algebra.matrix]

'cV[ _ ]_ _ (type_scope) [notation, in mathcomp.algebra.matrix]

'rV[ _ ]_ _ (type_scope) [notation, in mathcomp.algebra.matrix]

'M[ _ ]_ ( _ , _ ) (type_scope) [notation, in mathcomp.algebra.matrix]

{ action _ &-> _ } (type_scope) [notation, in mathcomp.fingroup.action]

{ in _ , isometry _ , to _ } (type_scope) [notation, in mathcomp.character.classfun]

'CF ( _ ) (type_scope) [notation, in mathcomp.character.classfun]

[ subg _ ] (type_scope) [notation, in mathcomp.fingroup.fingroup]

{ group _ } (type_scope) [notation, in mathcomp.fingroup.fingroup]

'Q_ _ (type_scope) [notation, in mathcomp.solvable.extremal]

'SD_ _ (type_scope) [notation, in mathcomp.solvable.extremal]

'D_ _ (type_scope) [notation, in mathcomp.solvable.extremal]

'Mod_ _ (type_scope) [notation, in mathcomp.solvable.extremal]

{ unit _ } (type_scope) [notation, in mathcomp.algebra.finalg]

{ pred _ } (type_scope) [notation, in mathcomp.ssreflect.ssrbool]

@ fun_adjunction _ _ _ _ _ _ (type_scope) [notation, in mathcomp.ssreflect.fingraph]

@ rel_adjunction _ _ _ _ _ _ (type_scope) [notation, in mathcomp.ssreflect.fingraph]

_ ^o (type_scope) [notation, in mathcomp.algebra.ssralg]

_ ^c (type_scope) [notation, in mathcomp.algebra.ssralg]

'D^ _ * Q (type_scope) [notation, in mathcomp.solvable.extraspecial]

'D^ _ (type_scope) [notation, in mathcomp.solvable.extraspecial]

_ ^{1+2* _ } (type_scope) [notation, in mathcomp.solvable.extraspecial]

_ ^{1+2} (type_scope) [notation, in mathcomp.solvable.extraspecial]

{ ? _ in _ | _ } (type_scope) [notation, in mathcomp.ssreflect.eqtype]

{ ? _ in _ } (type_scope) [notation, in mathcomp.ssreflect.eqtype]

{ ? _ | _ } (type_scope) [notation, in mathcomp.ssreflect.eqtype]

{ ? _ : _ | _ } (type_scope) [notation, in mathcomp.ssreflect.eqtype]

{ _ in _ | _ } (type_scope) [notation, in mathcomp.ssreflect.eqtype]

{ _ in _ } (type_scope) [notation, in mathcomp.ssreflect.eqtype]

'AEnd ( _ ) (type_scope) [notation, in mathcomp.field.falgebra]

'AHom ( _ , _ ) (type_scope) [notation, in mathcomp.field.falgebra]

{ aspace _ } (type_scope) [notation, in mathcomp.field.falgebra]

'A [ _ ]_ _ (type_scope) [notation, in mathcomp.algebra.mxalgebra]

'A [ _ ]_ ( _ ) (type_scope) [notation, in mathcomp.algebra.mxalgebra]

'A [ _ ]_ ( _ , _ ) (type_scope) [notation, in mathcomp.algebra.mxalgebra]

'A_ _ (type_scope) [notation, in mathcomp.algebra.mxalgebra]

'A_ ( _ ) (type_scope) [notation, in mathcomp.algebra.mxalgebra]

'A_ ( _ , _ ) (type_scope) [notation, in mathcomp.algebra.mxalgebra]

'CF ( _ ) (vspace_scope) [notation, in mathcomp.character.classfun]

_ @^-1: _ (vspace_scope) [notation, in mathcomp.algebra.vector]

_ @: _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ in _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ in _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ < _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ < _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ : _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ : _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ _ _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ <= _ < _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ <= _ < _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ <- _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\bigcap_ ( _ <- _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ in _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ in _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ < _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ < _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ : _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ : _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ _ _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ <= _ < _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ <= _ < _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ <- _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

\sum_ ( _ <- _ | _ ) _ (vspace_scope) [notation, in mathcomp.algebra.vector]

{ : _ } (vspace_scope) [notation, in mathcomp.algebra.vector]

_ :\: _ (vspace_scope) [notation, in mathcomp.algebra.vector]

_ ^C (vspace_scope) [notation, in mathcomp.algebra.vector]

_ :&: _ (vspace_scope) [notation, in mathcomp.algebra.vector]

_ + _ (vspace_scope) [notation, in mathcomp.algebra.vector]

0 (vspace_scope) [notation, in mathcomp.algebra.vector]

<< _ >> (vspace_scope) [notation, in mathcomp.algebra.vector]

<[ _ ] > (vspace_scope) [notation, in mathcomp.algebra.vector]

_ <= _ <= _ (vspace_scope) [notation, in mathcomp.algebra.vector]

_ <= _ (vspace_scope) [notation, in mathcomp.algebra.vector]

<< _ ; _ >> (vspace_scope) [notation, in mathcomp.field.falgebra]

<< _ & _ >> (vspace_scope) [notation, in mathcomp.field.falgebra]

'Z ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]

'C_ ( _ ) ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]

'C_ _ ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]

'C ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]

'C_ ( _ ) [ _ ] (vspace_scope) [notation, in mathcomp.field.falgebra]

'C_ _ [ _ ] (vspace_scope) [notation, in mathcomp.field.falgebra]

'C [ _ ] (vspace_scope) [notation, in mathcomp.field.falgebra]

_ ^+ _ (vspace_scope) [notation, in mathcomp.field.falgebra]

_ * _ (vspace_scope) [notation, in mathcomp.field.falgebra]

1 (vspace_scope) [notation, in mathcomp.field.falgebra]

_ .[ ACl _ ] [notation, in mathcomp.ssreflect.ssrAC]

_ .[ AC _ _ ] [notation, in mathcomp.ssreflect.ssrAC]

_ .[ ACof _ _ ] [notation, in mathcomp.ssreflect.ssrAC]

_ \x _ [notation, in mathcomp.fingroup.gproduct]

_ \* _ [notation, in mathcomp.fingroup.gproduct]

_ ><| _ [notation, in mathcomp.fingroup.gproduct]

_ \isog _ [notation, in mathcomp.fingroup.morphism]

'Chi_ _ [notation, in mathcomp.character.character]

'exists_in_ _ [notation, in mathcomp.ssreflect.fintype]

'exists_ _ [notation, in mathcomp.ssreflect.fintype]

'forall_in_ _ [notation, in mathcomp.ssreflect.fintype]

'forall_ _ [notation, in mathcomp.ssreflect.fintype]

'I_ _ [notation, in mathcomp.ssreflect.fintype]

'Phi_ _ [notation, in mathcomp.field.cyclotomic]

'S_ _ [notation, in mathcomp.fingroup.perm]

*%N [notation, in mathcomp.ssreflect.bigop]

*%R [notation, in mathcomp.algebra.ssralg]

*:%R [notation, in mathcomp.algebra.ssralg]

+%N [notation, in mathcomp.ssreflect.bigop]

+%R [notation, in mathcomp.algebra.ssralg]

<< _ ; _ >> [notation, in mathcomp.field.algebraics_fundamentals]

@ perm [notation, in mathcomp.fingroup.perm]

@ itv_splitU2 [notation, in mathcomp.algebra.interval]

@ ler_in_itv [notation, in mathcomp.algebra.interval]

@ ltr_in_itv [notation, in mathcomp.algebra.interval]

@ itv_gte [notation, in mathcomp.algebra.interval]

@ lersif_in_itv [notation, in mathcomp.algebra.interval]

@ lersif_ndivr_mull [notation, in mathcomp.algebra.interval]

@ lersif_ndivl_mull [notation, in mathcomp.algebra.interval]

@ lersif_ndivr_mulr [notation, in mathcomp.algebra.interval]

@ lersif_ndivl_mulr [notation, in mathcomp.algebra.interval]

@ lersif_pdivr_mull [notation, in mathcomp.algebra.interval]

@ lersif_pdivl_mull [notation, in mathcomp.algebra.interval]

@ lersif_pdivr_mulr [notation, in mathcomp.algebra.interval]

@ lersif_pdivl_mulr [notation, in mathcomp.algebra.interval]

@ lersif_maxl [notation, in mathcomp.algebra.interval]

@ lersif_maxr [notation, in mathcomp.algebra.interval]

@ lersif_minl [notation, in mathcomp.algebra.interval]

@ lersif_minr [notation, in mathcomp.algebra.interval]

@ lersif_distl [notation, in mathcomp.algebra.interval]

@ lersif_normr [notation, in mathcomp.algebra.interval]

@ lersif_norml [notation, in mathcomp.algebra.interval]

@ lersifN [notation, in mathcomp.algebra.interval]

@ lersif_nnormr [notation, in mathcomp.algebra.interval]

@ real_lersif_normr [notation, in mathcomp.algebra.interval]

@ real_lersif_norml [notation, in mathcomp.algebra.interval]

@ real_lersifN [notation, in mathcomp.algebra.interval]

@ lersif_nmul2r [notation, in mathcomp.algebra.interval]

@ lersif_nmul2l [notation, in mathcomp.algebra.interval]

@ lersif_pmul2r [notation, in mathcomp.algebra.interval]

@ lersif_pmul2l [notation, in mathcomp.algebra.interval]

@ ltrW_lersif [notation, in mathcomp.algebra.interval]

@ lersifW [notation, in mathcomp.algebra.interval]

@ lersif_imply [notation, in mathcomp.algebra.interval]

@ lersif_orb [notation, in mathcomp.algebra.interval]

@ lersif_andb [notation, in mathcomp.algebra.interval]

@ lersif_subr_addl [notation, in mathcomp.algebra.interval]

@ lersif_subl_addl [notation, in mathcomp.algebra.interval]

@ lersif_subr_addr [notation, in mathcomp.algebra.interval]

@ lersif_subl_addr [notation, in mathcomp.algebra.interval]

@ lersif_add2r [notation, in mathcomp.algebra.interval]

@ lersif_add2l [notation, in mathcomp.algebra.interval]

@ lersif_opp2 [notation, in mathcomp.algebra.interval]

@ lersif_oppr0 [notation, in mathcomp.algebra.interval]

@ lersif_0oppr [notation, in mathcomp.algebra.interval]

@ lersif_oppr [notation, in mathcomp.algebra.interval]

@ lersif_oppl [notation, in mathcomp.algebra.interval]

@ lersifF [notation, in mathcomp.algebra.interval]

@ lersifT [notation, in mathcomp.algebra.interval]

@ lersifS [notation, in mathcomp.algebra.interval]

@ lersifNF [notation, in mathcomp.algebra.interval]

@ lersifxx [notation, in mathcomp.algebra.interval]

@ lersif_anti [notation, in mathcomp.algebra.interval]

@ lersif_trans [notation, in mathcomp.algebra.interval]

@ subr_lersif0r [notation, in mathcomp.algebra.interval]

@ subr_lersifr0 [notation, in mathcomp.algebra.interval]

@ lersif [notation, in mathcomp.algebra.interval]

@ ffun_on _ _ [notation, in mathcomp.ssreflect.finfun]

@ cf_triangle_lerif [notation, in mathcomp.character.classfun]

@ sval [notation, in mathcomp.ssreflect.eqtype]

[ seq _ : _ <- _ | _ & _ ] [notation, in mathcomp.ssreflect.seq]

[ seq _ : _ <- _ | _ ] [notation, in mathcomp.ssreflect.seq]

\d_ _ [notation, in mathcomp.algebra.fraction]

\mpi [notation, in mathcomp.ssreflect.generic_quotient]

\n_ _ [notation, in mathcomp.algebra.fraction]

{ideal_quot _ } [notation, in mathcomp.algebra.ring_quotient]

{ fraction _ } [notation, in mathcomp.algebra.fraction]

{ ratio _ } [notation, in mathcomp.algebra.fraction]

{ poly _ } [notation, in mathcomp.algebra.poly]

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