mathcomp.ssreflect.tuple

Global Index

_

(75489 entries)

Notation Index

H

J

T

W

X

Y

_

(1813 entries)

Binder Index

_

other

(45320 entries)

Module Index

H

J

K

L

W

X

Y

Z

_

other

(382 entries)

Variable Index

J

W

X

Y

_

other

(3967 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(14046 entries)

Constructor Index

J

K

W

Y

_

other

(469 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(128 entries)

Projection Index

H

J

K

L

W

X

Y

_

other

(457 entries)

Section Index

J

W

X

Y

_

other

(1372 entries)

Abbreviation Index

Y

_

other

(1025 entries)

Definition Index

Y

_

other

(6124 entries)

Record Index

H

J

K

L

W

X

Y

_

other

(250 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]
[ bseq ] (form_scope) [notation, in mathcomp.ssreflect.tuple]
[ bseq _ ; .. ; _ ] (form_scope) [notation, in mathcomp.ssreflect.tuple]
[ bseq of _ ] (form_scope) [notation, in mathcomp.ssreflect.tuple]
{ bseq _ of _ } (form_scope) [notation, in mathcomp.ssreflect.tuple]
[ 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]
@ 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]
_ .-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]
_ ^* (fun_scope) [notation, in mathcomp.fingroup.action]
*~%R (fun_scope) [notation, in mathcomp.algebra.ssrint]
[ 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]
*:%R (fun_scope) [notation, in mathcomp.algebra.ssralg]
*%R (fun_scope) [notation, in mathcomp.algebra.ssralg]
+%R (fun_scope) [notation, in mathcomp.algebra.ssralg]
-%R (fun_scope) [notation, in mathcomp.algebra.ssralg]
[ 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]
[ 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]
\mxdiag_ _ _ (ring_scope) [notation, in mathcomp.algebra.matrix]
\mxdiag_ ( _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]
\mxcol_ _ _ (ring_scope) [notation, in mathcomp.algebra.matrix]
\mxcol_ ( _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]
\mxrow_ _ _ (ring_scope) [notation, in mathcomp.algebra.matrix]
\mxrow_ ( _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]
\mxblock_ ( _ , _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]
\mxblock_ ( _ , _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]
\mxblock_ ( _ < _ , _ < _ ) _ (ring_scope) [notation, in mathcomp.algebra.matrix]
\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]
_ ~_ _ { in _ } (ring_scope) [notation, in mathcomp.algebra.mxpoly]
'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]
_ <> _ :> 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]
[ rat _ // _ ] (ring_scope) [notation, in mathcomp.algebra.rat]
[ rat _ // _ ] (ring_scope) [notation, in mathcomp.algebra.rat]
_ %: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]
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]
_ .-bseq (type_scope) [notation, in mathcomp.ssreflect.tuple]
_ .-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]
_ ~_{in _ } { in _ } [notation, in mathcomp.algebra.mxpoly]
_ ~_{in _ } _ [notation, in mathcomp.algebra.mxpoly]
_ ~_ _ _ [notation, in mathcomp.algebra.mxpoly]
_ .[ 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]
+%N [notation, in mathcomp.ssreflect.bigop]
<< _ ; _ >> [notation, in mathcomp.field.algebraics_fundamentals]
@ perm [notation, in mathcomp.fingroup.perm]
@ lersif [notation, in mathcomp.algebra.interval]
@ 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]
\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

_

(75489 entries)

Notation Index

H

J

T

W

X

Y

_

(1813 entries)

Binder Index

_

other

(45320 entries)

Module Index

H

J

K

L

W

X

Y

Z

_

other

(382 entries)

Variable Index

J

W

X

Y

_

other

(3967 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(14046 entries)

Constructor Index

J

K

W

Y

_

other

(469 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(128 entries)

Projection Index

H

J

K

L

W

X

Y

_

other

(457 entries)

Section Index

J

W

X

Y

_

other

(1372 entries)

Abbreviation Index

Y

_

other

(1025 entries)

Definition Index

Y

_

other

(6124 entries)

Record Index

H

J

K

L

W

X

Y

_

other

(250 entries)