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 | (24263 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 | (1399 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 | (226 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 | (3670 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 | (89 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 | (12297 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 | (383 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 | (114 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 | (279 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 | (1169 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 | (742 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 | (3657 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 | (193 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]

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

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

[ 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]

_ != _ %[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]

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

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

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

_ ^: _ (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]

_ > _ (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]

[ 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]

[ 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]

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

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

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

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

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

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

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

[ arg min_ ( _ < _ | _ ) _ ] (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]

[ pic k _ : _ ] (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]

{ 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]

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

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

[ new Type 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]

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

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

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

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

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

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

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

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

[ 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]

_ .-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]

[ 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]

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

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

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

[ 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]

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

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

'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]

'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]

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

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

[ 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]

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

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

'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]

'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]

'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]

'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]

'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]

'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]

_ \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]

_ .-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]

'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]

'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]

'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]

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

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

_ \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]

[ 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]

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

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

_ != _ %[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.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]

_ %| _ (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]

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

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

[ 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]

\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]

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

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

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

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

_ <> _ %[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]

_ <> _ %[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]

_ / _ (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]

_ %: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]

`] -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]

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

\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]

_ .[ _ , _ ] (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]

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

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

'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]

_ \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]

_ ^ _ (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.field.algebraics_fundamentals]

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

_ / _ (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]

_ .-dtuple ( _ ) (set_scope) [notation, in mathcomp.solvable.primitive_action]

\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]

[ se t _ | _ : _ , _ : _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ se t _ | _ : _ , _ : _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ se t _ | _ : _ in _ , _ : _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ se t _ | _ : _ in _ , _ : _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ se t _ | _ : _ , _ : _ in _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ se t _ | _ : _ , _ : _ in _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ se t _ | _ in _ , _ in _ & _ ] (set_scope) [notation, in mathcomp.ssreflect.finset]

[ se t _ | _ in _ , _ 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 _ , _ : _ & _ ] (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]

'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]

_ ^o (type_scope) [notation, in mathcomp.algebra.ssralg]

_ ^c (type_scope) [notation, in mathcomp.algebra.ssralg]

{ perm _ } (type_scope) [notation, in mathcomp.fingroup.perm]

'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]

_ .-tuple (type_scope) [notation, in mathcomp.ssreflect.tuple]

{ '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]

'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]

{ 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]

{ pred _ } (type_scope) [notation, in mathcomp.ssreflect.ssrbool]

_ ^ _ (type_scope) [notation, in mathcomp.ssreflect.finfun]

{ dffun _ } (type_scope) [notation, in mathcomp.ssreflect.finfun]

{ ffun _ } (type_scope) [notation, in mathcomp.ssreflect.finfun]

{ ? _ 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]

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

{ group _ } (type_scope) [notation, in mathcomp.fingroup.fingroup]

@ fun_adjunction _ _ _ _ _ _ (type_scope) [notation, in mathcomp.ssreflect.fingraph]

@ rel_adjunction _ _ _ _ _ _ (type_scope) [notation, in mathcomp.ssreflect.fingraph]

'F_ _ (type_scope) [notation, in mathcomp.algebra.zmodp]

'Z_ _ (type_scope) [notation, in mathcomp.algebra.zmodp]

'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]

{ set _ } (type_scope) [notation, in mathcomp.ssreflect.finset]

_ @^-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]

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

<< _ ; _ >> (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]

_ \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]

@ perm_eq_trans [notation, in mathcomp.ssreflect.seq]

@ eq_big_perm [notation, in mathcomp.ssreflect.bigop]

@ ffun_on _ _ [notation, in mathcomp.ssreflect.finfun]

@ sval [notation, in mathcomp.ssreflect.eqtype]

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

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

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

\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 | (24263 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 | (1399 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 | (226 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 | (3670 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 | (89 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 | (12297 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 | (383 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 | (114 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 | (279 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 | (1169 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 | (742 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 | (3657 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 | (193 entries) |