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

(1583 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

(4 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

(186 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

(49 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

(914 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

(5 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

(2 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

(1 entry)

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

(78 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

(3 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

(340 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

(1 entry)

---

Global Index

A

all_D_transitions [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
all_bnd_apply_psis [lemma, in mathcomp_eulerian.perm_seq_bridge]
all_le_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
AltDesc [section, in mathcomp_eulerian.altsub]
AltDesc.n [variable, in mathcomp_eulerian.altsub]
altsub [library]
alt_desc_set [definition, in mathcomp_eulerian.beta_swap]
alt_aux_from_sign [lemma, in mathcomp_eulerian.altsub]
alt_321_sub [definition, in mathcomp_eulerian.altsub]
alt_31425 [definition, in mathcomp_eulerian.altsub]
alt_3142 [definition, in mathcomp_eulerian.altsub]
alt_321 [definition, in mathcomp_eulerian.altsub]
alt_312 [definition, in mathcomp_eulerian.altsub]
alt_aux [definition, in mathcomp_eulerian.altsub]
alt_plus_nalt_as_set_is_alt_sum [lemma, in mathcomp_eulerian.reflection]
alt_desc_set_is_alt [lemma, in mathcomp_eulerian.reflection]
alt_desc_set_1 [lemma, in mathcomp_eulerian.reflection]
alt_desc_set_0 [lemma, in mathcomp_eulerian.reflection]
AndreInterior [section, in mathcomp_eulerian.reflection]
AndreInterior.c [variable, in mathcomp_eulerian.reflection]
AndreInterior.n [variable, in mathcomp_eulerian.reflection]
AndreInterior.s [variable, in mathcomp_eulerian.reflection]
andre_interior_count [lemma, in mathcomp_eulerian.reflection]
andre_union_eq_split [lemma, in mathcomp_eulerian.reflection]
andre_target_gt [lemma, in mathcomp_eulerian.reflection]
andre_target_at [lemma, in mathcomp_eulerian.reflection]
andre_target_lt [lemma, in mathcomp_eulerian.reflection]
andre_s_ltn [lemma, in mathcomp_eulerian.reflection]
andre_split_lt [lemma, in mathcomp_eulerian.reflection]
andre_target [definition, in mathcomp_eulerian.reflection]
apply_psis_cat [lemma, in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_nil [lemma, in mathcomp_eulerian.psi_cdindex_defs]
apply_psis [definition, in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_size_eq [lemma, in mathcomp_eulerian.perm_seq_bridge]
apply_psis_cancel [lemma, in mathcomp_eulerian.perm_seq_bridge]
apply_psis_revK [lemma, in mathcomp_eulerian.perm_seq_bridge]
apply_psis_rev [lemma, in mathcomp_eulerian.perm_seq_bridge]
asc [definition, in mathcomp_eulerian.descent]
AsPermMaxBounds [section, in mathcomp_eulerian.altsub]
AsPermMaxBoundsM [section, in mathcomp_eulerian.altsub]
AsPermMaxBoundsM.n [variable, in mathcomp_eulerian.altsub]
AsPermMaxBounds.n [variable, in mathcomp_eulerian.altsub]
AssembleDecompFull [section, in mathcomp_eulerian.reflection]
AssembleDecompFull.Hx0L [variable, in mathcomp_eulerian.reflection]
AssembleDecompFull.Hx0R [variable, in mathcomp_eulerian.reflection]
AssembleDecompFull.j [variable, in mathcomp_eulerian.reflection]
AssembleDecompFull.n [variable, in mathcomp_eulerian.reflection]
AssembleDecompFull.t [variable, in mathcomp_eulerian.reflection]
AssembleDecompFull.x0L [variable, in mathcomp_eulerian.reflection]
AssembleDecompFull.x0R [variable, in mathcomp_eulerian.reflection]
AssembleForwardLeft [section, in mathcomp_eulerian.reflection]
AssembleForwardLeft.Hx0L [variable, in mathcomp_eulerian.reflection]
AssembleForwardLeft.Hx0R [variable, in mathcomp_eulerian.reflection]
AssembleForwardLeft.j [variable, in mathcomp_eulerian.reflection]
AssembleForwardLeft.n [variable, in mathcomp_eulerian.reflection]
AssembleForwardLeft.t [variable, in mathcomp_eulerian.reflection]
AssembleForwardLeft.x0L [variable, in mathcomp_eulerian.reflection]
AssembleForwardLeft.x0R [variable, in mathcomp_eulerian.reflection]
AssembleForwardRight [section, in mathcomp_eulerian.reflection]
AssembleForwardRight.Hx0L [variable, in mathcomp_eulerian.reflection]
AssembleForwardRight.Hx0R [variable, in mathcomp_eulerian.reflection]
AssembleForwardRight.j [variable, in mathcomp_eulerian.reflection]
AssembleForwardRight.n [variable, in mathcomp_eulerian.reflection]
AssembleForwardRight.t [variable, in mathcomp_eulerian.reflection]
AssembleForwardRight.x0L [variable, in mathcomp_eulerian.reflection]
AssembleForwardRight.x0R [variable, in mathcomp_eulerian.reflection]
AssemblePermLeftRT [section, in mathcomp_eulerian.reflection]
AssemblePermLeftRT.HL [variable, in mathcomp_eulerian.reflection]
AssemblePermLeftRT.j [variable, in mathcomp_eulerian.reflection]
AssemblePermLeftRT.L [variable, in mathcomp_eulerian.reflection]
AssemblePermLeftRT.n [variable, in mathcomp_eulerian.reflection]
AssemblePermLeftRT.sL [variable, in mathcomp_eulerian.reflection]
AssemblePermLeftRT.sR [variable, in mathcomp_eulerian.reflection]
AssemblePermLeftRT.t [variable, in mathcomp_eulerian.reflection]
AssembleRoundTrip [section, in mathcomp_eulerian.reflection]
AssembleRoundTrip.HL [variable, in mathcomp_eulerian.reflection]
AssembleRoundTrip.j [variable, in mathcomp_eulerian.reflection]
AssembleRoundTrip.L [variable, in mathcomp_eulerian.reflection]
AssembleRoundTrip.n [variable, in mathcomp_eulerian.reflection]
AssembleRoundTrip.sL [variable, in mathcomp_eulerian.reflection]
AssembleRoundTrip.sR [variable, in mathcomp_eulerian.reflection]
AssembleRoundTrip.t [variable, in mathcomp_eulerian.reflection]
AssembleUnique [section, in mathcomp_eulerian.reflection]
AssembleUnique.HL [variable, in mathcomp_eulerian.reflection]
AssembleUnique.j [variable, in mathcomp_eulerian.reflection]
AssembleUnique.L [variable, in mathcomp_eulerian.reflection]
AssembleUnique.n [variable, in mathcomp_eulerian.reflection]
AssembleUnique.sL [variable, in mathcomp_eulerian.reflection]
AssembleUnique.sR [variable, in mathcomp_eulerian.reflection]
AssembleUnique.t [variable, in mathcomp_eulerian.reflection]
assemble_decomp_inverse_gen [lemma, in mathcomp_eulerian.reflection]
assemble_perm_pirr [lemma, in mathcomp_eulerian.reflection]
assemble_decomp_unique [lemma, in mathcomp_eulerian.reflection]
assemble_decomp_inverse [lemma, in mathcomp_eulerian.reflection]
assemble_decomp_inverse_right [lemma, in mathcomp_eulerian.reflection]
assemble_decomp_inverse_left [lemma, in mathcomp_eulerian.reflection]
assemble_perm_right [lemma, in mathcomp_eulerian.reflection]
assemble_perm_left [lemma, in mathcomp_eulerian.reflection]
assemble_image_right [lemma, in mathcomp_eulerian.reflection]
assemble_image_left [lemma, in mathcomp_eulerian.reflection]
assemble_right [lemma, in mathcomp_eulerian.reflection]
assemble_left [lemma, in mathcomp_eulerian.reflection]
assemble_permE [lemma, in mathcomp_eulerian.reflection]
assemble_perm [definition, in mathcomp_eulerian.reflection]
assemble_fun_inj [lemma, in mathcomp_eulerian.reflection]
assemble_fun [definition, in mathcomp_eulerian.reflection]
as_perm_max_eq [lemma, in mathcomp_eulerian.altsub]
as_perm_max_upper [lemma, in mathcomp_eulerian.altsub]
as_perm_max_lower [lemma, in mathcomp_eulerian.altsub]
as_perm_max_le_size [lemma, in mathcomp_eulerian.altsub]
as_perm_alt_desc [lemma, in mathcomp_eulerian.altsub]
as_permE [lemma, in mathcomp_eulerian.altsub]
as_perm [definition, in mathcomp_eulerian.altsub]
as_perm_max [definition, in mathcomp_eulerian.altsub]
aux_id [lemma, in mathcomp_eulerian.eulerian]
aux_id_step [lemma, in mathcomp_eulerian.eulerian]

B

beta [definition, in mathcomp_eulerian.beta]
beta [library]
beta_alt_max [lemma, in mathcomp_eulerian.beta_swap]
beta_set_is_alt_eq [lemma, in mathcomp_eulerian.beta_swap]
beta_compl [lemma, in mathcomp_eulerian.beta_swap]
beta_rev [lemma, in mathcomp_eulerian.beta]
beta_eulerian [lemma, in mathcomp_eulerian.beta]
beta_full [lemma, in mathcomp_eulerian.beta]
beta_andre_right [lemma, in mathcomp_eulerian.reflection]
beta_andre_left [lemma, in mathcomp_eulerian.reflection]
beta_eq_triple_split [lemma, in mathcomp_eulerian.reflection]
beta_eq_double_sum [lemma, in mathcomp_eulerian.reflection]
beta_eq_pair_sum [lemma, in mathcomp_eulerian.reflection]
beta_swap [library]
beta_bridge [library]
beta_omega [library]
beta0 [lemma, in mathcomp_eulerian.beta]
binf_neq0 [lemma, in mathcomp_fps.fps_egf]
binS' [lemma, in mathcomp_eulerian.eulerian]
block_chain_values [lemma, in mathcomp_eulerian.beta_omega]
block_chain_step [lemma, in mathcomp_eulerian.beta_omega]
block_descent_chain [lemma, in mathcomp_eulerian.beta_omega]
block_right_descent [lemma, in mathcomp_eulerian.beta_omega]
block_left_descent [lemma, in mathcomp_eulerian.beta_omega]
block_right_ge [lemma, in mathcomp_eulerian.beta_omega]
block_left_le [lemma, in mathcomp_eulerian.beta_omega]
block_right_max [lemma, in mathcomp_eulerian.beta_omega]
block_left_min [lemma, in mathcomp_eulerian.beta_omega]
block_right_right_ok [lemma, in mathcomp_eulerian.beta_omega]
block_left_left_ok [lemma, in mathcomp_eulerian.beta_omega]
block_right [definition, in mathcomp_eulerian.beta_omega]
block_left [definition, in mathcomp_eulerian.beta_omega]
bool_triangle [lemma, in mathcomp_eulerian.altsub]
boundary_cancellation_alt [lemma, in mathcomp_eulerian.reflection]
Bridges [section, in mathcomp_eulerian.psi_descent_v2]
Bridges.Hmm [variable, in mathcomp_eulerian.psi_descent_v2]
Bridges.s [variable, in mathcomp_eulerian.psi_descent_v2]
Bridges.sl [variable, in mathcomp_eulerian.psi_descent_v2]
Bridges.sr [variable, in mathcomp_eulerian.psi_descent_v2]
Bridges.x [variable, in mathcomp_eulerian.psi_descent_v2]
bwdAss [definition, in mathcomp_eulerian.reflection]
bwd_fwd [lemma, in mathcomp_eulerian.reflection]

C

Cancellation [section, in mathcomp_eulerian.perm_compress]
Cancellation.n [variable, in mathcomp_eulerian.perm_compress]
cardCL_eq [lemma, in mathcomp_eulerian.reflection]
card_turn_witness [lemma, in mathcomp_eulerian.altsub]
card_turn_image [lemma, in mathcomp_eulerian.altsub]
card_split_ord_pair [lemma, in mathcomp_eulerian.inversions]
card_ord_pair [lemma, in mathcomp_eulerian.inversions]
card_split_lt_gt [lemma, in mathcomp_eulerian.qeul_rec]
card_rank_gt [lemma, in mathcomp_eulerian.qeul_rec]
card_rank_lt [lemma, in mathcomp_eulerian.qeul_rec]
card_ord_ltb [lemma, in mathcomp_eulerian.qeul_rec]
card_image_left_eq [definition, in mathcomp_eulerian.reflection]
card_image_right [lemma, in mathcomp_eulerian.reflection]
card_image_left [lemma, in mathcomp_eulerian.reflection]
card_eq_ord_max_fiber [lemma, in mathcomp_eulerian.stirling_fiber]
card_neq_ord_max_fiber [lemma, in mathcomp_eulerian.stirling_fiber]
carlitz [lemma, in mathcomp_eulerian.carlitz]
carlitz [library]
carlitz_inv [lemma, in mathcomp_eulerian.carlitz]
carlitz_div [lemma, in mathcomp_eulerian.carlitz]
castL [definition, in mathcomp_eulerian.reflection]
castR [definition, in mathcomp_eulerian.reflection]
cast_to_subj_inj [lemma, in mathcomp_eulerian.reflection]
cast_to_subj [definition, in mathcomp_eulerian.reflection]
cast_to_j_inj [lemma, in mathcomp_eulerian.reflection]
cast_to_j [definition, in mathcomp_eulerian.reflection]
cde [inductive, in mathcomp_eulerian.psi_cdindex_defs]
cde_total_width_phi_w [lemma, in mathcomp_eulerian.psi_cdindex_support]
cde_total_width_phi_w_all [lemma, in mathcomp_eulerian.psi_cdindex_support]
cde_sind [definition, in mathcomp_eulerian.psi_cdindex_defs]
cde_rec [definition, in mathcomp_eulerian.psi_cdindex_defs]
cde_ind [definition, in mathcomp_eulerian.psi_cdindex_defs]
cde_rect [definition, in mathcomp_eulerian.psi_cdindex_defs]
cde_total_width_cat [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset_D_succ [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset_C_succ [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_total_width [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_width [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
char_mono_apply_psis_D_bit_self [lemma, in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_D_bit_pred [lemma, in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_C_bit [lemma, in mathcomp_eulerian.psi_cdindex_core]
char_mono_psi_effect [lemma, in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_inj [lemma, in mathcomp_eulerian.psi_cdindex_support]
char_mono_apply_psis_mem [lemma, in mathcomp_eulerian.psi_cdindex_support]
char_mono_self_mem [lemma, in mathcomp_eulerian.psi_cdindex_support]
char_mono [definition, in mathcomp_eulerian.psi_cdindex_defs]
char_mono_in_expand_cde [lemma, in mathcomp_eulerian.perm_seq_bridge]
char_mono_class_inj [lemma, in mathcomp_eulerian.perm_seq_bridge]
char_mono_perm_to_seq [lemma, in mathcomp_eulerian.perm_seq_bridge]
check_fact3_size1 [lemma, in mathcomp_eulerian.psi_cdindex_core]
check_fact3P [lemma, in mathcomp_eulerian.psi_cdindex_core]
check_fact3 [definition, in mathcomp_eulerian.psi_cdindex_core]
check_fact3_true [lemma, in mathcomp_eulerian.psi_cdindex_support]
check_fact3_of_perm_eq [lemma, in mathcomp_eulerian.psi_cdindex_support]
check_strict_witness_correct [lemma, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_2 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_0 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_4_1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_4_0 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_3_0 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_strict_witness [definition, in mathcomp_eulerian.psi_cdindex_witness]
classify_vertex_mm [lemma, in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_right [lemma, in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_left [lemma, in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_cde_psi [lemma, in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_cde [definition, in mathcomp_eulerian.psi_cdindex_defs]
classify_map_succ [lemma, in mathcomp_eulerian.psi_cdindex_witness]
classify_skip_mm0 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
class_map [definition, in mathcomp_eulerian.perm_seq_bridge]
class_char_monos_uniq [lemma, in mathcomp_eulerian.perm_seq_bridge]
cmp_out_of_range_left [lemma, in mathcomp_eulerian.psi_descent_thms]
cmp_out_of_range [lemma, in mathcomp_eulerian.psi_descent_thms]
coefM_eql [lemma, in mathcomp_fps.fps]
coefM_eqr [lemma, in mathcomp_fps.fps]
coef_fpsXfM [lemma, in mathcomp_eulerian.stirling_egf]
coef_stirling_pol [lemma, in mathcomp_eulerian.stirling_egf]
coef_fps_primS [lemma, in mathcomp_fps.fps_deriv]
coef_fps_prim0 [lemma, in mathcomp_fps.fps_deriv]
coef_fps_deriv [lemma, in mathcomp_fps.fps_deriv]
coef_egf [lemma, in mathcomp_fps.fps_egf]
coef_fps_comp_trunc [lemma, in mathcomp_fps.fps_comp]
coef_comp_poly_eqp [lemma, in mathcomp_fps.fps_comp]
coef_comp_poly_wide [lemma, in mathcomp_fps.fps_comp]
coef_polyXn_small [lemma, in mathcomp_fps.fps_comp]
coef_fpsXn_trunc [lemma, in mathcomp_fps.fps_comp]
coef_fpsXn_small [lemma, in mathcomp_fps.fps_comp]
coef_fps_comp [lemma, in mathcomp_fps.fps_comp]
coef_q_eul_pol [lemma, in mathcomp_eulerian.qworpitzky]
coef_fps_geomXn [lemma, in mathcomp_fps.fps_ogf]
coef_fpsXfM' [lemma, in mathcomp_eulerian.carlitz]
coef_eul_pol [lemma, in mathcomp_eulerian.worpitzky]
coef_fps_onesubX [lemma, in mathcomp_fps.fps]
coef_poly_fps [lemma, in mathcomp_fps.fps]
coef_fpsZ [lemma, in mathcomp_fps.fps]
coef_fpsM [lemma, in mathcomp_fps.fps]
coef_fps1 [lemma, in mathcomp_fps.fps]
coef_fpsM_trunc [lemma, in mathcomp_fps.fps]
coef_fps_trunc [lemma, in mathcomp_fps.fps]
coef_fps_sum [lemma, in mathcomp_fps.fps]
coef_fpsB [lemma, in mathcomp_fps.fps]
coef_fpsN [lemma, in mathcomp_fps.fps]
coef_fpsD [lemma, in mathcomp_fps.fps]
coef_fps0 [lemma, in mathcomp_fps.fps]
coef0_fps_log [lemma, in mathcomp_fps.fps_explog]
coef0_fps_exp [lemma, in mathcomp_fps.fps_explog]
coef0_fps_comp [lemma, in mathcomp_fps.fps_comp]
coef0_fpsM [lemma, in mathcomp_fps.fps]
coinv_set [definition, in mathcomp_eulerian.inversions]
compl_perm_involutive [lemma, in mathcomp_eulerian.beta_swap]
compl_perm_inj [lemma, in mathcomp_eulerian.beta_swap]
compl_permE [lemma, in mathcomp_eulerian.beta_swap]
compl_perm [definition, in mathcomp_eulerian.beta_swap]
constant_descent_monotone [lemma, in mathcomp_eulerian.altsub]
cosf [definition, in mathcomp_fps.fps_trig]
cosf_deriv [lemma, in mathcomp_fps.fps_trig]
cosf_unit [lemma, in mathcomp_fps.fps_trig]
cosf0 [lemma, in mathcomp_fps.fps_trig]
cos_mul_sec [lemma, in mathcomp_fps.fps_trig]
count_lt [definition, in mathcomp_eulerian.foata]
count_gt_cat [lemma, in mathcomp_eulerian.foata]
count_gt_perm_eq [lemma, in mathcomp_eulerian.foata]
count_gt [definition, in mathcomp_eulerian.foata]
cross_inv_perm_eq_l [lemma, in mathcomp_eulerian.foata]
cross_inv_perm_eq_r [lemma, in mathcomp_eulerian.foata]
cross_inv_rcons [lemma, in mathcomp_eulerian.foata]
cross_inv_nil_r [lemma, in mathcomp_eulerian.foata]
cross_inv [definition, in mathcomp_eulerian.foata]
CycleBasic [section, in mathcomp_eulerian.cycles]
CycleCountInsertAfter [section, in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.j0 [variable, in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.n [variable, in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.s [variable, in mathcomp_eulerian.stirling_fiber]
cycles [library]
cycles_rec [library]
cycle_count_id [lemma, in mathcomp_eulerian.cycles]
cycle_count_le [lemma, in mathcomp_eulerian.cycles]
cycle_count [definition, in mathcomp_eulerian.cycles]
cycle_count_lift_perm_id [lemma, in mathcomp_eulerian.cycles_rec]
cycle_count_insert_after [lemma, in mathcomp_eulerian.stirling_fiber]
cyc_first_to_backK [lemma, in mathcomp_eulerian.foata]
cyc_first_to_back_perm_eq [lemma, in mathcomp_eulerian.foata]
cyc_first_to_back [definition, in mathcomp_eulerian.foata]
cyc_diff_block_gt [lemma, in mathcomp_eulerian.foata]
cyc_diff_block_lt [lemma, in mathcomp_eulerian.foata]
cyc_last_to_front_rcons [lemma, in mathcomp_eulerian.foata]
cyc_last_to_front_perm_eq [lemma, in mathcomp_eulerian.foata]
cyc_last_to_front [definition, in mathcomp_eulerian.foata]
C_letter [constructor, in mathcomp_eulerian.psi_cdindex_defs]

D

des [definition, in mathcomp_eulerian.descent]
Descent [section, in mathcomp_eulerian.descent]
descent [library]
DescentDrop [section, in mathcomp_eulerian.descent]
DescentDrop.n [variable, in mathcomp_eulerian.descent]
DescentReverse [section, in mathcomp_eulerian.descent]
DescentReverse.n [variable, in mathcomp_eulerian.descent]
DescentSplit [section, in mathcomp_eulerian.reflection]
DescentSplitRight [section, in mathcomp_eulerian.reflection]
DescentSplitRight.Hjn [variable, in mathcomp_eulerian.reflection]
DescentSplitRight.j [variable, in mathcomp_eulerian.reflection]
DescentSplitRight.n [variable, in mathcomp_eulerian.reflection]
DescentSplitRight.t [variable, in mathcomp_eulerian.reflection]
DescentSplit.Hk [variable, in mathcomp_eulerian.reflection]
DescentSplit.Hkn [variable, in mathcomp_eulerian.reflection]
DescentSplit.j [variable, in mathcomp_eulerian.reflection]
DescentSplit.k [variable, in mathcomp_eulerian.reflection]
DescentSplit.n [variable, in mathcomp_eulerian.reflection]
DescentSplit.t [variable, in mathcomp_eulerian.reflection]
DescentTranslate [section, in mathcomp_eulerian.reflection]
DescentTranslateRight [section, in mathcomp_eulerian.reflection]
DescentTranslateRight.Hj [variable, in mathcomp_eulerian.reflection]
DescentTranslateRight.j [variable, in mathcomp_eulerian.reflection]
DescentTranslateRight.n [variable, in mathcomp_eulerian.reflection]
DescentTranslateRight.t [variable, in mathcomp_eulerian.reflection]
DescentTranslate.Hk [variable, in mathcomp_eulerian.reflection]
DescentTranslate.Hkn [variable, in mathcomp_eulerian.reflection]
DescentTranslate.j [variable, in mathcomp_eulerian.reflection]
DescentTranslate.k [variable, in mathcomp_eulerian.reflection]
DescentTranslate.n [variable, in mathcomp_eulerian.reflection]
DescentTranslate.t [variable, in mathcomp_eulerian.reflection]
descent_psi_effect [lemma, in mathcomp_eulerian.psi_cdindex_core]
descent_psi_LR_swap1_ex [definition, in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap2_ex [definition, in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_remove_ex [definition, in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_add_ex [definition, in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap2 [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap1 [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_remove [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_add [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_lboundary_R [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_rboundary [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_interior [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_set_compl [lemma, in mathcomp_eulerian.beta_swap]
descent_set_full_rev [lemma, in mathcomp_eulerian.beta]
descent_set_rev_perm_ord [lemma, in mathcomp_eulerian.beta]
descent_set_rev_perm [lemma, in mathcomp_eulerian.beta]
descent_to_bvec_inj [lemma, in mathcomp_eulerian.perm_seq_basics]
descent_to_bvec [definition, in mathcomp_eulerian.perm_seq_basics]
descent_set [definition, in mathcomp_eulerian.descent]
descent_right_part_R_image [lemma, in mathcomp_eulerian.reflection]
descent_right_part_R [definition, in mathcomp_eulerian.reflection]
descent_left_part_image [lemma, in mathcomp_eulerian.reflection]
descent_boundary_right_disjoint [lemma, in mathcomp_eulerian.reflection]
descent_left_right_disjoint [lemma, in mathcomp_eulerian.reflection]
descent_left_boundary_disjoint [lemma, in mathcomp_eulerian.reflection]
descent_set_decomp_partition [lemma, in mathcomp_eulerian.reflection]
descent_right_part [definition, in mathcomp_eulerian.reflection]
descent_boundary_part [definition, in mathcomp_eulerian.reflection]
descent_left_part [definition, in mathcomp_eulerian.reflection]
descent_right_of_t [lemma, in mathcomp_eulerian.reflection]
descent_left_of_t [lemma, in mathcomp_eulerian.reflection]
descent_set_insert_max_interior [lemma, in mathcomp_eulerian.reflection]
descent_set_insert_max_ord_max [lemma, in mathcomp_eulerian.reflection]
descent_set_insert_max_ord0 [lemma, in mathcomp_eulerian.reflection]
Descent.n [variable, in mathcomp_eulerian.descent]
desc_positions_bvec [lemma, in mathcomp_eulerian.perm_seq_basics]
DesInsertMax [section, in mathcomp_eulerian.eulerian]
DesInsertMax.n [variable, in mathcomp_eulerian.eulerian]
DesInsertMax.t [variable, in mathcomp_eulerian.eulerian]
des_insert_max_interior [lemma, in mathcomp_eulerian.eulerian]
des_insert_max_ord_max [lemma, in mathcomp_eulerian.eulerian]
des_insert_max_ord0 [lemma, in mathcomp_eulerian.eulerian]
des_rev_perm [lemma, in mathcomp_eulerian.descent]
des_id [lemma, in mathcomp_eulerian.descent]
des_add_asc [lemma, in mathcomp_eulerian.descent]
des_le [lemma, in mathcomp_eulerian.descent]
des0_id [lemma, in mathcomp_eulerian.eulerian]
dir_right_of_turn [lemma, in mathcomp_eulerian.altsub]
dir_left_of_turn [lemma, in mathcomp_eulerian.altsub]
DropPerm [section, in mathcomp_eulerian.perm_compress]
DropPerm.n [variable, in mathcomp_eulerian.perm_compress]
DropPerm.s [variable, in mathcomp_eulerian.perm_compress]
drop_permE [lemma, in mathcomp_eulerian.perm_compress]
drop_perm [definition, in mathcomp_eulerian.perm_compress]
drop_fun_inj [lemma, in mathcomp_eulerian.perm_compress]
drop_funE [lemma, in mathcomp_eulerian.perm_compress]
drop_fun [definition, in mathcomp_eulerian.perm_compress]
drop_fun_ne [lemma, in mathcomp_eulerian.perm_compress]
drop_mm_eq [lemma, in mathcomp_eulerian.psi_descent_v2]
drop_psi_above [lemma, in mathcomp_eulerian.psi_core]
drop_mm_psi [lemma, in mathcomp_eulerian.psi_core]
drop_psi [lemma, in mathcomp_eulerian.psi_core]
drop1_witness_map_succ [lemma, in mathcomp_eulerian.psi_cdindex_witness]
D_vertex_descent_transition [lemma, in mathcomp_eulerian.psi_cdindex_support]
D_offsets_phi_w_eq_S_w_seq [lemma, in mathcomp_eulerian.psi_cdindex_support]
D_offsets_cat_D [lemma, in mathcomp_eulerian.psi_cdindex_support]
D_offsets_cons_C [lemma, in mathcomp_eulerian.psi_cdindex_support]
D_letter [constructor, in mathcomp_eulerian.psi_cdindex_defs]
D_offsets [definition, in mathcomp_eulerian.psi_cdindex_support_defs]

E

egf [definition, in mathcomp_fps.fps_egf]
Egf [section, in mathcomp_fps.fps_egf]
egfD [lemma, in mathcomp_fps.fps_egf]
egfZ [lemma, in mathcomp_fps.fps_egf]
egf_deriv [lemma, in mathcomp_fps.fps_egf]
egf_mul [lemma, in mathcomp_fps.fps_egf]
egf_dirac [lemma, in mathcomp_fps.fps_egf]
egf_eq [lemma, in mathcomp_fps.fps_egf]
Egf.charF0 [variable, in mathcomp_fps.fps_egf]
Egf.F [variable, in mathcomp_fps.fps_egf]
elem_rs_in_range [lemma, in mathcomp_eulerian.psi_descent_thms]
elem_in_range [lemma, in mathcomp_eulerian.psi_descent_thms]
embed_desc_right [definition, in mathcomp_eulerian.reflection]
embed_desc_left [definition, in mathcomp_eulerian.reflection]
embed_right_inj [lemma, in mathcomp_eulerian.reflection]
embed_right [definition, in mathcomp_eulerian.reflection]
embed_left_inj [lemma, in mathcomp_eulerian.reflection]
embed_left [definition, in mathcomp_eulerian.reflection]
endpoint_next_has_left_child_ex2 [definition, in mathcomp_eulerian.psi_cdindex_tree]
endpoint_next_has_left_child_ex [definition, in mathcomp_eulerian.psi_cdindex_tree]
endpoint_implies_next_has_left_child [lemma, in mathcomp_eulerian.psi_cdindex_tree]
endpoint_implies_next_t [lemma, in mathcomp_eulerian.psi_cdindex_tree]
enum_ord_split [lemma, in mathcomp_eulerian.altsub]
enum_rank_in_val_ltn [lemma, in mathcomp_eulerian.reflection]
enum_val_ltn [lemma, in mathcomp_eulerian.reflection]
enum_val_perm_right [lemma, in mathcomp_eulerian.reflection]
enum_val_perm_left [lemma, in mathcomp_eulerian.reflection]
Equidistribution [section, in mathcomp_eulerian.foata]
Equidistribution.FoataPerm [section, in mathcomp_eulerian.foata]
Equidistribution.FoataPerm.n [variable, in mathcomp_eulerian.foata]
eq_egf [lemma, in mathcomp_fps.fps_egf]
euler [definition, in mathcomp_eulerian.reflection]
eulerA [definition, in mathcomp_eulerian.reflection]
eulerA_S2 [lemma, in mathcomp_eulerian.reflection]
eulerA_2 [lemma, in mathcomp_eulerian.reflection]
eulerA_1 [lemma, in mathcomp_eulerian.reflection]
eulerA_0 [lemma, in mathcomp_eulerian.reflection]
eulerian [definition, in mathcomp_eulerian.eulerian]
eulerian [library]
EulerianBasic [section, in mathcomp_eulerian.eulerian]
eulerian_explicit [lemma, in mathcomp_eulerian.eulerian]
eulerian_rec [lemma, in mathcomp_eulerian.eulerian]
eulerian_n_n [lemma, in mathcomp_eulerian.eulerian]
eulerian_symm [lemma, in mathcomp_eulerian.eulerian]
eulerian_n_0 [lemma, in mathcomp_eulerian.eulerian]
eulerian_out_of_range [lemma, in mathcomp_eulerian.eulerian]
eulerian_row_sum_fact [lemma, in mathcomp_eulerian.eulerian]
eulerian_row_sum [lemma, in mathcomp_eulerian.eulerian]
euler_egf_ode [lemma, in mathcomp_eulerian.stanley_egf]
euler_egf0 [lemma, in mathcomp_eulerian.stanley_egf]
euler_egf [definition, in mathcomp_eulerian.stanley_egf]
euler_rec_n2_via [definition, in mathcomp_eulerian.reflection]
euler_rec_n1_via [definition, in mathcomp_eulerian.reflection]
euler_rec_n0_direct [definition, in mathcomp_eulerian.reflection]
euler_rec_n0 [definition, in mathcomp_eulerian.reflection]
euler_rec [lemma, in mathcomp_eulerian.reflection]
euler_1 [lemma, in mathcomp_eulerian.reflection]
euler_0 [lemma, in mathcomp_eulerian.reflection]
eul_pol [definition, in mathcomp_eulerian.qeul]
exactly_one_descent_LR_ex [definition, in mathcomp_eulerian.psi_descent_v2]
exactly_one_descent_LR [lemma, in mathcomp_eulerian.psi_descent_v2]
ExistenceLB [section, in mathcomp_eulerian.altsub]
ExistenceLB.n [variable, in mathcomp_eulerian.altsub]
expand_cde [definition, in mathcomp_eulerian.psi_cdindex_defs]
expand_cde_mem_iff [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
expand_cde_mem_transitions [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
expf [definition, in mathcomp_fps.fps_trig]
expf_deriv [lemma, in mathcomp_fps.fps_trig]
expf0 [lemma, in mathcomp_fps.fps_trig]
ExtractMax [section, in mathcomp_eulerian.eulerian]
ExtractMax.n [variable, in mathcomp_eulerian.eulerian]
ExtractMax.p [variable, in mathcomp_eulerian.eulerian]
ExtractMax.s [variable, in mathcomp_eulerian.eulerian]
ExtractMax.sp [variable, in mathcomp_eulerian.eulerian]
extract_max_widen [lemma, in mathcomp_eulerian.eulerian]
extract_max_permE [lemma, in mathcomp_eulerian.eulerian]
extract_max_perm [definition, in mathcomp_eulerian.eulerian]
extract_max_fun_inj [lemma, in mathcomp_eulerian.eulerian]
extract_max_funE [lemma, in mathcomp_eulerian.eulerian]
extract_max_fun [definition, in mathcomp_eulerian.eulerian]
extract_max_ne [lemma, in mathcomp_eulerian.eulerian]
ex_roundtrip_compute [definition, in mathcomp_eulerian.mmtree]
ex_roundtrip [definition, in mathcomp_eulerian.mmtree]
ex_nontrivial [definition, in mathcomp_eulerian.mmtree]
ex_seq [definition, in mathcomp_eulerian.mmtree]
E_letter [constructor, in mathcomp_eulerian.psi_cdindex_defs]

F

factf_neq0 [lemma, in mathcomp_fps.fps_egf]
factU [lemma, in mathcomp_fps.fps_explog]
factU_polyrat [lemma, in mathcomp_eulerian.stirling_egf]
fact3 [lemma, in mathcomp_eulerian.psi_cdindex_support]
fact3_ex_213 [definition, in mathcomp_eulerian.psi_cdindex_support]
fact3_ex_315426 [definition, in mathcomp_eulerian.psi_cdindex_support]
find_ss_spec [lemma, in mathcomp_eulerian.perm_seq_bridge]
find_ss [definition, in mathcomp_eulerian.perm_seq_bridge]
flip_count_perm_seq_eq_turn_count [lemma, in mathcomp_eulerian.altsub]
flip_count_as_sum [lemma, in mathcomp_eulerian.altsub]
flip_count_pick_le_perm [lemma, in mathcomp_eulerian.altsub]
flip_count_is_alt_bool [lemma, in mathcomp_eulerian.altsub]
flip_count_sign_seq_le_subseq [lemma, in mathcomp_eulerian.altsub]
flip_count_pairmap_le_subseq [lemma, in mathcomp_eulerian.altsub]
flip_count_sign_seq_insert_front [lemma, in mathcomp_eulerian.altsub]
flip_count_pairmap_insert_anywhere [lemma, in mathcomp_eulerian.altsub]
flip_step_helper [lemma, in mathcomp_eulerian.altsub]
flip_count_pairmap_insert [lemma, in mathcomp_eulerian.altsub]
flip_count [definition, in mathcomp_eulerian.altsub]
foata [definition, in mathcomp_eulerian.foata]
foata [library]
FoataBlocks [section, in mathcomp_eulerian.beta_omega]
FoataBlocks.n [variable, in mathcomp_eulerian.beta_omega]
foata_perm_inj [lemma, in mathcomp_eulerian.foata]
foata_perm_inv_maj [lemma, in mathcomp_eulerian.foata]
foata_perm [definition, in mathcomp_eulerian.foata]
foata_perm_to_seq_bnd [lemma, in mathcomp_eulerian.foata]
foata_perm_to_seq_uniq [lemma, in mathcomp_eulerian.foata]
foata_perm_to_seq_size [lemma, in mathcomp_eulerian.foata]
foata_inj_uniq [lemma, in mathcomp_eulerian.foata]
foata_invK [lemma, in mathcomp_eulerian.foata]
foata_invK_aux [lemma, in mathcomp_eulerian.foata]
foata_inv [definition, in mathcomp_eulerian.foata]
foata_inv_aux [definition, in mathcomp_eulerian.foata]
foata_step_undoK [lemma, in mathcomp_eulerian.foata]
foata_step_undo [definition, in mathcomp_eulerian.foata]
foata_inv_eq_maj [lemma, in mathcomp_eulerian.foata]
foata_step_inv [lemma, in mathcomp_eulerian.foata]
foata_step_inv_gt [lemma, in mathcomp_eulerian.foata]
foata_step_inv_lt [lemma, in mathcomp_eulerian.foata]
foata_last_eq [lemma, in mathcomp_eulerian.foata]
foata_last [lemma, in mathcomp_eulerian.foata]
foata_rcons [lemma, in mathcomp_eulerian.foata]
foata_step_last [lemma, in mathcomp_eulerian.foata]
foata_uniq [lemma, in mathcomp_eulerian.foata]
foata_size [lemma, in mathcomp_eulerian.foata]
foata_perm_eq [lemma, in mathcomp_eulerian.foata]
foata_step_perm_eq [lemma, in mathcomp_eulerian.foata]
foata_step [definition, in mathcomp_eulerian.foata]
foldr_maxn_ge [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
foldr_minn_all_gt' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
foldr_minn_ge' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_path' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_set_to_seq_lb [lemma, in mathcomp_eulerian.beta_bridge]
foldr_maxn_ge_nth [lemma, in mathcomp_eulerian.psi_core]
foldr_minn_le_nth [lemma, in mathcomp_eulerian.psi_core]
foldr_maxn_ge [lemma, in mathcomp_eulerian.psi_core]
foldr_maxn_aux [lemma, in mathcomp_eulerian.psi_core]
foldr_minn_le [lemma, in mathcomp_eulerian.psi_core]
foldr_minn_aux [lemma, in mathcomp_eulerian.psi_core]
fps [record, in mathcomp_fps.fps]
fps [library]
fpscoef [projection, in mathcomp_fps.fps]
FpsComp [section, in mathcomp_fps.fps_comp]
FpsCompUnit [section, in mathcomp_fps.fps_comp]
FpsCompUnit.R [variable, in mathcomp_fps.fps_comp]
FpsComp.R [variable, in mathcomp_fps.fps_comp]
FpsDeriv [section, in mathcomp_fps.fps_deriv]
FpsDerivChar0 [section, in mathcomp_fps.fps_deriv]
FpsDerivChar0.charF0 [variable, in mathcomp_fps.fps_deriv]
FpsDerivChar0.F [variable, in mathcomp_fps.fps_deriv]
FpsDeriv.R [variable, in mathcomp_fps.fps_deriv]
FpsExpLog [section, in mathcomp_fps.fps_explog]
FpsExpLog.natU [variable, in mathcomp_fps.fps_explog]
FpsExpLog.R [variable, in mathcomp_fps.fps_explog]
FpsExt [section, in mathcomp_fps.fps]
FpsExt.R [variable, in mathcomp_fps.fps]
FpsOde [section, in mathcomp_fps.fps_ode]
FpsOde.charF0 [variable, in mathcomp_fps.fps_ode]
FpsOde.F [variable, in mathcomp_fps.fps_ode]
fpsP [lemma, in mathcomp_fps.fps]
FpsRing [section, in mathcomp_fps.fps]
FpsRing.R [variable, in mathcomp_fps.fps]
FpsUnitRing [section, in mathcomp_fps.fps]
FpsUnitRing.R [variable, in mathcomp_fps.fps]
FpsZmod [section, in mathcomp_fps.fps]
FpsZmod.R [variable, in mathcomp_fps.fps]
fps_geom_deriv [lemma, in mathcomp_eulerian.stirling_egf]
fps_exp_log_geom [lemma, in mathcomp_fps.fps_explog]
fps_expK [lemma, in mathcomp_fps.fps_explog]
fps_logK [lemma, in mathcomp_fps.fps_explog]
fps_expD [lemma, in mathcomp_fps.fps_explog]
fps_deriv_inj0U [lemma, in mathcomp_fps.fps_explog]
fps_lin_ode_uniq [lemma, in mathcomp_fps.fps_explog]
fps_log_deriv [lemma, in mathcomp_fps.fps_explog]
fps_exp_deriv [lemma, in mathcomp_fps.fps_explog]
fps_unit1 [lemma, in mathcomp_fps.fps_explog]
fps_exp_unit [lemma, in mathcomp_fps.fps_explog]
fps_log [definition, in mathcomp_fps.fps_explog]
fps_exp [definition, in mathcomp_fps.fps_explog]
fps_l_deriv [lemma, in mathcomp_fps.fps_explog]
fps_e_deriv [lemma, in mathcomp_fps.fps_explog]
fps_l0 [lemma, in mathcomp_fps.fps_explog]
fps_e0 [lemma, in mathcomp_fps.fps_explog]
fps_l [definition, in mathcomp_fps.fps_explog]
fps_e [definition, in mathcomp_fps.fps_explog]
fps_deriv_inj0 [lemma, in mathcomp_fps.fps_deriv]
fps_deriv_eq0 [lemma, in mathcomp_fps.fps_deriv]
fps_derivK [lemma, in mathcomp_fps.fps_deriv]
fps_prim [definition, in mathcomp_fps.fps_deriv]
fps_derivX [lemma, in mathcomp_fps.fps_deriv]
fps_deriv_poly [lemma, in mathcomp_fps.fps_deriv]
fps_derivM [lemma, in mathcomp_fps.fps_deriv]
fps_deriv_sum [lemma, in mathcomp_fps.fps_deriv]
fps_derivC [lemma, in mathcomp_fps.fps_deriv]
fps_deriv1 [lemma, in mathcomp_fps.fps_deriv]
fps_deriv0 [lemma, in mathcomp_fps.fps_deriv]
fps_derivZ [lemma, in mathcomp_fps.fps_deriv]
fps_derivB [lemma, in mathcomp_fps.fps_deriv]
fps_derivN [lemma, in mathcomp_fps.fps_deriv]
fps_derivD [lemma, in mathcomp_fps.fps_deriv]
fps_deriv [definition, in mathcomp_fps.fps_deriv]
fps_compV [lemma, in mathcomp_fps.fps_comp]
fps_comp_unit [lemma, in mathcomp_fps.fps_comp]
fps_comp_deriv [lemma, in mathcomp_fps.fps_comp]
fps_comp_deriv_poly [lemma, in mathcomp_fps.fps_comp]
fps_comp_coef_eqf [lemma, in mathcomp_fps.fps_comp]
fps_compM [lemma, in mathcomp_fps.fps_comp]
fps_compX [lemma, in mathcomp_fps.fps_comp]
fps_compC [lemma, in mathcomp_fps.fps_comp]
fps_comp1 [lemma, in mathcomp_fps.fps_comp]
fps_comp0 [lemma, in mathcomp_fps.fps_comp]
fps_compN [lemma, in mathcomp_fps.fps_comp]
fps_compZ [lemma, in mathcomp_fps.fps_comp]
fps_compD [lemma, in mathcomp_fps.fps_comp]
fps_comp [definition, in mathcomp_fps.fps_comp]
fps_quad_ode_uniq [lemma, in mathcomp_fps.fps_ode]
fps_inv_onesubX [lemma, in mathcomp_fps.fps]
fps_onesubX_unit [lemma, in mathcomp_fps.fps]
fps_geom [definition, in mathcomp_fps.fps]
fps_unitE [lemma, in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComUnitAlgebra [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComUnitRing [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_UnitAlgebra [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_UnitRing [definition, in mathcomp_fps.fps]
fps_inv_out [lemma, in mathcomp_fps.fps]
fps_unitP [lemma, in mathcomp_fps.fps]
fps_mulVf [lemma, in mathcomp_fps.fps]
fps_inv [definition, in mathcomp_fps.fps]
fps_unit [definition, in mathcomp_fps.fps]
fps_inv_coefS [lemma, in mathcomp_fps.fps]
fps_inv_coef0 [lemma, in mathcomp_fps.fps]
fps_inv_coef [definition, in mathcomp_fps.fps]
fps_poly_fps__canonical__GRing_RMorphism [definition, in mathcomp_fps.fps]
fps_poly_fps__canonical__Algebra_Additive [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComAlgebra [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_Algebra [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComSemiAlgebra [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_SemiAlgebra [definition, in mathcomp_fps.fps]
fps_scaleAr [lemma, in mathcomp_fps.fps]
fps_fps__canonical__GRing_Lalgebra [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_LSemiAlgebra [definition, in mathcomp_fps.fps]
fps_scaleAl [lemma, in mathcomp_fps.fps]
fps_fps__canonical__GRing_Lmodule [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_LSemiModule [definition, in mathcomp_fps.fps]
fps_scaleDl [lemma, in mathcomp_fps.fps]
fps_scaleDr [lemma, in mathcomp_fps.fps]
fps_scale1f [lemma, in mathcomp_fps.fps]
fps_scaleA [lemma, in mathcomp_fps.fps]
fps_scale [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComNzRing [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComNzSemiRing [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_NzRing [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_NzSemiRing [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComPzRing [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComPzSemiRing [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_PzRing [definition, in mathcomp_fps.fps]
fps_fps__canonical__GRing_PzSemiRing [definition, in mathcomp_fps.fps]
fps_oner_neq0 [lemma, in mathcomp_fps.fps]
fps_mulDl [lemma, in mathcomp_fps.fps]
fps_mul1f [lemma, in mathcomp_fps.fps]
fps_trunc_one [lemma, in mathcomp_fps.fps]
fps_mulC [lemma, in mathcomp_fps.fps]
fps_mulA [lemma, in mathcomp_fps.fps]
fps_trunc [definition, in mathcomp_fps.fps]
fps_mul [definition, in mathcomp_fps.fps]
fps_one [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_Zmodule [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_Nmodule [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_AddUMagma [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_BaseZmodule [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_ChoiceBaseAddUMagma [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_BaseAddUMagma [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_AddSemigroup [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_AddMagma [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_ChoiceBaseAddMagma [definition, in mathcomp_fps.fps]
fps_fps__canonical__Algebra_BaseAddMagma [definition, in mathcomp_fps.fps]
fps_addNf [lemma, in mathcomp_fps.fps]
fps_add0f [lemma, in mathcomp_fps.fps]
fps_addC [lemma, in mathcomp_fps.fps]
fps_addA [lemma, in mathcomp_fps.fps]
fps_opp [definition, in mathcomp_fps.fps]
fps_add [definition, in mathcomp_fps.fps]
fps_zero [definition, in mathcomp_fps.fps]
fps_fps__canonical__choice_Choice [definition, in mathcomp_fps.fps]
fps_fps__canonical__eqtype_Equality [definition, in mathcomp_fps.fps]
fps_trig [library]
fps_ode [library]
fps_egf [library]
fps_deriv [library]
fps_comp [library]
fps_explog [library]
fps_ogf [library]
fwdAss [definition, in mathcomp_eulerian.reflection]
fwd_bwd [lemma, in mathcomp_eulerian.reflection]

G

Geometric [section, in mathcomp_fps.fps]
Geometric.R [variable, in mathcomp_fps.fps]
Geometric.sum_delta [variable, in mathcomp_fps.fps]
GeomPowers [section, in mathcomp_fps.fps_ogf]
GeomPowers.R [variable, in mathcomp_fps.fps_ogf]
geq_minn' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
geq_maxn' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
GRing_ComNzRing_hasMulInverse__to__GRing_NzRing_hasMulInverse [definition, in mathcomp_fps.fps]
GRing_isZmodMorphism__to__Algebra_isNmodMorphism [definition, in mathcomp_fps.fps]
GRing_Lalgebra_isAlgebra__to__GRing_LSemiAlgebra_isSemiAlgebra [definition, in mathcomp_fps.fps]
GRing_Lmodule_isLalgebra__to__GRing_LSemiModule_isLSemiAlgebra [definition, in mathcomp_fps.fps]
GRing_Zmodule_isLmodule__to__GRing_Nmodule_isLSemiModule [definition, in mathcomp_fps.fps]
GRing_Zmodule_isComNzRing__to__GRing_PzSemiRing_isNonZero [definition, in mathcomp_fps.fps]
GRing_Zmodule_isComNzRing__to__GRing_Nmodule_isPzSemiRing [definition, in mathcomp_fps.fps]
GRing_Zmodule_isComNzRing__to__GRing_PzSemiRing_hasCommutativeMul [definition, in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_hasZero [definition, in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_BaseAddUMagma_isAddUMagma [definition, in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_BaseAddMagma_isAddMagma [definition, in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_AddMagma_isAddSemigroup [definition, in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_hasAdd [definition, in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_BaseZmoduleNmodule_isZmodule [definition, in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_hasOpp [definition, in mathcomp_fps.fps]

H

has_left_child_is_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_last_fuel [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_last [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_t_last_valid [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_psi [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
has_left_child_order_iso [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
has_left_child_of_shape [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
has_transition_omega_seq [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition_cons2 [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition_cons [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
has_left_child_t_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_0 [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_gt [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_lt [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t [definition, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_psi_ex [definition, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_iota [lemma, in mathcomp_eulerian.psi_cdindex_witness]
has_left_child_true [definition, in mathcomp_eulerian.psi_descent_v2]
has_left_child_false [definition, in mathcomp_eulerian.psi_descent_v2]
has_left_child_cons [lemma, in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel_monotone [lemma, in mathcomp_eulerian.psi_descent_v2]
has_left_child_0 [lemma, in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel_0 [lemma, in mathcomp_eulerian.psi_descent_v2]
has_left_child [definition, in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel [definition, in mathcomp_eulerian.psi_descent_v2]
HB_unnamed_mixin_45 [definition, in mathcomp_fps.fps]
HB_unnamed_factory_43 [definition, in mathcomp_fps.fps]
HB_unnamed_factory_41 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_40 [definition, in mathcomp_fps.fps]
HB_unnamed_factory_38 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_37 [definition, in mathcomp_fps.fps]
HB_unnamed_factory_35 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_34 [definition, in mathcomp_fps.fps]
HB_unnamed_factory_32 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_31 [definition, in mathcomp_fps.fps]
HB_unnamed_factory_29 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_28 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_27 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_26 [definition, in mathcomp_fps.fps]
HB_unnamed_factory_22 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_21 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_20 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_19 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_18 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_17 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_16 [definition, in mathcomp_fps.fps]
HB_unnamed_mixin_15 [definition, in mathcomp_fps.fps]
HB_unnamed_factory_7 [definition, in mathcomp_fps.fps]
HB_unnamed_factory_5 [definition, in mathcomp_fps.fps]
hb_instance_4.R [variable, in mathcomp_fps.fps]
hb_instance_4.hb_instance_4 [section, in mathcomp_fps.fps]
HB_unnamed_factory_2 [definition, in mathcomp_fps.fps]
hb_instance_1.R [variable, in mathcomp_fps.fps]
hb_instance_1.hb_instance_1 [section, in mathcomp_fps.fps]
head_max_is_descent [lemma, in mathcomp_eulerian.psi_descent_thms]
head_min_not_descent [lemma, in mathcomp_eulerian.psi_descent_thms]
head_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]
hlc_core_1 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
hlc_core_not1 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
hlc_bridge_right [lemma, in mathcomp_eulerian.psi_descent_v2]
hlc_bridge_root [lemma, in mathcomp_eulerian.psi_descent_v2]
hlc_bridge_left [lemma, in mathcomp_eulerian.psi_descent_v2]
H1 [section, in mathcomp_eulerian.cycles_rec]
H1.n [variable, in mathcomp_eulerian.cycles_rec]
H1.s [variable, in mathcomp_eulerian.cycles_rec]

I

if_sum_const [lemma, in mathcomp_eulerian.qeul_rec]
ImageLeft [section, in mathcomp_eulerian.reflection]
ImageLeft.j [variable, in mathcomp_eulerian.reflection]
ImageLeft.n [variable, in mathcomp_eulerian.reflection]
ImageLeft.t [variable, in mathcomp_eulerian.reflection]
ImageRight [section, in mathcomp_eulerian.reflection]
ImageRight.j [variable, in mathcomp_eulerian.reflection]
ImageRight.n [variable, in mathcomp_eulerian.reflection]
ImageRight.t [variable, in mathcomp_eulerian.reflection]
image_right_eq_compl [lemma, in mathcomp_eulerian.reflection]
image_left_card_plus_right [lemma, in mathcomp_eulerian.reflection]
image_left_right_cover [lemma, in mathcomp_eulerian.reflection]
image_left_right_disjoint [lemma, in mathcomp_eulerian.reflection]
image_right [definition, in mathcomp_eulerian.reflection]
image_left_witness_pos [lemma, in mathcomp_eulerian.reflection]
image_left [definition, in mathcomp_eulerian.reflection]
imset_rev_ord_compl [lemma, in mathcomp_eulerian.beta]
imset_rev_ord_inv [lemma, in mathcomp_eulerian.beta]
imset_lift_eq [lemma, in mathcomp_eulerian.reflection]
index_rcons_eq_size [lemma, in mathcomp_eulerian.psi_cdindex_core]
index_lt_sorted [lemma, in mathcomp_eulerian.perm_seq_bridge]
index_map_inj_in [lemma, in mathcomp_eulerian.psi_comm]
InnerReindexBij [section, in mathcomp_eulerian.reflection]
InnerReindexBij.Hj [variable, in mathcomp_eulerian.reflection]
InnerReindexBij.Hjn [variable, in mathcomp_eulerian.reflection]
InnerReindexBij.HL [variable, in mathcomp_eulerian.reflection]
InnerReindexBij.HxLcan [variable, in mathcomp_eulerian.reflection]
InnerReindexBij.HxRcan [variable, in mathcomp_eulerian.reflection]
InnerReindexBij.j [variable, in mathcomp_eulerian.reflection]
InnerReindexBij.L [variable, in mathcomp_eulerian.reflection]
InnerReindexBij.n [variable, in mathcomp_eulerian.reflection]
InnerReindexBij.xLcan [variable, in mathcomp_eulerian.reflection]
InnerReindexBij.xRcan [variable, in mathcomp_eulerian.reflection]
InsertAfter [section, in mathcomp_eulerian.stirling_fiber]
InsertAfter.n [variable, in mathcomp_eulerian.stirling_fiber]
InsertExtractBij [section, in mathcomp_eulerian.eulerian]
InsertExtractBij.n [variable, in mathcomp_eulerian.eulerian]
InsertMax [section, in mathcomp_eulerian.eulerian]
InsertMax.n [variable, in mathcomp_eulerian.eulerian]
InsertMax.p [variable, in mathcomp_eulerian.eulerian]
InsertMax.t [variable, in mathcomp_eulerian.eulerian]
insert_max_perm_bij [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm_fiber [lemma, in mathcomp_eulerian.eulerian]
insert_extract_max [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm_lift [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm_at_p [lemma, in mathcomp_eulerian.eulerian]
insert_max_permE [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm [definition, in mathcomp_eulerian.eulerian]
insert_max_fun_inj [lemma, in mathcomp_eulerian.eulerian]
insert_max_fun_lift [lemma, in mathcomp_eulerian.eulerian]
insert_max_fun_p [lemma, in mathcomp_eulerian.eulerian]
insert_max_fun [definition, in mathcomp_eulerian.eulerian]
insert_after_surj [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_inj_pair [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_decomp [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_ord_max_neq [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_other [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_j0 [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_ord_max [lemma, in mathcomp_eulerian.stirling_fiber]
insert_afterE [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after [definition, in mathcomp_eulerian.stirling_fiber]
insert_after_fun_inj [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_fun [definition, in mathcomp_eulerian.stirling_fiber]
interior_is_turn_inj [lemma, in mathcomp_eulerian.altsub]
interior_set_is_alt [lemma, in mathcomp_eulerian.reflection]
interior_descent_set_eq [lemma, in mathcomp_eulerian.reflection]
internal_vertices_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
internal_vertices [definition, in mathcomp_eulerian.psi_cdindex_defs]
InterTurn [section, in mathcomp_eulerian.altsub]
InterTurn.n [variable, in mathcomp_eulerian.altsub]
inter_turn_monotone_strict [lemma, in mathcomp_eulerian.altsub]
inter_turn_monotone [lemma, in mathcomp_eulerian.altsub]
inv [definition, in mathcomp_eulerian.inversions]
Inversions [section, in mathcomp_eulerian.inversions]
inversions [library]
Inversions.n [variable, in mathcomp_eulerian.inversions]
InvInsertMax [section, in mathcomp_eulerian.qfact]
InvInsertMax.n [variable, in mathcomp_eulerian.qfact]
InvInsertMax.p [variable, in mathcomp_eulerian.qfact]
InvInsertMax.t [variable, in mathcomp_eulerian.qfact]
InvMajBoundsRev [section, in mathcomp_eulerian.inversions]
InvMajBoundsRev.n [variable, in mathcomp_eulerian.inversions]
inv_rev_perm [lemma, in mathcomp_eulerian.inversions]
inv_rev_perm_eq_coinv [lemma, in mathcomp_eulerian.inversions]
inv_le [lemma, in mathcomp_eulerian.inversions]
inv_double_sum [lemma, in mathcomp_eulerian.inversions]
inv_id [lemma, in mathcomp_eulerian.inversions]
inv_set [definition, in mathcomp_eulerian.inversions]
inv_q_fact [lemma, in mathcomp_eulerian.qfact]
inv_insert_max [lemma, in mathcomp_eulerian.qfact]
inv_via_sum [lemma, in mathcomp_eulerian.qfact]
inv_maj_equidistr [lemma, in mathcomp_eulerian.foata]
inv_eq_inv_seq [lemma, in mathcomp_eulerian.foata]
inv_seq_cons_eq_rcons_shift [lemma, in mathcomp_eulerian.foata]
inv_seq_flatten_swap_eq [lemma, in mathcomp_eulerian.foata]
inv_seq_cat [lemma, in mathcomp_eulerian.foata]
inv_seq_rcons [lemma, in mathcomp_eulerian.foata]
inv_seq [definition, in mathcomp_eulerian.foata]
inv_prefE [lemma, in mathcomp_fps.fps]
inv_pref [definition, in mathcomp_fps.fps]
in_internal_vertices [lemma, in mathcomp_eulerian.psi_cdindex_support]
is_internal_lt [lemma, in mathcomp_eulerian.psi_cdindex_core]
is_internal_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
is_internal [definition, in mathcomp_eulerian.psi_cdindex_defs]
is_descent_compl [lemma, in mathcomp_eulerian.beta_swap]
is_alt_pick_turn_witness [lemma, in mathcomp_eulerian.altsub]
is_alt_from_sign [lemma, in mathcomp_eulerian.altsub]
is_alt_flip_count [lemma, in mathcomp_eulerian.altsub]
is_alt_bool [definition, in mathcomp_eulerian.altsub]
is_alt_bool_aux [definition, in mathcomp_eulerian.altsub]
is_alt_three [lemma, in mathcomp_eulerian.altsub]
is_alt_cons2 [lemma, in mathcomp_eulerian.altsub]
is_alt [definition, in mathcomp_eulerian.altsub]
is_turn [definition, in mathcomp_eulerian.altsub]
is_internal_t_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
is_internal_t [definition, in mathcomp_eulerian.psi_cdindex_tree]
is_D_letter [definition, in mathcomp_eulerian.psi_cdindex_witness]
is_descent_seq_ex [definition, in mathcomp_eulerian.psi_descent_v2]
is_inv [definition, in mathcomp_eulerian.inversions]
is_descent_perm_seq [lemma, in mathcomp_eulerian.perm_seq_basics]
is_descent_seq [definition, in mathcomp_eulerian.perm_seq_basics]
is_inv_lift_p [lemma, in mathcomp_eulerian.qfact]
is_inv_lift_pair [lemma, in mathcomp_eulerian.qfact]
is_desc_seq [definition, in mathcomp_eulerian.foata]
is_descent_rev [lemma, in mathcomp_eulerian.descent]
is_descent [definition, in mathcomp_eulerian.descent]
is_descent_perm_right [lemma, in mathcomp_eulerian.reflection]
is_descent_perm_left [lemma, in mathcomp_eulerian.reflection]

J

j_plus_lt_n [lemma, in mathcomp_eulerian.reflection]

L

last_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
Leaf [constructor, in mathcomp_eulerian.mmtree]
left_ok_self [lemma, in mathcomp_eulerian.beta_omega]
left_ok [definition, in mathcomp_eulerian.beta_omega]
leqj [definition, in mathcomp_eulerian.reflection]
leqj_pred_n [lemma, in mathcomp_eulerian.reflection]
leqj_n1 [definition, in mathcomp_eulerian.reflection]
leq_seqb_anti [lemma, in mathcomp_eulerian.psi_cdindex_core]
leq_seqb_trans [lemma, in mathcomp_eulerian.psi_cdindex_core]
leq_seqb_total [lemma, in mathcomp_eulerian.psi_cdindex_core]
leq_seqb [definition, in mathcomp_eulerian.psi_cdindex_defs]
leq_maxn' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
leq_lift [lemma, in mathcomp_eulerian.ordinal_reindex]
LiftOrd [section, in mathcomp_eulerian.ordinal_reindex]
LiftOrd.n [variable, in mathcomp_eulerian.ordinal_reindex]
LiftPerm [section, in mathcomp_eulerian.perm_compress]
LiftPerm.k [variable, in mathcomp_eulerian.perm_compress]
LiftPerm.n [variable, in mathcomp_eulerian.perm_compress]
LiftPerm.t [variable, in mathcomp_eulerian.perm_compress]
lift_perm_drop_perm [lemma, in mathcomp_eulerian.perm_compress]
lift_perm_lift [lemma, in mathcomp_eulerian.perm_compress]
lift_perm_ord_max [lemma, in mathcomp_eulerian.perm_compress]
lift_permE [lemma, in mathcomp_eulerian.perm_compress]
lift_perm [definition, in mathcomp_eulerian.perm_compress]
lift_fun_inj [lemma, in mathcomp_eulerian.perm_compress]
lift_fun_lift [lemma, in mathcomp_eulerian.perm_compress]
lift_fun_ord_max [lemma, in mathcomp_eulerian.perm_compress]
lift_fun [definition, in mathcomp_eulerian.perm_compress]
lift_drop_permE [lemma, in mathcomp_eulerian.perm_compress]
lift_perm_id_iter_lift [lemma, in mathcomp_eulerian.cycles_rec]
lift_perm_id_iter [lemma, in mathcomp_eulerian.cycles_rec]
LowerBound [section, in mathcomp_eulerian.altsub]
LowerBound.n [variable, in mathcomp_eulerian.altsub]
LR_pred_is_endpoint_ex3 [definition, in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_ex2 [definition, in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_ex [definition, in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint [lemma, in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_t [lemma, in mathcomp_eulerian.psi_cdindex_tree]
ltn_lift [lemma, in mathcomp_eulerian.ordinal_reindex]

M

maj [definition, in mathcomp_eulerian.inversions]
MajorIndex [section, in mathcomp_eulerian.inversions]
MajorIndex.n [variable, in mathcomp_eulerian.inversions]
maj_rev_perm [lemma, in mathcomp_eulerian.inversions]
maj_le [lemma, in mathcomp_eulerian.inversions]
maj_id [lemma, in mathcomp_eulerian.inversions]
maj_insert_max_interior [lemma, in mathcomp_eulerian.qeul_rec]
maj_insert_max_ord_max [lemma, in mathcomp_eulerian.qeul_rec]
maj_insert_max_ord0 [lemma, in mathcomp_eulerian.qeul_rec]
maj_q_fact [lemma, in mathcomp_eulerian.qfact]
maj_eq_maj_seq [lemma, in mathcomp_eulerian.foata]
maj_seq_rcons [lemma, in mathcomp_eulerian.foata]
maj_seq [definition, in mathcomp_eulerian.foata]
map_mod_iota_rot [lemma, in mathcomp_eulerian.psi_core]
map_nth_iota_sorted [lemma, in mathcomp_eulerian.psi_core]
MaxAlternation [section, in mathcomp_eulerian.altsub]
MaxAlternation.n [variable, in mathcomp_eulerian.altsub]
max_pos_core_gt0 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
max_pos_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
max_eq_nth_sort_last [lemma, in mathcomp_eulerian.psi_core]
max_val_drop [lemma, in mathcomp_eulerian.psi_core]
max_val_perm_eq [lemma, in mathcomp_eulerian.psi_core]
max_pos_lt [lemma, in mathcomp_eulerian.psi_core]
max_in [lemma, in mathcomp_eulerian.psi_core]
max_pos [definition, in mathcomp_eulerian.psi_core]
mem_omega_set [lemma, in mathcomp_eulerian.beta_omega]
mem_alt_desc_set [lemma, in mathcomp_eulerian.beta_swap]
mem_pos_seq [lemma, in mathcomp_eulerian.altsub]
mem_slot_iv [lemma, in mathcomp_eulerian.altsub]
mem_omega_seq [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
mem_filter_iota_nth [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
mem_set_to_seq_ord [lemma, in mathcomp_eulerian.beta_bridge]
mem_set_to_seq_iff [lemma, in mathcomp_eulerian.beta_bridge]
mem_set_to_seq [lemma, in mathcomp_eulerian.beta_bridge]
mem_descent_set [lemma, in mathcomp_eulerian.descent]
mem_image_right [lemma, in mathcomp_eulerian.reflection]
mem_image_left [lemma, in mathcomp_eulerian.reflection]
min_pos_lt [lemma, in mathcomp_eulerian.mmtree]
min_in [lemma, in mathcomp_eulerian.mmtree]
min_pos [definition, in mathcomp_eulerian.mmtree]
min_pos_core [lemma, in mathcomp_eulerian.psi_cdindex_witness]
min_pos_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
min_eq_nth_sort_0 [lemma, in mathcomp_eulerian.psi_core]
min_val_drop [lemma, in mathcomp_eulerian.psi_core]
min_val_perm_eq [lemma, in mathcomp_eulerian.psi_core]
mmtree [inductive, in mathcomp_eulerian.mmtree]
MMTree [section, in mathcomp_eulerian.mmtree]
mmtree [library]
mmtree_shape_psi [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_decompose [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_order_iso [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_cons [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_nil [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_fuel_monotone [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape [definition, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_fuel [definition, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_of_seqK [lemma, in mathcomp_eulerian.mmtree]
mmtree_of_seq_fuel_correct [lemma, in mathcomp_eulerian.mmtree]
mmtree_of_seq [definition, in mathcomp_eulerian.mmtree]
mmtree_of_seq_fuel [definition, in mathcomp_eulerian.mmtree]
mmtree_to_seq [definition, in mathcomp_eulerian.mmtree]
mmtree_sind [definition, in mathcomp_eulerian.mmtree]
mmtree_rec [definition, in mathcomp_eulerian.mmtree]
mmtree_ind [definition, in mathcomp_eulerian.mmtree]
mmtree_rect [definition, in mathcomp_eulerian.mmtree]
mmtree_of_seq_mmK [lemma, in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm_fuel_correct [lemma, in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm [definition, in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm_fuel [definition, in mathcomp_eulerian.psi_core]
mm_pos_rcons_lt [lemma, in mathcomp_eulerian.psi_cdindex_core]
mm_pos_lt_pred [lemma, in mathcomp_eulerian.psi_cdindex_support]
mm_pos_witness [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_core [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_min_first [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_drop_mm [lemma, in mathcomp_eulerian.psi_core]
mm_pos_order_iso [lemma, in mathcomp_eulerian.psi_core]
mm_pos_psi_eq [lemma, in mathcomp_eulerian.psi_core]
mm_pos_char [lemma, in mathcomp_eulerian.psi_core]
mm_pos_lt [lemma, in mathcomp_eulerian.psi_core]
mm_pos [definition, in mathcomp_eulerian.psi_core]
mono_inj_in [lemma, in mathcomp_eulerian.psi_comm]

N

natf_neq0_char0 [lemma, in mathcomp_fps.fps_deriv]
natSf_neq0 [lemma, in mathcomp_fps.fps_deriv]
natU_polyrat [lemma, in mathcomp_eulerian.stirling_egf]
nat_of_andb [lemma, in mathcomp_eulerian.reflection]
neg_add_neg [lemma, in mathcomp_eulerian.altsub]
nil_in_powerset_internal [lemma, in mathcomp_eulerian.perm_seq_bridge]
Node [constructor, in mathcomp_eulerian.mmtree]
notin_take_mm [lemma, in mathcomp_eulerian.psi_core]
not_set_is_alt_omega_not_full [lemma, in mathcomp_eulerian.beta_swap]
not_set_is_alt_n_ge2 [lemma, in mathcomp_eulerian.beta_swap]
not_is_descentE [lemma, in mathcomp_eulerian.altsub]
no_inner_in_pos_seq [lemma, in mathcomp_eulerian.altsub]
nth_char_mono [lemma, in mathcomp_eulerian.psi_cdindex_core]
nth_window_at [lemma, in mathcomp_eulerian.psi_descent_thms]
nth_descent_to_bvec [lemma, in mathcomp_eulerian.perm_seq_basics]
nth_perm_to_seq [lemma, in mathcomp_eulerian.perm_seq_basics]
nth_w_mm_pos [lemma, in mathcomp_eulerian.psi_core]
nth_psi_inside [lemma, in mathcomp_eulerian.psi_core]
nth_psi_right [lemma, in mathcomp_eulerian.psi_core]
nth_psi_left [lemma, in mathcomp_eulerian.psi_core]
nth_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]

O

omega_set [definition, in mathcomp_eulerian.beta_omega]
omega_set_alt_full [lemma, in mathcomp_eulerian.beta_swap]
omega_proper_beta_lt [lemma, in mathcomp_eulerian.perm_seq_bridge]
omega_seq_subset_bounded [lemma, in mathcomp_eulerian.perm_seq_bridge]
omega_set_seq_bridge_bounded [lemma, in mathcomp_eulerian.perm_seq_bridge]
omega_seq_mem_eq [lemma, in mathcomp_eulerian.perm_seq_bridge]
omega_monotone_class_count [lemma, in mathcomp_eulerian.psi_cdindex_witness]
omega_seq [definition, in mathcomp_eulerian.psi_cdindex_witness]
omega_set_seq_local_bridge [lemma, in mathcomp_eulerian.beta_bridge]
omega_seq_local [definition, in mathcomp_eulerian.beta_bridge]
onepX_mul_altgeom [lemma, in mathcomp_fps.fps_explog]
onepX_unit [lemma, in mathcomp_fps.fps_explog]
onesubXn_mul_geomn [lemma, in mathcomp_fps.fps_ogf]
onesubX_pow_t_ode1 [lemma, in mathcomp_eulerian.stirling_egf]
onesubX_pow_t [definition, in mathcomp_eulerian.stirling_egf]
onesubX_mul_geom [lemma, in mathcomp_fps.fps]
order_iso_drop [lemma, in mathcomp_eulerian.psi_core]
order_iso_take [lemma, in mathcomp_eulerian.psi_core]
ordinal_reindex [library]
ord_max_notin_turn_image [lemma, in mathcomp_eulerian.altsub]
ord0_neq_ord_max [lemma, in mathcomp_eulerian.altsub]
ord0_notin_turn_image [lemma, in mathcomp_eulerian.altsub]

P

path_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
path_leq_last' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
PermOfLeft [section, in mathcomp_eulerian.reflection]
PermOfLeft.j [variable, in mathcomp_eulerian.reflection]
PermOfLeft.n [variable, in mathcomp_eulerian.reflection]
PermOfLeft.t [variable, in mathcomp_eulerian.reflection]
PermOfRight [section, in mathcomp_eulerian.reflection]
PermOfRight.j [variable, in mathcomp_eulerian.reflection]
PermOfRight.n [variable, in mathcomp_eulerian.reflection]
PermOfRight.t [variable, in mathcomp_eulerian.reflection]
perm_eq_from_subset [lemma, in mathcomp_eulerian.psi_cdindex_support]
perm_eq_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_defs]
perm_seq [definition, in mathcomp_eulerian.altsub]
perm_to_seq_class_map [lemma, in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_seq_to_perm [lemma, in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_bnd [lemma, in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_inj [lemma, in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_uniq [lemma, in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_size [lemma, in mathcomp_eulerian.perm_seq_basics]
perm_to_seq [definition, in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_foata_perm [lemma, in mathcomp_eulerian.foata]
perm_eq_flatten_map_pred [lemma, in mathcomp_eulerian.foata]
perm_eq_flatten_map_cyc [lemma, in mathcomp_eulerian.foata]
perm_right_lt_iff [lemma, in mathcomp_eulerian.reflection]
perm_left_lt_iff [lemma, in mathcomp_eulerian.reflection]
perm_right_witness_indep [lemma, in mathcomp_eulerian.reflection]
perm_rightE [lemma, in mathcomp_eulerian.reflection]
perm_right [definition, in mathcomp_eulerian.reflection]
perm_right_fun_inj [lemma, in mathcomp_eulerian.reflection]
perm_right_fun [definition, in mathcomp_eulerian.reflection]
perm_left_witness_indep [lemma, in mathcomp_eulerian.reflection]
perm_leftE [lemma, in mathcomp_eulerian.reflection]
perm_left [definition, in mathcomp_eulerian.reflection]
perm_left_fun_inj [lemma, in mathcomp_eulerian.reflection]
perm_left_fun [definition, in mathcomp_eulerian.reflection]
perm_seq_bridge [library]
perm_compress [library]
perm_seq_basics [library]
PhaseA [section, in mathcomp_eulerian.reflection]
PhaseARight [section, in mathcomp_eulerian.reflection]
PhaseARight.Hjn [variable, in mathcomp_eulerian.reflection]
PhaseARight.j [variable, in mathcomp_eulerian.reflection]
PhaseARight.n [variable, in mathcomp_eulerian.reflection]
PhaseARight.t [variable, in mathcomp_eulerian.reflection]
PhaseA.Hk [variable, in mathcomp_eulerian.reflection]
PhaseA.Hkn [variable, in mathcomp_eulerian.reflection]
PhaseA.j [variable, in mathcomp_eulerian.reflection]
PhaseA.k [variable, in mathcomp_eulerian.reflection]
PhaseA.n [variable, in mathcomp_eulerian.reflection]
PhaseA.t [variable, in mathcomp_eulerian.reflection]
PhaseB [section, in mathcomp_eulerian.reflection]
PhaseB.HL [variable, in mathcomp_eulerian.reflection]
PhaseB.j [variable, in mathcomp_eulerian.reflection]
PhaseB.L [variable, in mathcomp_eulerian.reflection]
PhaseB.n [variable, in mathcomp_eulerian.reflection]
PhaseB.sL [variable, in mathcomp_eulerian.reflection]
PhaseB.sR [variable, in mathcomp_eulerian.reflection]
phi_w_as_map [lemma, in mathcomp_eulerian.psi_cdindex_core]
phi_w_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
phi_w_support_general [lemma, in mathcomp_eulerian.psi_cdindex_support]
phi_w_decomp_mm [lemma, in mathcomp_eulerian.psi_cdindex_support]
phi_w_cons_mm0 [lemma, in mathcomp_eulerian.psi_cdindex_support]
phi_w [definition, in mathcomp_eulerian.psi_cdindex_defs]
phi_w_support_ex1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
phi'_w [definition, in mathcomp_eulerian.psi_cdindex_defs]
PickSeqFull [section, in mathcomp_eulerian.altsub]
PickSeqFull.n [variable, in mathcomp_eulerian.altsub]
pick_seq_subseq_perm_seq [lemma, in mathcomp_eulerian.altsub]
pick_seq_pos_seq [lemma, in mathcomp_eulerian.altsub]
pick_seq_setT [lemma, in mathcomp_eulerian.altsub]
pick_seq [definition, in mathcomp_eulerian.altsub]
PolyFps [section, in mathcomp_fps.fps]
PolyFps.R [variable, in mathcomp_fps.fps]
poly_fpsC [lemma, in mathcomp_fps.fps]
poly_fps_is_monoid_morphism [lemma, in mathcomp_fps.fps]
poly_fps_is_zmod_morphism [lemma, in mathcomp_fps.fps]
poly_fps_inj [lemma, in mathcomp_fps.fps]
poly_fps [definition, in mathcomp_fps.fps]
porbits_lift_perm_id [lemma, in mathcomp_eulerian.cycles_rec]
porbit_id_singleton [lemma, in mathcomp_eulerian.cycles]
porbit_lift_perm_id_lift [lemma, in mathcomp_eulerian.cycles_rec]
porbit_lift_perm_id_max [lemma, in mathcomp_eulerian.cycles_rec]
post_window_extremum_ex [definition, in mathcomp_eulerian.psi_descent_v2]
post_window_extremum [lemma, in mathcomp_eulerian.psi_descent_v2]
pos_seq_last_val [lemma, in mathcomp_eulerian.altsub]
pos_seq_nth0 [lemma, in mathcomp_eulerian.altsub]
pos_seq_val_lt_inv [lemma, in mathcomp_eulerian.altsub]
pos_seq_val_lt [lemma, in mathcomp_eulerian.altsub]
pos_seq_strict_sorted [lemma, in mathcomp_eulerian.altsub]
pos_seq_uniq [lemma, in mathcomp_eulerian.altsub]
pos_seq [definition, in mathcomp_eulerian.altsub]
powerset_internal [definition, in mathcomp_eulerian.psi_cdindex_defs]
powerset_internal_apply_psis [lemma, in mathcomp_eulerian.perm_seq_bridge]
pow_ogf [definition, in mathcomp_eulerian.stanley_ogf]
pred_sub_add [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_window_extremum_R [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_window_gt_min_ex [definition, in mathcomp_eulerian.psi_descent_v2]
pre_window_gt_min_when_max_head [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_window_lt_max_when_min_head [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_win_gt_min_eq [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_win_lt_max_eq [lemma, in mathcomp_eulerian.psi_descent_v2]
psi [definition, in mathcomp_eulerian.psi_core]
psi_apply_psis_comm [lemma, in mathcomp_eulerian.perm_seq_bridge]
psi_comm_nontrivial [definition, in mathcomp_eulerian.psi_comm]
psi_comm_ex [definition, in mathcomp_eulerian.psi_comm]
psi_comm [lemma, in mathcomp_eulerian.psi_comm]
psi_comm_nested_ex [definition, in mathcomp_eulerian.psi_comm]
psi_comm_nested [lemma, in mathcomp_eulerian.psi_comm]
psi_map_comm [lemma, in mathcomp_eulerian.psi_comm]
psi_comm_disjoint_ex [definition, in mathcomp_eulerian.psi_comm]
psi_comm_disjoint [lemma, in mathcomp_eulerian.psi_comm]
psi_comm_disjoint_lr [lemma, in mathcomp_eulerian.psi_comm]
psi_0_eq [lemma, in mathcomp_eulerian.psi_core]
psi_involutive [lemma, in mathcomp_eulerian.psi_core]
psi_id_trivial [lemma, in mathcomp_eulerian.psi_core]
psi_id_oor [lemma, in mathcomp_eulerian.psi_core]
psi_involutive_ex [definition, in mathcomp_eulerian.psi_core]
psi_nontrivial [definition, in mathcomp_eulerian.psi_core]
psi_perm_eq [lemma, in mathcomp_eulerian.psi_core]
psi_descent_v2 [library]
psi_cdindex_support [library]
psi_comm [library]
psi_cdindex_tree_shape [library]
psi_cdindex_tree_hlc [library]
psi_cdindex_tree [library]
psi_cdindex_defs [library]
psi_descent [library]
psi_core [library]
psi_descent_thms [library]
psi_cdindex_witness [library]
psi_cdindex_core [library]
psi_cdindex_support_defs [library]

Q

qbin [definition, in mathcomp_eulerian.qbin]
qbin [library]
qbinS [lemma, in mathcomp_eulerian.qbin]
qbin_absorbC [lemma, in mathcomp_eulerian.qworpitzky]
qbin_n1 [lemma, in mathcomp_eulerian.qworpitzky]
qbin_horner1 [lemma, in mathcomp_eulerian.qbin]
qbin_nn [lemma, in mathcomp_eulerian.qbin]
qbin_small [lemma, in mathcomp_eulerian.qbin]
qbin_0S [lemma, in mathcomp_eulerian.qbin]
qbin_n0 [lemma, in mathcomp_eulerian.qbin]
qeul [library]
qeul_rec [library]
qfact [library]
qpow [abbreviation, in mathcomp_eulerian.qeul]
qworpitzky [library]
q_eul_pol_q1 [lemma, in mathcomp_eulerian.qeul]
q_eul_pol_t1 [lemma, in mathcomp_eulerian.qeul]
q_eul_pol [definition, in mathcomp_eulerian.qeul]
q_worpitzky [lemma, in mathcomp_eulerian.qworpitzky]
q_bin_step [lemma, in mathcomp_eulerian.qworpitzky]
q_intD [lemma, in mathcomp_eulerian.qworpitzky]
q_eulerian_rec [lemma, in mathcomp_eulerian.qeul_rec]
q_intS [lemma, in mathcomp_eulerian.qeul_rec]
q_eulerian_out_of_range [lemma, in mathcomp_eulerian.qeul_rec]
q_eulerian_n_0 [lemma, in mathcomp_eulerian.qeul_rec]
q_eulerian [definition, in mathcomp_eulerian.qeul_rec]
q_fact [definition, in mathcomp_eulerian.qfact]
q_int [definition, in mathcomp_eulerian.qfact]
q_pow_ogf [definition, in mathcomp_eulerian.carlitz]
q_stairE [lemma, in mathcomp_eulerian.carlitz]
q_onesub_prod_unit [lemma, in mathcomp_eulerian.carlitz]
q_staircase [lemma, in mathcomp_eulerian.carlitz]
q_stair_step [lemma, in mathcomp_eulerian.carlitz]
q_stair0 [lemma, in mathcomp_eulerian.carlitz]
q_stair [definition, in mathcomp_eulerian.carlitz]
q_onesub_prod [definition, in mathcomp_eulerian.carlitz]
q1_subst [definition, in mathcomp_eulerian.qeul]

R

rank_shift_interior_order_ex [definition, in mathcomp_eulerian.psi_descent_v2]
rank_shift_psi_comm [lemma, in mathcomp_eulerian.psi_comm]
rank_shift_map_comm [lemma, in mathcomp_eulerian.psi_comm]
rank_shift_preserves_interior_order [lemma, in mathcomp_eulerian.psi_comm]
rank_shift_head_max_to_min [lemma, in mathcomp_eulerian.psi_core]
rank_shift_head_min_to_max [lemma, in mathcomp_eulerian.psi_core]
rank_shift_seq_involutive [lemma, in mathcomp_eulerian.psi_core]
rank_shift_seqE [lemma, in mathcomp_eulerian.psi_core]
rank_shift_perm_eq [lemma, in mathcomp_eulerian.psi_core]
rank_shift_seq [definition, in mathcomp_eulerian.psi_core]
rank_left [definition, in mathcomp_eulerian.reflection]
rat_char0 [lemma, in mathcomp_eulerian.stanley_egf]
reflection [library]
rev_perm_involutive [lemma, in mathcomp_eulerian.eulerian]
rev_perm_inj [lemma, in mathcomp_eulerian.eulerian]
rev_ord_lt [lemma, in mathcomp_eulerian.inversions]
rev_permE [lemma, in mathcomp_eulerian.descent]
rev_perm [definition, in mathcomp_eulerian.descent]
rev_perm_ordE [lemma, in mathcomp_eulerian.descent]
rev_perm_ord [definition, in mathcomp_eulerian.descent]
right_ok_self [lemma, in mathcomp_eulerian.beta_omega]
right_ok [definition, in mathcomp_eulerian.beta_omega]
rs_head_min_no_descent [lemma, in mathcomp_eulerian.psi_descent_thms]
rs_head_max_descent [lemma, in mathcomp_eulerian.psi_descent_thms]

S

secf [definition, in mathcomp_fps.fps_trig]
secf_deriv [lemma, in mathcomp_fps.fps_trig]
secf0 [lemma, in mathcomp_fps.fps_trig]
sectan_ode [lemma, in mathcomp_fps.fps_trig]
sectan0 [lemma, in mathcomp_fps.fps_trig]
sec2f [lemma, in mathcomp_fps.fps_trig]
SeqToPerm [section, in mathcomp_eulerian.perm_seq_basics]
SeqToPerm.Hbnd [variable, in mathcomp_eulerian.perm_seq_basics]
SeqToPerm.Hsz [variable, in mathcomp_eulerian.perm_seq_basics]
SeqToPerm.Huniq [variable, in mathcomp_eulerian.perm_seq_basics]
SeqToPerm.n [variable, in mathcomp_eulerian.perm_seq_basics]
SeqToPerm.w [variable, in mathcomp_eulerian.perm_seq_basics]
seq_cat_right_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
seq_cat_left_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
seq_to_perm [definition, in mathcomp_eulerian.perm_seq_basics]
seq_to_fun_inj [lemma, in mathcomp_eulerian.perm_seq_basics]
seq_to_fun [definition, in mathcomp_eulerian.perm_seq_basics]
seq_nth_bound [lemma, in mathcomp_eulerian.perm_seq_basics]
setU1_imset_lift_eq [lemma, in mathcomp_eulerian.reflection]
set_is_alt_classify [lemma, in mathcomp_eulerian.beta_swap]
set_not_altP [lemma, in mathcomp_eulerian.beta_swap]
set_is_alt [definition, in mathcomp_eulerian.beta_swap]
set_to_seq [definition, in mathcomp_eulerian.beta_bridge]
set_is_alt_indicator [lemma, in mathcomp_eulerian.reflection]
shift_preserves_ltn [lemma, in mathcomp_eulerian.psi_comm]
sigma [abbreviation, in mathcomp_eulerian.stirling_fiber]
SignPerm [section, in mathcomp_eulerian.altsub]
SignPerm.n [variable, in mathcomp_eulerian.altsub]
sign_seq_alt_of_triple_flip [lemma, in mathcomp_eulerian.altsub]
sign_flip_at_turn [lemma, in mathcomp_eulerian.altsub]
sign_seq_is_alt [lemma, in mathcomp_eulerian.altsub]
sign_seq_perm_seq [lemma, in mathcomp_eulerian.altsub]
sign_seq [definition, in mathcomp_eulerian.altsub]
sinf [definition, in mathcomp_fps.fps_trig]
sinf_deriv [lemma, in mathcomp_fps.fps_trig]
sinf0 [lemma, in mathcomp_fps.fps_trig]
sin2cos2 [lemma, in mathcomp_fps.fps_trig]
size_expand_cde_phi_w [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_expand_cde [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_powerset_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_powerset_of [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_char_mono [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_window_at [lemma, in mathcomp_eulerian.psi_descent_thms]
size_mmtree_shape [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
size_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_defs]
size_pos_seq [lemma, in mathcomp_eulerian.altsub]
size_take_drop_skip [lemma, in mathcomp_eulerian.altsub]
size_sign_seq_perm [lemma, in mathcomp_eulerian.altsub]
size_sign_seq [lemma, in mathcomp_eulerian.altsub]
size_perm_seq [lemma, in mathcomp_eulerian.altsub]
size_in_expand_cde [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
size_mmtree_to_seq_node [lemma, in mathcomp_eulerian.psi_cdindex_tree]
size_witness_perm [lemma, in mathcomp_eulerian.psi_cdindex_witness]
size_descent_to_bvec [lemma, in mathcomp_eulerian.perm_seq_basics]
size_count_lt_gt [lemma, in mathcomp_eulerian.foata]
size_psi [lemma, in mathcomp_eulerian.psi_core]
size_rank_shift_seq2 [lemma, in mathcomp_eulerian.psi_core]
size_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]
size_inv_pref [lemma, in mathcomp_fps.fps]
SlotInterval [section, in mathcomp_eulerian.altsub]
SlotInterval.n [variable, in mathcomp_eulerian.altsub]
slot_descent_const_strict [lemma, in mathcomp_eulerian.altsub]
slot_descent_const [lemma, in mathcomp_eulerian.altsub]
slot_iv [definition, in mathcomp_eulerian.altsub]
sorted_val_enum_ord [lemma, in mathcomp_eulerian.altsub]
sorted_uniq_nth_ltn [lemma, in mathcomp_eulerian.psi_comm]
sorted_last_ge [lemma, in mathcomp_eulerian.psi_core]
sorted_head_le [lemma, in mathcomp_eulerian.psi_core]
sorted_ltn_val_enum [lemma, in mathcomp_eulerian.reflection]
sort_perm_eq_leq_seqb [lemma, in mathcomp_eulerian.psi_cdindex_core]
sort_enum_subseq_enum [lemma, in mathcomp_eulerian.altsub]
sort_enum_strict_sorted [lemma, in mathcomp_eulerian.altsub]
sort_map_mono [lemma, in mathcomp_eulerian.psi_comm]
sort_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]
split_blocks_inv_eq [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_eq [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_cyc_wf [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_app_notP [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_flatten [lemma, in mathcomp_eulerian.foata]
split_blocks_inv [definition, in mathcomp_eulerian.foata]
split_blocks_inv_aux [definition, in mathcomp_eulerian.foata]
split_blocks_gt_strict [lemma, in mathcomp_eulerian.foata]
split_blocks_lt_strict [lemma, in mathcomp_eulerian.foata]
split_blocks_size_eq [lemma, in mathcomp_eulerian.foata]
split_blocks_aux_size_when_last_P [lemma, in mathcomp_eulerian.foata]
split_blocks_wf [lemma, in mathcomp_eulerian.foata]
split_blocks_aux_wf [lemma, in mathcomp_eulerian.foata]
split_blocks_aux_all_nonempty [lemma, in mathcomp_eulerian.foata]
split_blocks_flatten [lemma, in mathcomp_eulerian.foata]
split_blocks_aux_flatten [lemma, in mathcomp_eulerian.foata]
split_blocks [definition, in mathcomp_eulerian.foata]
split_blocks_aux [definition, in mathcomp_eulerian.foata]
split_embed [lemma, in mathcomp_eulerian.reflection]
split_pos_inj [lemma, in mathcomp_eulerian.reflection]
split_pos [definition, in mathcomp_eulerian.reflection]
stanley_1_6_1_coef [lemma, in mathcomp_eulerian.stanley_egf]
stanley_1_6_1 [lemma, in mathcomp_eulerian.stanley_egf]
stanley_1_4_inv [lemma, in mathcomp_eulerian.stanley_ogf]
stanley_1_4 [lemma, in mathcomp_eulerian.stanley_ogf]
stanley_1_4_div [lemma, in mathcomp_eulerian.stanley_ogf]
stanley_ogf [library]
stanley_egf [library]
stirling_cycle_egf [lemma, in mathcomp_eulerian.stirling_egf]
stirling_ode_convert [lemma, in mathcomp_eulerian.stirling_egf]
stirling_egf_ode1 [lemma, in mathcomp_eulerian.stirling_egf]
stirling_egf0 [lemma, in mathcomp_eulerian.stirling_egf]
stirling_egf [definition, in mathcomp_eulerian.stirling_egf]
stirling_pol_rec [lemma, in mathcomp_eulerian.stirling_egf]
stirling_pol0 [lemma, in mathcomp_eulerian.stirling_egf]
stirling_pol [definition, in mathcomp_eulerian.stirling_egf]
stirling_c_out [lemma, in mathcomp_eulerian.stirling_egf]
stirling_cS0 [lemma, in mathcomp_eulerian.stirling_egf]
stirling_c00 [lemma, in mathcomp_eulerian.stirling_egf]
stirling_c_row_sum_fact [lemma, in mathcomp_eulerian.cycles]
stirling_c_row_sum [lemma, in mathcomp_eulerian.cycles]
stirling_c [definition, in mathcomp_eulerian.cycles]
stirling_c_rec [lemma, in mathcomp_eulerian.stirling_fiber]
stirling_fiber [library]
stirling_egf [library]
strict_witness_ex3 [definition, in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_ex2 [definition, in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_ex1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_exists [lemma, in mathcomp_eulerian.psi_cdindex_witness]
subseq_powerset_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
subseq_powerset_of [lemma, in mathcomp_eulerian.psi_cdindex_core]
subseq_drop_extra [lemma, in mathcomp_eulerian.altsub]
subset_powerset_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
subset_powerset_of [lemma, in mathcomp_eulerian.psi_cdindex_core]
sub_gt0_n_j [lemma, in mathcomp_eulerian.reflection]
sub_succ [lemma, in mathcomp_eulerian.reflection]
sum_descent [lemma, in mathcomp_eulerian.eulerian]
sum_des_eq_eul_pol [lemma, in mathcomp_eulerian.qeul]
sum_beta_eq_fact [lemma, in mathcomp_eulerian.beta]
sum_bin_stair [lemma, in mathcomp_fps.fps_ogf]
sum_succ_ord_eq_bin2 [lemma, in mathcomp_eulerian.inversions]
sum_asc_gaps [lemma, in mathcomp_eulerian.qeul_rec]
sum_desc_gaps [lemma, in mathcomp_eulerian.qeul_rec]
sum_in_nat_of_bool [lemma, in mathcomp_eulerian.qeul_rec]
sum_rank_gt [lemma, in mathcomp_eulerian.qeul_rec]
sum_rank_lt [lemma, in mathcomp_eulerian.qeul_rec]
sum_geq_p [lemma, in mathcomp_eulerian.qfact]
sum_rev_X [lemma, in mathcomp_eulerian.qfact]
sum_inv_cyc_gt_blocks [lemma, in mathcomp_eulerian.foata]
sum_inv_cyc_lt_blocks [lemma, in mathcomp_eulerian.foata]
sum_size_belast_wf [lemma, in mathcomp_eulerian.foata]
sum_set_is_alt_eq_andre_sum [lemma, in mathcomp_eulerian.reflection]
sum_set_is_alt_ord_max [lemma, in mathcomp_eulerian.reflection]
sum_set_is_alt_ord0 [lemma, in mathcomp_eulerian.reflection]
sum_descent_set_indicator [lemma, in mathcomp_eulerian.reflection]
sum_reindex_inner [lemma, in mathcomp_eulerian.reflection]
sum_partition_image_left [lemma, in mathcomp_eulerian.reflection]
sym_diff [definition, in mathcomp_eulerian.beta_omega]
S_w_seq_decomp_mm [lemma, in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_bound [lemma, in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_all_lt [lemma, in mathcomp_eulerian.perm_seq_bridge]
S_w_seq_witness_perm [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_map_succ [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_shift [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_witness_k0 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_core [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex4 [definition, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex3 [definition, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex2 [definition, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq [definition, in mathcomp_eulerian.psi_cdindex_witness]

T

take_mm_eq [lemma, in mathcomp_eulerian.psi_descent_v2]
take_mm_psi [lemma, in mathcomp_eulerian.psi_core]
take_psi_perm [lemma, in mathcomp_eulerian.psi_core]
take_psi [lemma, in mathcomp_eulerian.psi_core]
tanf [definition, in mathcomp_fps.fps_trig]
tanf_deriv [lemma, in mathcomp_fps.fps_trig]
tanf0 [lemma, in mathcomp_fps.fps_trig]
tcs_12345 [definition, in mathcomp_eulerian.altsub]
tcs_321 [definition, in mathcomp_eulerian.altsub]
tcs_3142 [definition, in mathcomp_eulerian.altsub]
tcs_312 [definition, in mathcomp_eulerian.altsub]
toggle_at_j_omega_strict_superset [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_j_omega_bit_i_new [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_omega_strict_superset [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_omega_bit_i_new [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_other [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_self [lemma, in mathcomp_eulerian.beta_omega]
toggle_atK [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_in [lemma, in mathcomp_eulerian.beta_omega]
toggle_at [definition, in mathcomp_eulerian.beta_omega]
toggle_at_compl [lemma, in mathcomp_eulerian.beta_swap]
transitions_expand_cde_mem [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
tree_structure [lemma, in mathcomp_eulerian.psi_descent_v2]
tree_structure_via_tree [lemma, in mathcomp_eulerian.psi_descent_v2]
tree_props [definition, in mathcomp_eulerian.psi_descent_v2]
triangle_xor_nat [lemma, in mathcomp_eulerian.altsub]
Trig [section, in mathcomp_fps.fps_trig]
Trig.charF0 [variable, in mathcomp_fps.fps_trig]
Trig.F [variable, in mathcomp_fps.fps_trig]
triple_flip_pos_seq [lemma, in mathcomp_eulerian.altsub]
TurnDefs [section, in mathcomp_eulerian.altsub]
TurnDefs.n [variable, in mathcomp_eulerian.altsub]
TurnLemmas [section, in mathcomp_eulerian.altsub]
TurnLemmas.n [variable, in mathcomp_eulerian.altsub]
turn_image_lt_max [lemma, in mathcomp_eulerian.altsub]
turn_witness [definition, in mathcomp_eulerian.altsub]
turn_inj_inj [lemma, in mathcomp_eulerian.altsub]
turn_inj [definition, in mathcomp_eulerian.altsub]
turn_iv_subset [lemma, in mathcomp_eulerian.altsub]
turn_iv [definition, in mathcomp_eulerian.altsub]
turn_count_seq [definition, in mathcomp_eulerian.altsub]
turn_count_alt_desc [lemma, in mathcomp_eulerian.altsub]
turn_count_id [lemma, in mathcomp_eulerian.altsub]
turn_count_le [lemma, in mathcomp_eulerian.altsub]
turn_count [definition, in mathcomp_eulerian.altsub]
two_eulerA_split [lemma, in mathcomp_eulerian.reflection]
t_embed_right_inj [lemma, in mathcomp_eulerian.reflection]
t_embed_inj [lemma, in mathcomp_eulerian.reflection]

U

uniq_powerset_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
uniq_powerset_of [lemma, in mathcomp_eulerian.psi_cdindex_core]
uniq_map_char_mono_powerset [lemma, in mathcomp_eulerian.psi_cdindex_support]
uniq_expand_cde [lemma, in mathcomp_eulerian.psi_cdindex_support]
uniq_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_defs]
uniq_adj_of_uniq [lemma, in mathcomp_eulerian.altsub]
uniq_adj_head_neq [lemma, in mathcomp_eulerian.altsub]
uniq_adj [definition, in mathcomp_eulerian.altsub]
uniq_expand_cde [lemma, in mathcomp_eulerian.perm_seq_bridge]
uniq_set_to_seq [lemma, in mathcomp_eulerian.beta_bridge]
uniq_psi [lemma, in mathcomp_eulerian.psi_core]
uniq_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]
UnliftOrd [section, in mathcomp_eulerian.ordinal_reindex]
UnliftOrd.n [variable, in mathcomp_eulerian.ordinal_reindex]
UpperBound [section, in mathcomp_eulerian.altsub]
UpperBoundAssembly [section, in mathcomp_eulerian.altsub]
UpperBoundAssembly.n [variable, in mathcomp_eulerian.altsub]
UpperBoundChain [section, in mathcomp_eulerian.altsub]
UpperBoundChain.n [variable, in mathcomp_eulerian.altsub]
UpperBound.n [variable, in mathcomp_eulerian.altsub]

V

valid_mm_build [lemma, in mathcomp_eulerian.psi_descent_v2]
valid_mm [definition, in mathcomp_eulerian.psi_descent_v2]
val_turn_inj [lemma, in mathcomp_eulerian.altsub]

W

wa_bridge_right [lemma, in mathcomp_eulerian.psi_descent_v2]
wa_bridge_root [lemma, in mathcomp_eulerian.psi_descent_v2]
wa_bridge_left [lemma, in mathcomp_eulerian.psi_descent_v2]
wf_block_decomp [lemma, in mathcomp_eulerian.foata]
wf_block_rcons [lemma, in mathcomp_eulerian.foata]
wf_block [definition, in mathcomp_eulerian.foata]
widenSn_neq_ord_max [lemma, in mathcomp_eulerian.eulerian]
widenSn_inj [lemma, in mathcomp_eulerian.eulerian]
widen_inj [lemma, in mathcomp_eulerian.reflection]
window_size_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
window_at_uniq [lemma, in mathcomp_eulerian.psi_descent_thms]
window_size_of_shape [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
window_size_t_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_gt [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_lt [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_t [definition, in mathcomp_eulerian.psi_cdindex_tree]
window_size_last [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_last_fuel [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex3 [definition, in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex2 [definition, in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex1 [definition, in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ancestor_ex [definition, in mathcomp_eulerian.psi_comm]
window_size_psi_ancestor [lemma, in mathcomp_eulerian.psi_comm]
window_at_psi_disjoint [lemma, in mathcomp_eulerian.psi_comm]
window_size_psi [lemma, in mathcomp_eulerian.psi_comm]
window_size_order_iso [lemma, in mathcomp_eulerian.psi_core]
window_trichotomy_ex [definition, in mathcomp_eulerian.psi_core]
window_trichotomy [lemma, in mathcomp_eulerian.psi_core]
window_head_extremum [lemma, in mathcomp_eulerian.psi_core]
window_at_psi_self [lemma, in mathcomp_eulerian.psi_core]
window_size_psi_self [lemma, in mathcomp_eulerian.psi_core]
window_fits_left [lemma, in mathcomp_eulerian.psi_core]
window_at_cons [lemma, in mathcomp_eulerian.psi_core]
window_size_cons [lemma, in mathcomp_eulerian.psi_core]
window_size_fuel_monotone [lemma, in mathcomp_eulerian.psi_core]
window_size_oor [lemma, in mathcomp_eulerian.psi_core]
window_size_bound [lemma, in mathcomp_eulerian.psi_core]
window_size_gt0 [lemma, in mathcomp_eulerian.psi_core]
window_size_fuel_bound [lemma, in mathcomp_eulerian.psi_core]
window_at [definition, in mathcomp_eulerian.psi_core]
window_size [definition, in mathcomp_eulerian.psi_core]
window_size_fuel [definition, in mathcomp_eulerian.psi_core]
witness_perm_uniq [lemma, in mathcomp_eulerian.psi_cdindex_witness]
witness_perm [definition, in mathcomp_eulerian.psi_cdindex_witness]
worpitzky [lemma, in mathcomp_eulerian.eulerian]
worpitzky [lemma, in mathcomp_eulerian.worpitzky]
worpitzky [library]
worpitzky_binom_id [lemma, in mathcomp_eulerian.eulerian]
worpitzky_bin_step [lemma, in mathcomp_eulerian.worpitzky]
ws_core_1 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
ws_bridge_right [lemma, in mathcomp_eulerian.psi_descent_v2]
ws_bridge_root [lemma, in mathcomp_eulerian.psi_descent_v2]
ws_bridge_left [lemma, in mathcomp_eulerian.psi_descent_v2]
ws_lt_size [lemma, in mathcomp_eulerian.psi_core]

X

xone_desc_eq [lemma, in mathcomp_eulerian.psi_descent_v2]

other

'Xf (ring_scope) [notation, in mathcomp_fps.fps]
\fps _ .x^ _ (ring_scope) [notation, in mathcomp_fps.fps]
_ ``_ _ (ring_scope) [notation, in mathcomp_fps.fps]
{ fps _ } (type_scope) [notation, in mathcomp_fps.fps]
σ [abbreviation, in mathcomp_eulerian.qfact]

---

Notation Index

other

'Xf (ring_scope) [in mathcomp_fps.fps]
\fps _ .x^ _ (ring_scope) [in mathcomp_fps.fps]
_ ``_ _ (ring_scope) [in mathcomp_fps.fps]
{ fps _ } (type_scope) [in mathcomp_fps.fps]

---

Variable Index

A

AltDesc.n [in mathcomp_eulerian.altsub]
AndreInterior.c [in mathcomp_eulerian.reflection]
AndreInterior.n [in mathcomp_eulerian.reflection]
AndreInterior.s [in mathcomp_eulerian.reflection]
AsPermMaxBoundsM.n [in mathcomp_eulerian.altsub]
AsPermMaxBounds.n [in mathcomp_eulerian.altsub]
AssembleDecompFull.Hx0L [in mathcomp_eulerian.reflection]
AssembleDecompFull.Hx0R [in mathcomp_eulerian.reflection]
AssembleDecompFull.j [in mathcomp_eulerian.reflection]
AssembleDecompFull.n [in mathcomp_eulerian.reflection]
AssembleDecompFull.t [in mathcomp_eulerian.reflection]
AssembleDecompFull.x0L [in mathcomp_eulerian.reflection]
AssembleDecompFull.x0R [in mathcomp_eulerian.reflection]
AssembleForwardLeft.Hx0L [in mathcomp_eulerian.reflection]
AssembleForwardLeft.Hx0R [in mathcomp_eulerian.reflection]
AssembleForwardLeft.j [in mathcomp_eulerian.reflection]
AssembleForwardLeft.n [in mathcomp_eulerian.reflection]
AssembleForwardLeft.t [in mathcomp_eulerian.reflection]
AssembleForwardLeft.x0L [in mathcomp_eulerian.reflection]
AssembleForwardLeft.x0R [in mathcomp_eulerian.reflection]
AssembleForwardRight.Hx0L [in mathcomp_eulerian.reflection]
AssembleForwardRight.Hx0R [in mathcomp_eulerian.reflection]
AssembleForwardRight.j [in mathcomp_eulerian.reflection]
AssembleForwardRight.n [in mathcomp_eulerian.reflection]
AssembleForwardRight.t [in mathcomp_eulerian.reflection]
AssembleForwardRight.x0L [in mathcomp_eulerian.reflection]
AssembleForwardRight.x0R [in mathcomp_eulerian.reflection]
AssemblePermLeftRT.HL [in mathcomp_eulerian.reflection]
AssemblePermLeftRT.j [in mathcomp_eulerian.reflection]
AssemblePermLeftRT.L [in mathcomp_eulerian.reflection]
AssemblePermLeftRT.n [in mathcomp_eulerian.reflection]
AssemblePermLeftRT.sL [in mathcomp_eulerian.reflection]
AssemblePermLeftRT.sR [in mathcomp_eulerian.reflection]
AssemblePermLeftRT.t [in mathcomp_eulerian.reflection]
AssembleRoundTrip.HL [in mathcomp_eulerian.reflection]
AssembleRoundTrip.j [in mathcomp_eulerian.reflection]
AssembleRoundTrip.L [in mathcomp_eulerian.reflection]
AssembleRoundTrip.n [in mathcomp_eulerian.reflection]
AssembleRoundTrip.sL [in mathcomp_eulerian.reflection]
AssembleRoundTrip.sR [in mathcomp_eulerian.reflection]
AssembleRoundTrip.t [in mathcomp_eulerian.reflection]
AssembleUnique.HL [in mathcomp_eulerian.reflection]
AssembleUnique.j [in mathcomp_eulerian.reflection]
AssembleUnique.L [in mathcomp_eulerian.reflection]
AssembleUnique.n [in mathcomp_eulerian.reflection]
AssembleUnique.sL [in mathcomp_eulerian.reflection]
AssembleUnique.sR [in mathcomp_eulerian.reflection]
AssembleUnique.t [in mathcomp_eulerian.reflection]

B

Bridges.Hmm [in mathcomp_eulerian.psi_descent_v2]
Bridges.s [in mathcomp_eulerian.psi_descent_v2]
Bridges.sl [in mathcomp_eulerian.psi_descent_v2]
Bridges.sr [in mathcomp_eulerian.psi_descent_v2]
Bridges.x [in mathcomp_eulerian.psi_descent_v2]

C

Cancellation.n [in mathcomp_eulerian.perm_compress]
CycleCountInsertAfter.j0 [in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.n [in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.s [in mathcomp_eulerian.stirling_fiber]

D

DescentDrop.n [in mathcomp_eulerian.descent]
DescentReverse.n [in mathcomp_eulerian.descent]
DescentSplitRight.Hjn [in mathcomp_eulerian.reflection]
DescentSplitRight.j [in mathcomp_eulerian.reflection]
DescentSplitRight.n [in mathcomp_eulerian.reflection]
DescentSplitRight.t [in mathcomp_eulerian.reflection]
DescentSplit.Hk [in mathcomp_eulerian.reflection]
DescentSplit.Hkn [in mathcomp_eulerian.reflection]
DescentSplit.j [in mathcomp_eulerian.reflection]
DescentSplit.k [in mathcomp_eulerian.reflection]
DescentSplit.n [in mathcomp_eulerian.reflection]
DescentSplit.t [in mathcomp_eulerian.reflection]
DescentTranslateRight.Hj [in mathcomp_eulerian.reflection]
DescentTranslateRight.j [in mathcomp_eulerian.reflection]
DescentTranslateRight.n [in mathcomp_eulerian.reflection]
DescentTranslateRight.t [in mathcomp_eulerian.reflection]
DescentTranslate.Hk [in mathcomp_eulerian.reflection]
DescentTranslate.Hkn [in mathcomp_eulerian.reflection]
DescentTranslate.j [in mathcomp_eulerian.reflection]
DescentTranslate.k [in mathcomp_eulerian.reflection]
DescentTranslate.n [in mathcomp_eulerian.reflection]
DescentTranslate.t [in mathcomp_eulerian.reflection]
Descent.n [in mathcomp_eulerian.descent]
DesInsertMax.n [in mathcomp_eulerian.eulerian]
DesInsertMax.t [in mathcomp_eulerian.eulerian]
DropPerm.n [in mathcomp_eulerian.perm_compress]
DropPerm.s [in mathcomp_eulerian.perm_compress]

E

Egf.charF0 [in mathcomp_fps.fps_egf]
Egf.F [in mathcomp_fps.fps_egf]
Equidistribution.FoataPerm.n [in mathcomp_eulerian.foata]
ExistenceLB.n [in mathcomp_eulerian.altsub]
ExtractMax.n [in mathcomp_eulerian.eulerian]
ExtractMax.p [in mathcomp_eulerian.eulerian]
ExtractMax.s [in mathcomp_eulerian.eulerian]
ExtractMax.sp [in mathcomp_eulerian.eulerian]

F

FoataBlocks.n [in mathcomp_eulerian.beta_omega]
FpsCompUnit.R [in mathcomp_fps.fps_comp]
FpsComp.R [in mathcomp_fps.fps_comp]
FpsDerivChar0.charF0 [in mathcomp_fps.fps_deriv]
FpsDerivChar0.F [in mathcomp_fps.fps_deriv]
FpsDeriv.R [in mathcomp_fps.fps_deriv]
FpsExpLog.natU [in mathcomp_fps.fps_explog]
FpsExpLog.R [in mathcomp_fps.fps_explog]
FpsExt.R [in mathcomp_fps.fps]
FpsOde.charF0 [in mathcomp_fps.fps_ode]
FpsOde.F [in mathcomp_fps.fps_ode]
FpsRing.R [in mathcomp_fps.fps]
FpsUnitRing.R [in mathcomp_fps.fps]
FpsZmod.R [in mathcomp_fps.fps]

G

Geometric.R [in mathcomp_fps.fps]
Geometric.sum_delta [in mathcomp_fps.fps]
GeomPowers.R [in mathcomp_fps.fps_ogf]

H

hb_instance_4.R [in mathcomp_fps.fps]
hb_instance_1.R [in mathcomp_fps.fps]
H1.n [in mathcomp_eulerian.cycles_rec]
H1.s [in mathcomp_eulerian.cycles_rec]

I

ImageLeft.j [in mathcomp_eulerian.reflection]
ImageLeft.n [in mathcomp_eulerian.reflection]
ImageLeft.t [in mathcomp_eulerian.reflection]
ImageRight.j [in mathcomp_eulerian.reflection]
ImageRight.n [in mathcomp_eulerian.reflection]
ImageRight.t [in mathcomp_eulerian.reflection]
InnerReindexBij.Hj [in mathcomp_eulerian.reflection]
InnerReindexBij.Hjn [in mathcomp_eulerian.reflection]
InnerReindexBij.HL [in mathcomp_eulerian.reflection]
InnerReindexBij.HxLcan [in mathcomp_eulerian.reflection]
InnerReindexBij.HxRcan [in mathcomp_eulerian.reflection]
InnerReindexBij.j [in mathcomp_eulerian.reflection]
InnerReindexBij.L [in mathcomp_eulerian.reflection]
InnerReindexBij.n [in mathcomp_eulerian.reflection]
InnerReindexBij.xLcan [in mathcomp_eulerian.reflection]
InnerReindexBij.xRcan [in mathcomp_eulerian.reflection]
InsertAfter.n [in mathcomp_eulerian.stirling_fiber]
InsertExtractBij.n [in mathcomp_eulerian.eulerian]
InsertMax.n [in mathcomp_eulerian.eulerian]
InsertMax.p [in mathcomp_eulerian.eulerian]
InsertMax.t [in mathcomp_eulerian.eulerian]
InterTurn.n [in mathcomp_eulerian.altsub]
Inversions.n [in mathcomp_eulerian.inversions]
InvInsertMax.n [in mathcomp_eulerian.qfact]
InvInsertMax.p [in mathcomp_eulerian.qfact]
InvInsertMax.t [in mathcomp_eulerian.qfact]
InvMajBoundsRev.n [in mathcomp_eulerian.inversions]

L

LiftOrd.n [in mathcomp_eulerian.ordinal_reindex]
LiftPerm.k [in mathcomp_eulerian.perm_compress]
LiftPerm.n [in mathcomp_eulerian.perm_compress]
LiftPerm.t [in mathcomp_eulerian.perm_compress]
LowerBound.n [in mathcomp_eulerian.altsub]

M

MajorIndex.n [in mathcomp_eulerian.inversions]
MaxAlternation.n [in mathcomp_eulerian.altsub]

P

PermOfLeft.j [in mathcomp_eulerian.reflection]
PermOfLeft.n [in mathcomp_eulerian.reflection]
PermOfLeft.t [in mathcomp_eulerian.reflection]
PermOfRight.j [in mathcomp_eulerian.reflection]
PermOfRight.n [in mathcomp_eulerian.reflection]
PermOfRight.t [in mathcomp_eulerian.reflection]
PhaseARight.Hjn [in mathcomp_eulerian.reflection]
PhaseARight.j [in mathcomp_eulerian.reflection]
PhaseARight.n [in mathcomp_eulerian.reflection]
PhaseARight.t [in mathcomp_eulerian.reflection]
PhaseA.Hk [in mathcomp_eulerian.reflection]
PhaseA.Hkn [in mathcomp_eulerian.reflection]
PhaseA.j [in mathcomp_eulerian.reflection]
PhaseA.k [in mathcomp_eulerian.reflection]
PhaseA.n [in mathcomp_eulerian.reflection]
PhaseA.t [in mathcomp_eulerian.reflection]
PhaseB.HL [in mathcomp_eulerian.reflection]
PhaseB.j [in mathcomp_eulerian.reflection]
PhaseB.L [in mathcomp_eulerian.reflection]
PhaseB.n [in mathcomp_eulerian.reflection]
PhaseB.sL [in mathcomp_eulerian.reflection]
PhaseB.sR [in mathcomp_eulerian.reflection]
PickSeqFull.n [in mathcomp_eulerian.altsub]
PolyFps.R [in mathcomp_fps.fps]

S

SeqToPerm.Hbnd [in mathcomp_eulerian.perm_seq_basics]
SeqToPerm.Hsz [in mathcomp_eulerian.perm_seq_basics]
SeqToPerm.Huniq [in mathcomp_eulerian.perm_seq_basics]
SeqToPerm.n [in mathcomp_eulerian.perm_seq_basics]
SeqToPerm.w [in mathcomp_eulerian.perm_seq_basics]
SignPerm.n [in mathcomp_eulerian.altsub]
SlotInterval.n [in mathcomp_eulerian.altsub]

T

Trig.charF0 [in mathcomp_fps.fps_trig]
Trig.F [in mathcomp_fps.fps_trig]
TurnDefs.n [in mathcomp_eulerian.altsub]
TurnLemmas.n [in mathcomp_eulerian.altsub]

U

UnliftOrd.n [in mathcomp_eulerian.ordinal_reindex]
UpperBoundAssembly.n [in mathcomp_eulerian.altsub]
UpperBoundChain.n [in mathcomp_eulerian.altsub]
UpperBound.n [in mathcomp_eulerian.altsub]

---

Library Index

A

altsub

B

beta
beta_swap
beta_bridge
beta_omega

C

carlitz
cycles
cycles_rec

D

descent

E

eulerian

F

foata
fps
fps_trig
fps_ode
fps_egf
fps_deriv
fps_comp
fps_explog
fps_ogf

I

inversions

M

mmtree

O

ordinal_reindex

P

perm_seq_bridge
perm_compress
perm_seq_basics
psi_descent_v2
psi_cdindex_support
psi_comm
psi_cdindex_tree_shape
psi_cdindex_tree_hlc
psi_cdindex_tree
psi_cdindex_defs
psi_descent
psi_core
psi_descent_thms
psi_cdindex_witness
psi_cdindex_core
psi_cdindex_support_defs

Q

qbin
qeul
qeul_rec
qfact
qworpitzky

R

reflection

S

stanley_ogf
stanley_egf
stirling_fiber
stirling_egf

W

worpitzky

---

Lemma Index

A

all_bnd_apply_psis [in mathcomp_eulerian.perm_seq_bridge]
all_le_iota' [in mathcomp_eulerian.psi_cdindex_witness]
alt_aux_from_sign [in mathcomp_eulerian.altsub]
alt_plus_nalt_as_set_is_alt_sum [in mathcomp_eulerian.reflection]
alt_desc_set_is_alt [in mathcomp_eulerian.reflection]
alt_desc_set_1 [in mathcomp_eulerian.reflection]
alt_desc_set_0 [in mathcomp_eulerian.reflection]
andre_interior_count [in mathcomp_eulerian.reflection]
andre_union_eq_split [in mathcomp_eulerian.reflection]
andre_target_gt [in mathcomp_eulerian.reflection]
andre_target_at [in mathcomp_eulerian.reflection]
andre_target_lt [in mathcomp_eulerian.reflection]
andre_s_ltn [in mathcomp_eulerian.reflection]
andre_split_lt [in mathcomp_eulerian.reflection]
apply_psis_cat [in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_nil [in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_size_eq [in mathcomp_eulerian.perm_seq_bridge]
apply_psis_cancel [in mathcomp_eulerian.perm_seq_bridge]
apply_psis_revK [in mathcomp_eulerian.perm_seq_bridge]
apply_psis_rev [in mathcomp_eulerian.perm_seq_bridge]
assemble_decomp_inverse_gen [in mathcomp_eulerian.reflection]
assemble_perm_pirr [in mathcomp_eulerian.reflection]
assemble_decomp_unique [in mathcomp_eulerian.reflection]
assemble_decomp_inverse [in mathcomp_eulerian.reflection]
assemble_decomp_inverse_right [in mathcomp_eulerian.reflection]
assemble_decomp_inverse_left [in mathcomp_eulerian.reflection]
assemble_perm_right [in mathcomp_eulerian.reflection]
assemble_perm_left [in mathcomp_eulerian.reflection]
assemble_image_right [in mathcomp_eulerian.reflection]
assemble_image_left [in mathcomp_eulerian.reflection]
assemble_right [in mathcomp_eulerian.reflection]
assemble_left [in mathcomp_eulerian.reflection]
assemble_permE [in mathcomp_eulerian.reflection]
assemble_fun_inj [in mathcomp_eulerian.reflection]
as_perm_max_eq [in mathcomp_eulerian.altsub]
as_perm_max_upper [in mathcomp_eulerian.altsub]
as_perm_max_lower [in mathcomp_eulerian.altsub]
as_perm_max_le_size [in mathcomp_eulerian.altsub]
as_perm_alt_desc [in mathcomp_eulerian.altsub]
as_permE [in mathcomp_eulerian.altsub]
aux_id [in mathcomp_eulerian.eulerian]
aux_id_step [in mathcomp_eulerian.eulerian]

B

beta_alt_max [in mathcomp_eulerian.beta_swap]
beta_set_is_alt_eq [in mathcomp_eulerian.beta_swap]
beta_compl [in mathcomp_eulerian.beta_swap]
beta_rev [in mathcomp_eulerian.beta]
beta_eulerian [in mathcomp_eulerian.beta]
beta_full [in mathcomp_eulerian.beta]
beta_andre_right [in mathcomp_eulerian.reflection]
beta_andre_left [in mathcomp_eulerian.reflection]
beta_eq_triple_split [in mathcomp_eulerian.reflection]
beta_eq_double_sum [in mathcomp_eulerian.reflection]
beta_eq_pair_sum [in mathcomp_eulerian.reflection]
beta0 [in mathcomp_eulerian.beta]
binf_neq0 [in mathcomp_fps.fps_egf]
binS' [in mathcomp_eulerian.eulerian]
block_chain_values [in mathcomp_eulerian.beta_omega]
block_chain_step [in mathcomp_eulerian.beta_omega]
block_descent_chain [in mathcomp_eulerian.beta_omega]
block_right_descent [in mathcomp_eulerian.beta_omega]
block_left_descent [in mathcomp_eulerian.beta_omega]
block_right_ge [in mathcomp_eulerian.beta_omega]
block_left_le [in mathcomp_eulerian.beta_omega]
block_right_max [in mathcomp_eulerian.beta_omega]
block_left_min [in mathcomp_eulerian.beta_omega]
block_right_right_ok [in mathcomp_eulerian.beta_omega]
block_left_left_ok [in mathcomp_eulerian.beta_omega]
bool_triangle [in mathcomp_eulerian.altsub]
boundary_cancellation_alt [in mathcomp_eulerian.reflection]
bwd_fwd [in mathcomp_eulerian.reflection]

C

cardCL_eq [in mathcomp_eulerian.reflection]
card_turn_witness [in mathcomp_eulerian.altsub]
card_turn_image [in mathcomp_eulerian.altsub]
card_split_ord_pair [in mathcomp_eulerian.inversions]
card_ord_pair [in mathcomp_eulerian.inversions]
card_split_lt_gt [in mathcomp_eulerian.qeul_rec]
card_rank_gt [in mathcomp_eulerian.qeul_rec]
card_rank_lt [in mathcomp_eulerian.qeul_rec]
card_ord_ltb [in mathcomp_eulerian.qeul_rec]
card_image_right [in mathcomp_eulerian.reflection]
card_image_left [in mathcomp_eulerian.reflection]
card_eq_ord_max_fiber [in mathcomp_eulerian.stirling_fiber]
card_neq_ord_max_fiber [in mathcomp_eulerian.stirling_fiber]
carlitz [in mathcomp_eulerian.carlitz]
carlitz_inv [in mathcomp_eulerian.carlitz]
carlitz_div [in mathcomp_eulerian.carlitz]
cast_to_subj_inj [in mathcomp_eulerian.reflection]
cast_to_j_inj [in mathcomp_eulerian.reflection]
cde_total_width_phi_w [in mathcomp_eulerian.psi_cdindex_support]
cde_total_width_phi_w_all [in mathcomp_eulerian.psi_cdindex_support]
cde_total_width_cat [in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset_D_succ [in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset_C_succ [in mathcomp_eulerian.psi_cdindex_support_defs]
char_mono_apply_psis_D_bit_self [in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_D_bit_pred [in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_C_bit [in mathcomp_eulerian.psi_cdindex_core]
char_mono_psi_effect [in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_inj [in mathcomp_eulerian.psi_cdindex_support]
char_mono_apply_psis_mem [in mathcomp_eulerian.psi_cdindex_support]
char_mono_self_mem [in mathcomp_eulerian.psi_cdindex_support]
char_mono_in_expand_cde [in mathcomp_eulerian.perm_seq_bridge]
char_mono_class_inj [in mathcomp_eulerian.perm_seq_bridge]
char_mono_perm_to_seq [in mathcomp_eulerian.perm_seq_bridge]
check_fact3_size1 [in mathcomp_eulerian.psi_cdindex_core]
check_fact3P [in mathcomp_eulerian.psi_cdindex_core]
check_fact3_true [in mathcomp_eulerian.psi_cdindex_support]
check_fact3_of_perm_eq [in mathcomp_eulerian.psi_cdindex_support]
check_strict_witness_correct [in mathcomp_eulerian.psi_cdindex_witness]
classify_vertex_mm [in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_right [in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_left [in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_cde_psi [in mathcomp_eulerian.psi_cdindex_support]
classify_map_succ [in mathcomp_eulerian.psi_cdindex_witness]
classify_skip_mm0 [in mathcomp_eulerian.psi_cdindex_witness]
class_char_monos_uniq [in mathcomp_eulerian.perm_seq_bridge]
cmp_out_of_range_left [in mathcomp_eulerian.psi_descent_thms]
cmp_out_of_range [in mathcomp_eulerian.psi_descent_thms]
coefM_eql [in mathcomp_fps.fps]
coefM_eqr [in mathcomp_fps.fps]
coef_fpsXfM [in mathcomp_eulerian.stirling_egf]
coef_stirling_pol [in mathcomp_eulerian.stirling_egf]
coef_fps_primS [in mathcomp_fps.fps_deriv]
coef_fps_prim0 [in mathcomp_fps.fps_deriv]
coef_fps_deriv [in mathcomp_fps.fps_deriv]
coef_egf [in mathcomp_fps.fps_egf]
coef_fps_comp_trunc [in mathcomp_fps.fps_comp]
coef_comp_poly_eqp [in mathcomp_fps.fps_comp]
coef_comp_poly_wide [in mathcomp_fps.fps_comp]
coef_polyXn_small [in mathcomp_fps.fps_comp]
coef_fpsXn_trunc [in mathcomp_fps.fps_comp]
coef_fpsXn_small [in mathcomp_fps.fps_comp]
coef_fps_comp [in mathcomp_fps.fps_comp]
coef_q_eul_pol [in mathcomp_eulerian.qworpitzky]
coef_fps_geomXn [in mathcomp_fps.fps_ogf]
coef_fpsXfM' [in mathcomp_eulerian.carlitz]
coef_eul_pol [in mathcomp_eulerian.worpitzky]
coef_fps_onesubX [in mathcomp_fps.fps]
coef_poly_fps [in mathcomp_fps.fps]
coef_fpsZ [in mathcomp_fps.fps]
coef_fpsM [in mathcomp_fps.fps]
coef_fps1 [in mathcomp_fps.fps]
coef_fpsM_trunc [in mathcomp_fps.fps]
coef_fps_trunc [in mathcomp_fps.fps]
coef_fps_sum [in mathcomp_fps.fps]
coef_fpsB [in mathcomp_fps.fps]
coef_fpsN [in mathcomp_fps.fps]
coef_fpsD [in mathcomp_fps.fps]
coef_fps0 [in mathcomp_fps.fps]
coef0_fps_log [in mathcomp_fps.fps_explog]
coef0_fps_exp [in mathcomp_fps.fps_explog]
coef0_fps_comp [in mathcomp_fps.fps_comp]
coef0_fpsM [in mathcomp_fps.fps]
compl_perm_involutive [in mathcomp_eulerian.beta_swap]
compl_perm_inj [in mathcomp_eulerian.beta_swap]
compl_permE [in mathcomp_eulerian.beta_swap]
constant_descent_monotone [in mathcomp_eulerian.altsub]
cosf_deriv [in mathcomp_fps.fps_trig]
cosf_unit [in mathcomp_fps.fps_trig]
cosf0 [in mathcomp_fps.fps_trig]
cos_mul_sec [in mathcomp_fps.fps_trig]
count_gt_cat [in mathcomp_eulerian.foata]
count_gt_perm_eq [in mathcomp_eulerian.foata]
cross_inv_perm_eq_l [in mathcomp_eulerian.foata]
cross_inv_perm_eq_r [in mathcomp_eulerian.foata]
cross_inv_rcons [in mathcomp_eulerian.foata]
cross_inv_nil_r [in mathcomp_eulerian.foata]
cycle_count_id [in mathcomp_eulerian.cycles]
cycle_count_le [in mathcomp_eulerian.cycles]
cycle_count_lift_perm_id [in mathcomp_eulerian.cycles_rec]
cycle_count_insert_after [in mathcomp_eulerian.stirling_fiber]
cyc_first_to_backK [in mathcomp_eulerian.foata]
cyc_first_to_back_perm_eq [in mathcomp_eulerian.foata]
cyc_diff_block_gt [in mathcomp_eulerian.foata]
cyc_diff_block_lt [in mathcomp_eulerian.foata]
cyc_last_to_front_rcons [in mathcomp_eulerian.foata]
cyc_last_to_front_perm_eq [in mathcomp_eulerian.foata]

D

descent_psi_effect [in mathcomp_eulerian.psi_cdindex_core]
descent_psi_LR_swap2 [in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap1 [in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_remove [in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_add [in mathcomp_eulerian.psi_descent_thms]
descent_psi_lboundary_R [in mathcomp_eulerian.psi_descent_thms]
descent_psi_rboundary [in mathcomp_eulerian.psi_descent_thms]
descent_psi_interior [in mathcomp_eulerian.psi_descent_thms]
descent_set_compl [in mathcomp_eulerian.beta_swap]
descent_set_full_rev [in mathcomp_eulerian.beta]
descent_set_rev_perm_ord [in mathcomp_eulerian.beta]
descent_set_rev_perm [in mathcomp_eulerian.beta]
descent_to_bvec_inj [in mathcomp_eulerian.perm_seq_basics]
descent_right_part_R_image [in mathcomp_eulerian.reflection]
descent_left_part_image [in mathcomp_eulerian.reflection]
descent_boundary_right_disjoint [in mathcomp_eulerian.reflection]
descent_left_right_disjoint [in mathcomp_eulerian.reflection]
descent_left_boundary_disjoint [in mathcomp_eulerian.reflection]
descent_set_decomp_partition [in mathcomp_eulerian.reflection]
descent_right_of_t [in mathcomp_eulerian.reflection]
descent_left_of_t [in mathcomp_eulerian.reflection]
descent_set_insert_max_interior [in mathcomp_eulerian.reflection]
descent_set_insert_max_ord_max [in mathcomp_eulerian.reflection]
descent_set_insert_max_ord0 [in mathcomp_eulerian.reflection]
desc_positions_bvec [in mathcomp_eulerian.perm_seq_basics]
des_insert_max_interior [in mathcomp_eulerian.eulerian]
des_insert_max_ord_max [in mathcomp_eulerian.eulerian]
des_insert_max_ord0 [in mathcomp_eulerian.eulerian]
des_rev_perm [in mathcomp_eulerian.descent]
des_id [in mathcomp_eulerian.descent]
des_add_asc [in mathcomp_eulerian.descent]
des_le [in mathcomp_eulerian.descent]
des0_id [in mathcomp_eulerian.eulerian]
dir_right_of_turn [in mathcomp_eulerian.altsub]
dir_left_of_turn [in mathcomp_eulerian.altsub]
drop_permE [in mathcomp_eulerian.perm_compress]
drop_fun_inj [in mathcomp_eulerian.perm_compress]
drop_funE [in mathcomp_eulerian.perm_compress]
drop_fun_ne [in mathcomp_eulerian.perm_compress]
drop_mm_eq [in mathcomp_eulerian.psi_descent_v2]
drop_psi_above [in mathcomp_eulerian.psi_core]
drop_mm_psi [in mathcomp_eulerian.psi_core]
drop_psi [in mathcomp_eulerian.psi_core]
drop1_witness_map_succ [in mathcomp_eulerian.psi_cdindex_witness]
D_vertex_descent_transition [in mathcomp_eulerian.psi_cdindex_support]
D_offsets_phi_w_eq_S_w_seq [in mathcomp_eulerian.psi_cdindex_support]
D_offsets_cat_D [in mathcomp_eulerian.psi_cdindex_support]
D_offsets_cons_C [in mathcomp_eulerian.psi_cdindex_support]

E

egfD [in mathcomp_fps.fps_egf]
egfZ [in mathcomp_fps.fps_egf]
egf_deriv [in mathcomp_fps.fps_egf]
egf_mul [in mathcomp_fps.fps_egf]
egf_dirac [in mathcomp_fps.fps_egf]
egf_eq [in mathcomp_fps.fps_egf]
elem_rs_in_range [in mathcomp_eulerian.psi_descent_thms]
elem_in_range [in mathcomp_eulerian.psi_descent_thms]
embed_right_inj [in mathcomp_eulerian.reflection]
embed_left_inj [in mathcomp_eulerian.reflection]
endpoint_implies_next_has_left_child [in mathcomp_eulerian.psi_cdindex_tree]
endpoint_implies_next_t [in mathcomp_eulerian.psi_cdindex_tree]
enum_ord_split [in mathcomp_eulerian.altsub]
enum_rank_in_val_ltn [in mathcomp_eulerian.reflection]
enum_val_ltn [in mathcomp_eulerian.reflection]
enum_val_perm_right [in mathcomp_eulerian.reflection]
enum_val_perm_left [in mathcomp_eulerian.reflection]
eq_egf [in mathcomp_fps.fps_egf]
eulerA_S2 [in mathcomp_eulerian.reflection]
eulerA_2 [in mathcomp_eulerian.reflection]
eulerA_1 [in mathcomp_eulerian.reflection]
eulerA_0 [in mathcomp_eulerian.reflection]
eulerian_explicit [in mathcomp_eulerian.eulerian]
eulerian_rec [in mathcomp_eulerian.eulerian]
eulerian_n_n [in mathcomp_eulerian.eulerian]
eulerian_symm [in mathcomp_eulerian.eulerian]
eulerian_n_0 [in mathcomp_eulerian.eulerian]
eulerian_out_of_range [in mathcomp_eulerian.eulerian]
eulerian_row_sum_fact [in mathcomp_eulerian.eulerian]
eulerian_row_sum [in mathcomp_eulerian.eulerian]
euler_egf_ode [in mathcomp_eulerian.stanley_egf]
euler_egf0 [in mathcomp_eulerian.stanley_egf]
euler_rec [in mathcomp_eulerian.reflection]
euler_1 [in mathcomp_eulerian.reflection]
euler_0 [in mathcomp_eulerian.reflection]
exactly_one_descent_LR [in mathcomp_eulerian.psi_descent_v2]
expand_cde_mem_iff [in mathcomp_eulerian.psi_cdindex_support_defs]
expand_cde_mem_transitions [in mathcomp_eulerian.psi_cdindex_support_defs]
expf_deriv [in mathcomp_fps.fps_trig]
expf0 [in mathcomp_fps.fps_trig]
extract_max_widen [in mathcomp_eulerian.eulerian]
extract_max_permE [in mathcomp_eulerian.eulerian]
extract_max_fun_inj [in mathcomp_eulerian.eulerian]
extract_max_funE [in mathcomp_eulerian.eulerian]
extract_max_ne [in mathcomp_eulerian.eulerian]

F

factf_neq0 [in mathcomp_fps.fps_egf]
factU [in mathcomp_fps.fps_explog]
factU_polyrat [in mathcomp_eulerian.stirling_egf]
fact3 [in mathcomp_eulerian.psi_cdindex_support]
find_ss_spec [in mathcomp_eulerian.perm_seq_bridge]
flip_count_perm_seq_eq_turn_count [in mathcomp_eulerian.altsub]
flip_count_as_sum [in mathcomp_eulerian.altsub]
flip_count_pick_le_perm [in mathcomp_eulerian.altsub]
flip_count_is_alt_bool [in mathcomp_eulerian.altsub]
flip_count_sign_seq_le_subseq [in mathcomp_eulerian.altsub]
flip_count_pairmap_le_subseq [in mathcomp_eulerian.altsub]
flip_count_sign_seq_insert_front [in mathcomp_eulerian.altsub]
flip_count_pairmap_insert_anywhere [in mathcomp_eulerian.altsub]
flip_step_helper [in mathcomp_eulerian.altsub]
flip_count_pairmap_insert [in mathcomp_eulerian.altsub]
foata_perm_inj [in mathcomp_eulerian.foata]
foata_perm_inv_maj [in mathcomp_eulerian.foata]
foata_perm_to_seq_bnd [in mathcomp_eulerian.foata]
foata_perm_to_seq_uniq [in mathcomp_eulerian.foata]
foata_perm_to_seq_size [in mathcomp_eulerian.foata]
foata_inj_uniq [in mathcomp_eulerian.foata]
foata_invK [in mathcomp_eulerian.foata]
foata_invK_aux [in mathcomp_eulerian.foata]
foata_step_undoK [in mathcomp_eulerian.foata]
foata_inv_eq_maj [in mathcomp_eulerian.foata]
foata_step_inv [in mathcomp_eulerian.foata]
foata_step_inv_gt [in mathcomp_eulerian.foata]
foata_step_inv_lt [in mathcomp_eulerian.foata]
foata_last_eq [in mathcomp_eulerian.foata]
foata_last [in mathcomp_eulerian.foata]
foata_rcons [in mathcomp_eulerian.foata]
foata_step_last [in mathcomp_eulerian.foata]
foata_uniq [in mathcomp_eulerian.foata]
foata_size [in mathcomp_eulerian.foata]
foata_perm_eq [in mathcomp_eulerian.foata]
foata_step_perm_eq [in mathcomp_eulerian.foata]
foldr_maxn_ge [in mathcomp_eulerian.psi_cdindex_support_defs]
foldr_minn_all_gt' [in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_iota' [in mathcomp_eulerian.psi_cdindex_witness]
foldr_minn_ge' [in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_path' [in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_set_to_seq_lb [in mathcomp_eulerian.beta_bridge]
foldr_maxn_ge_nth [in mathcomp_eulerian.psi_core]
foldr_minn_le_nth [in mathcomp_eulerian.psi_core]
foldr_maxn_ge [in mathcomp_eulerian.psi_core]
foldr_maxn_aux [in mathcomp_eulerian.psi_core]
foldr_minn_le [in mathcomp_eulerian.psi_core]
foldr_minn_aux [in mathcomp_eulerian.psi_core]
fpsP [in mathcomp_fps.fps]
fps_geom_deriv [in mathcomp_eulerian.stirling_egf]
fps_exp_log_geom [in mathcomp_fps.fps_explog]
fps_expK [in mathcomp_fps.fps_explog]
fps_logK [in mathcomp_fps.fps_explog]
fps_expD [in mathcomp_fps.fps_explog]
fps_deriv_inj0U [in mathcomp_fps.fps_explog]
fps_lin_ode_uniq [in mathcomp_fps.fps_explog]
fps_log_deriv [in mathcomp_fps.fps_explog]
fps_exp_deriv [in mathcomp_fps.fps_explog]
fps_unit1 [in mathcomp_fps.fps_explog]
fps_exp_unit [in mathcomp_fps.fps_explog]
fps_l_deriv [in mathcomp_fps.fps_explog]
fps_e_deriv [in mathcomp_fps.fps_explog]
fps_l0 [in mathcomp_fps.fps_explog]
fps_e0 [in mathcomp_fps.fps_explog]
fps_deriv_inj0 [in mathcomp_fps.fps_deriv]
fps_deriv_eq0 [in mathcomp_fps.fps_deriv]
fps_derivK [in mathcomp_fps.fps_deriv]
fps_derivX [in mathcomp_fps.fps_deriv]
fps_deriv_poly [in mathcomp_fps.fps_deriv]
fps_derivM [in mathcomp_fps.fps_deriv]
fps_deriv_sum [in mathcomp_fps.fps_deriv]
fps_derivC [in mathcomp_fps.fps_deriv]
fps_deriv1 [in mathcomp_fps.fps_deriv]
fps_deriv0 [in mathcomp_fps.fps_deriv]
fps_derivZ [in mathcomp_fps.fps_deriv]
fps_derivB [in mathcomp_fps.fps_deriv]
fps_derivN [in mathcomp_fps.fps_deriv]
fps_derivD [in mathcomp_fps.fps_deriv]
fps_compV [in mathcomp_fps.fps_comp]
fps_comp_unit [in mathcomp_fps.fps_comp]
fps_comp_deriv [in mathcomp_fps.fps_comp]
fps_comp_deriv_poly [in mathcomp_fps.fps_comp]
fps_comp_coef_eqf [in mathcomp_fps.fps_comp]
fps_compM [in mathcomp_fps.fps_comp]
fps_compX [in mathcomp_fps.fps_comp]
fps_compC [in mathcomp_fps.fps_comp]
fps_comp1 [in mathcomp_fps.fps_comp]
fps_comp0 [in mathcomp_fps.fps_comp]
fps_compN [in mathcomp_fps.fps_comp]
fps_compZ [in mathcomp_fps.fps_comp]
fps_compD [in mathcomp_fps.fps_comp]
fps_quad_ode_uniq [in mathcomp_fps.fps_ode]
fps_inv_onesubX [in mathcomp_fps.fps]
fps_onesubX_unit [in mathcomp_fps.fps]
fps_unitE [in mathcomp_fps.fps]
fps_inv_out [in mathcomp_fps.fps]
fps_unitP [in mathcomp_fps.fps]
fps_mulVf [in mathcomp_fps.fps]
fps_inv_coefS [in mathcomp_fps.fps]
fps_inv_coef0 [in mathcomp_fps.fps]
fps_scaleAr [in mathcomp_fps.fps]
fps_scaleAl [in mathcomp_fps.fps]
fps_scaleDl [in mathcomp_fps.fps]
fps_scaleDr [in mathcomp_fps.fps]
fps_scale1f [in mathcomp_fps.fps]
fps_scaleA [in mathcomp_fps.fps]
fps_oner_neq0 [in mathcomp_fps.fps]
fps_mulDl [in mathcomp_fps.fps]
fps_mul1f [in mathcomp_fps.fps]
fps_trunc_one [in mathcomp_fps.fps]
fps_mulC [in mathcomp_fps.fps]
fps_mulA [in mathcomp_fps.fps]
fps_addNf [in mathcomp_fps.fps]
fps_add0f [in mathcomp_fps.fps]
fps_addC [in mathcomp_fps.fps]
fps_addA [in mathcomp_fps.fps]
fwd_bwd [in mathcomp_eulerian.reflection]

G

geq_minn' [in mathcomp_eulerian.psi_cdindex_witness]
geq_maxn' [in mathcomp_eulerian.psi_cdindex_witness]

H

has_left_child_is_internal [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_last_fuel [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_last [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_t_last_valid [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_psi [in mathcomp_eulerian.psi_cdindex_tree_shape]
has_left_child_order_iso [in mathcomp_eulerian.psi_cdindex_tree_shape]
has_left_child_of_shape [in mathcomp_eulerian.psi_cdindex_tree_shape]
has_transition_omega_seq [in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition_cons2 [in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition_cons [in mathcomp_eulerian.psi_cdindex_support_defs]
has_left_child_t_eq [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_0 [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_gt [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_eq [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_lt [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_iota [in mathcomp_eulerian.psi_cdindex_witness]
has_left_child_cons [in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel_monotone [in mathcomp_eulerian.psi_descent_v2]
has_left_child_0 [in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel_0 [in mathcomp_eulerian.psi_descent_v2]
head_max_is_descent [in mathcomp_eulerian.psi_descent_thms]
head_min_not_descent [in mathcomp_eulerian.psi_descent_thms]
head_rank_shift_seq [in mathcomp_eulerian.psi_core]
hlc_core_1 [in mathcomp_eulerian.psi_cdindex_witness]
hlc_core_not1 [in mathcomp_eulerian.psi_cdindex_witness]
hlc_bridge_right [in mathcomp_eulerian.psi_descent_v2]
hlc_bridge_root [in mathcomp_eulerian.psi_descent_v2]
hlc_bridge_left [in mathcomp_eulerian.psi_descent_v2]

I

if_sum_const [in mathcomp_eulerian.qeul_rec]
image_right_eq_compl [in mathcomp_eulerian.reflection]
image_left_card_plus_right [in mathcomp_eulerian.reflection]
image_left_right_cover [in mathcomp_eulerian.reflection]
image_left_right_disjoint [in mathcomp_eulerian.reflection]
image_left_witness_pos [in mathcomp_eulerian.reflection]
imset_rev_ord_compl [in mathcomp_eulerian.beta]
imset_rev_ord_inv [in mathcomp_eulerian.beta]
imset_lift_eq [in mathcomp_eulerian.reflection]
index_rcons_eq_size [in mathcomp_eulerian.psi_cdindex_core]
index_lt_sorted [in mathcomp_eulerian.perm_seq_bridge]
index_map_inj_in [in mathcomp_eulerian.psi_comm]
insert_max_perm_bij [in mathcomp_eulerian.eulerian]
insert_max_perm_fiber [in mathcomp_eulerian.eulerian]
insert_extract_max [in mathcomp_eulerian.eulerian]
insert_max_perm_lift [in mathcomp_eulerian.eulerian]
insert_max_perm_at_p [in mathcomp_eulerian.eulerian]
insert_max_permE [in mathcomp_eulerian.eulerian]
insert_max_fun_inj [in mathcomp_eulerian.eulerian]
insert_max_fun_lift [in mathcomp_eulerian.eulerian]
insert_max_fun_p [in mathcomp_eulerian.eulerian]
insert_after_surj [in mathcomp_eulerian.stirling_fiber]
insert_after_inj_pair [in mathcomp_eulerian.stirling_fiber]
insert_after_decomp [in mathcomp_eulerian.stirling_fiber]
insert_after_ord_max_neq [in mathcomp_eulerian.stirling_fiber]
insert_after_other [in mathcomp_eulerian.stirling_fiber]
insert_after_j0 [in mathcomp_eulerian.stirling_fiber]
insert_after_ord_max [in mathcomp_eulerian.stirling_fiber]
insert_afterE [in mathcomp_eulerian.stirling_fiber]
insert_after_fun_inj [in mathcomp_eulerian.stirling_fiber]
interior_is_turn_inj [in mathcomp_eulerian.altsub]
interior_set_is_alt [in mathcomp_eulerian.reflection]
interior_descent_set_eq [in mathcomp_eulerian.reflection]
internal_vertices_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
inter_turn_monotone_strict [in mathcomp_eulerian.altsub]
inter_turn_monotone [in mathcomp_eulerian.altsub]
inv_rev_perm [in mathcomp_eulerian.inversions]
inv_rev_perm_eq_coinv [in mathcomp_eulerian.inversions]
inv_le [in mathcomp_eulerian.inversions]
inv_double_sum [in mathcomp_eulerian.inversions]
inv_id [in mathcomp_eulerian.inversions]
inv_q_fact [in mathcomp_eulerian.qfact]
inv_insert_max [in mathcomp_eulerian.qfact]
inv_via_sum [in mathcomp_eulerian.qfact]
inv_maj_equidistr [in mathcomp_eulerian.foata]
inv_eq_inv_seq [in mathcomp_eulerian.foata]
inv_seq_cons_eq_rcons_shift [in mathcomp_eulerian.foata]
inv_seq_flatten_swap_eq [in mathcomp_eulerian.foata]
inv_seq_cat [in mathcomp_eulerian.foata]
inv_seq_rcons [in mathcomp_eulerian.foata]
inv_prefE [in mathcomp_fps.fps]
in_internal_vertices [in mathcomp_eulerian.psi_cdindex_support]
is_internal_lt [in mathcomp_eulerian.psi_cdindex_core]
is_internal_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
is_descent_compl [in mathcomp_eulerian.beta_swap]
is_alt_pick_turn_witness [in mathcomp_eulerian.altsub]
is_alt_from_sign [in mathcomp_eulerian.altsub]
is_alt_flip_count [in mathcomp_eulerian.altsub]
is_alt_three [in mathcomp_eulerian.altsub]
is_alt_cons2 [in mathcomp_eulerian.altsub]
is_internal_t_eq [in mathcomp_eulerian.psi_cdindex_tree]
is_descent_perm_seq [in mathcomp_eulerian.perm_seq_basics]
is_inv_lift_p [in mathcomp_eulerian.qfact]
is_inv_lift_pair [in mathcomp_eulerian.qfact]
is_descent_rev [in mathcomp_eulerian.descent]
is_descent_perm_right [in mathcomp_eulerian.reflection]
is_descent_perm_left [in mathcomp_eulerian.reflection]

J

j_plus_lt_n [in mathcomp_eulerian.reflection]

L

last_iota' [in mathcomp_eulerian.psi_cdindex_witness]
left_ok_self [in mathcomp_eulerian.beta_omega]
leqj_pred_n [in mathcomp_eulerian.reflection]
leq_seqb_anti [in mathcomp_eulerian.psi_cdindex_core]
leq_seqb_trans [in mathcomp_eulerian.psi_cdindex_core]
leq_seqb_total [in mathcomp_eulerian.psi_cdindex_core]
leq_maxn' [in mathcomp_eulerian.psi_cdindex_witness]
leq_lift [in mathcomp_eulerian.ordinal_reindex]
lift_perm_drop_perm [in mathcomp_eulerian.perm_compress]
lift_perm_lift [in mathcomp_eulerian.perm_compress]
lift_perm_ord_max [in mathcomp_eulerian.perm_compress]
lift_permE [in mathcomp_eulerian.perm_compress]
lift_fun_inj [in mathcomp_eulerian.perm_compress]
lift_fun_lift [in mathcomp_eulerian.perm_compress]
lift_fun_ord_max [in mathcomp_eulerian.perm_compress]
lift_drop_permE [in mathcomp_eulerian.perm_compress]
lift_perm_id_iter_lift [in mathcomp_eulerian.cycles_rec]
lift_perm_id_iter [in mathcomp_eulerian.cycles_rec]
LR_pred_is_endpoint [in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_t [in mathcomp_eulerian.psi_cdindex_tree]
ltn_lift [in mathcomp_eulerian.ordinal_reindex]

M

maj_rev_perm [in mathcomp_eulerian.inversions]
maj_le [in mathcomp_eulerian.inversions]
maj_id [in mathcomp_eulerian.inversions]
maj_insert_max_interior [in mathcomp_eulerian.qeul_rec]
maj_insert_max_ord_max [in mathcomp_eulerian.qeul_rec]
maj_insert_max_ord0 [in mathcomp_eulerian.qeul_rec]
maj_q_fact [in mathcomp_eulerian.qfact]
maj_eq_maj_seq [in mathcomp_eulerian.foata]
maj_seq_rcons [in mathcomp_eulerian.foata]
map_mod_iota_rot [in mathcomp_eulerian.psi_core]
map_nth_iota_sorted [in mathcomp_eulerian.psi_core]
max_pos_core_gt0 [in mathcomp_eulerian.psi_cdindex_witness]
max_pos_iota' [in mathcomp_eulerian.psi_cdindex_witness]
max_eq_nth_sort_last [in mathcomp_eulerian.psi_core]
max_val_drop [in mathcomp_eulerian.psi_core]
max_val_perm_eq [in mathcomp_eulerian.psi_core]
max_pos_lt [in mathcomp_eulerian.psi_core]
max_in [in mathcomp_eulerian.psi_core]
mem_omega_set [in mathcomp_eulerian.beta_omega]
mem_alt_desc_set [in mathcomp_eulerian.beta_swap]
mem_pos_seq [in mathcomp_eulerian.altsub]
mem_slot_iv [in mathcomp_eulerian.altsub]
mem_omega_seq [in mathcomp_eulerian.psi_cdindex_support_defs]
mem_filter_iota_nth [in mathcomp_eulerian.psi_cdindex_support_defs]
mem_set_to_seq_ord [in mathcomp_eulerian.beta_bridge]
mem_set_to_seq_iff [in mathcomp_eulerian.beta_bridge]
mem_set_to_seq [in mathcomp_eulerian.beta_bridge]
mem_descent_set [in mathcomp_eulerian.descent]
mem_image_right [in mathcomp_eulerian.reflection]
mem_image_left [in mathcomp_eulerian.reflection]
min_pos_lt [in mathcomp_eulerian.mmtree]
min_in [in mathcomp_eulerian.mmtree]
min_pos_core [in mathcomp_eulerian.psi_cdindex_witness]
min_pos_iota' [in mathcomp_eulerian.psi_cdindex_witness]
min_eq_nth_sort_0 [in mathcomp_eulerian.psi_core]
min_val_drop [in mathcomp_eulerian.psi_core]
min_val_perm_eq [in mathcomp_eulerian.psi_core]
mmtree_shape_psi [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_decompose [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_order_iso [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_cons [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_nil [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_fuel_monotone [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_of_seqK [in mathcomp_eulerian.mmtree]
mmtree_of_seq_fuel_correct [in mathcomp_eulerian.mmtree]
mmtree_of_seq_mmK [in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm_fuel_correct [in mathcomp_eulerian.psi_core]
mm_pos_rcons_lt [in mathcomp_eulerian.psi_cdindex_core]
mm_pos_lt_pred [in mathcomp_eulerian.psi_cdindex_support]
mm_pos_witness [in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_core [in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_min_first [in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_iota' [in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_drop_mm [in mathcomp_eulerian.psi_core]
mm_pos_order_iso [in mathcomp_eulerian.psi_core]
mm_pos_psi_eq [in mathcomp_eulerian.psi_core]
mm_pos_char [in mathcomp_eulerian.psi_core]
mm_pos_lt [in mathcomp_eulerian.psi_core]
mono_inj_in [in mathcomp_eulerian.psi_comm]

N

natf_neq0_char0 [in mathcomp_fps.fps_deriv]
natSf_neq0 [in mathcomp_fps.fps_deriv]
natU_polyrat [in mathcomp_eulerian.stirling_egf]
nat_of_andb [in mathcomp_eulerian.reflection]
neg_add_neg [in mathcomp_eulerian.altsub]
nil_in_powerset_internal [in mathcomp_eulerian.perm_seq_bridge]
notin_take_mm [in mathcomp_eulerian.psi_core]
not_set_is_alt_omega_not_full [in mathcomp_eulerian.beta_swap]
not_set_is_alt_n_ge2 [in mathcomp_eulerian.beta_swap]
not_is_descentE [in mathcomp_eulerian.altsub]
no_inner_in_pos_seq [in mathcomp_eulerian.altsub]
nth_char_mono [in mathcomp_eulerian.psi_cdindex_core]
nth_window_at [in mathcomp_eulerian.psi_descent_thms]
nth_descent_to_bvec [in mathcomp_eulerian.perm_seq_basics]
nth_perm_to_seq [in mathcomp_eulerian.perm_seq_basics]
nth_w_mm_pos [in mathcomp_eulerian.psi_core]
nth_psi_inside [in mathcomp_eulerian.psi_core]
nth_psi_right [in mathcomp_eulerian.psi_core]
nth_psi_left [in mathcomp_eulerian.psi_core]
nth_rank_shift_seq [in mathcomp_eulerian.psi_core]

O

omega_set_alt_full [in mathcomp_eulerian.beta_swap]
omega_proper_beta_lt [in mathcomp_eulerian.perm_seq_bridge]
omega_seq_subset_bounded [in mathcomp_eulerian.perm_seq_bridge]
omega_set_seq_bridge_bounded [in mathcomp_eulerian.perm_seq_bridge]
omega_seq_mem_eq [in mathcomp_eulerian.perm_seq_bridge]
omega_monotone_class_count [in mathcomp_eulerian.psi_cdindex_witness]
omega_set_seq_local_bridge [in mathcomp_eulerian.beta_bridge]
onepX_mul_altgeom [in mathcomp_fps.fps_explog]
onepX_unit [in mathcomp_fps.fps_explog]
onesubXn_mul_geomn [in mathcomp_fps.fps_ogf]
onesubX_pow_t_ode1 [in mathcomp_eulerian.stirling_egf]
onesubX_mul_geom [in mathcomp_fps.fps]
order_iso_drop [in mathcomp_eulerian.psi_core]
order_iso_take [in mathcomp_eulerian.psi_core]
ord_max_notin_turn_image [in mathcomp_eulerian.altsub]
ord0_neq_ord_max [in mathcomp_eulerian.altsub]
ord0_notin_turn_image [in mathcomp_eulerian.altsub]

P

path_iota' [in mathcomp_eulerian.psi_cdindex_witness]
path_leq_last' [in mathcomp_eulerian.psi_cdindex_witness]
perm_eq_from_subset [in mathcomp_eulerian.psi_cdindex_support]
perm_eq_apply_psis [in mathcomp_eulerian.psi_cdindex_defs]
perm_to_seq_class_map [in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_seq_to_perm [in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_bnd [in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_inj [in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_uniq [in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_size [in mathcomp_eulerian.perm_seq_basics]
perm_to_seq_foata_perm [in mathcomp_eulerian.foata]
perm_eq_flatten_map_pred [in mathcomp_eulerian.foata]
perm_eq_flatten_map_cyc [in mathcomp_eulerian.foata]
perm_right_lt_iff [in mathcomp_eulerian.reflection]
perm_left_lt_iff [in mathcomp_eulerian.reflection]
perm_right_witness_indep [in mathcomp_eulerian.reflection]
perm_rightE [in mathcomp_eulerian.reflection]
perm_right_fun_inj [in mathcomp_eulerian.reflection]
perm_left_witness_indep [in mathcomp_eulerian.reflection]
perm_leftE [in mathcomp_eulerian.reflection]
perm_left_fun_inj [in mathcomp_eulerian.reflection]
phi_w_as_map [in mathcomp_eulerian.psi_cdindex_core]
phi_w_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
phi_w_support_general [in mathcomp_eulerian.psi_cdindex_support]
phi_w_decomp_mm [in mathcomp_eulerian.psi_cdindex_support]
phi_w_cons_mm0 [in mathcomp_eulerian.psi_cdindex_support]
pick_seq_subseq_perm_seq [in mathcomp_eulerian.altsub]
pick_seq_pos_seq [in mathcomp_eulerian.altsub]
pick_seq_setT [in mathcomp_eulerian.altsub]
poly_fpsC [in mathcomp_fps.fps]
poly_fps_is_monoid_morphism [in mathcomp_fps.fps]
poly_fps_is_zmod_morphism [in mathcomp_fps.fps]
poly_fps_inj [in mathcomp_fps.fps]
porbits_lift_perm_id [in mathcomp_eulerian.cycles_rec]
porbit_id_singleton [in mathcomp_eulerian.cycles]
porbit_lift_perm_id_lift [in mathcomp_eulerian.cycles_rec]
porbit_lift_perm_id_max [in mathcomp_eulerian.cycles_rec]
post_window_extremum [in mathcomp_eulerian.psi_descent_v2]
pos_seq_last_val [in mathcomp_eulerian.altsub]
pos_seq_nth0 [in mathcomp_eulerian.altsub]
pos_seq_val_lt_inv [in mathcomp_eulerian.altsub]
pos_seq_val_lt [in mathcomp_eulerian.altsub]
pos_seq_strict_sorted [in mathcomp_eulerian.altsub]
pos_seq_uniq [in mathcomp_eulerian.altsub]
powerset_internal_apply_psis [in mathcomp_eulerian.perm_seq_bridge]
pred_sub_add [in mathcomp_eulerian.psi_descent_v2]
pre_window_extremum_R [in mathcomp_eulerian.psi_descent_v2]
pre_window_gt_min_when_max_head [in mathcomp_eulerian.psi_descent_v2]
pre_window_lt_max_when_min_head [in mathcomp_eulerian.psi_descent_v2]
pre_win_gt_min_eq [in mathcomp_eulerian.psi_descent_v2]
pre_win_lt_max_eq [in mathcomp_eulerian.psi_descent_v2]
psi_apply_psis_comm [in mathcomp_eulerian.perm_seq_bridge]
psi_comm [in mathcomp_eulerian.psi_comm]
psi_comm_nested [in mathcomp_eulerian.psi_comm]
psi_map_comm [in mathcomp_eulerian.psi_comm]
psi_comm_disjoint [in mathcomp_eulerian.psi_comm]
psi_comm_disjoint_lr [in mathcomp_eulerian.psi_comm]
psi_0_eq [in mathcomp_eulerian.psi_core]
psi_involutive [in mathcomp_eulerian.psi_core]
psi_id_trivial [in mathcomp_eulerian.psi_core]
psi_id_oor [in mathcomp_eulerian.psi_core]
psi_perm_eq [in mathcomp_eulerian.psi_core]

Q

qbinS [in mathcomp_eulerian.qbin]
qbin_absorbC [in mathcomp_eulerian.qworpitzky]
qbin_n1 [in mathcomp_eulerian.qworpitzky]
qbin_horner1 [in mathcomp_eulerian.qbin]
qbin_nn [in mathcomp_eulerian.qbin]
qbin_small [in mathcomp_eulerian.qbin]
qbin_0S [in mathcomp_eulerian.qbin]
qbin_n0 [in mathcomp_eulerian.qbin]
q_eul_pol_q1 [in mathcomp_eulerian.qeul]
q_eul_pol_t1 [in mathcomp_eulerian.qeul]
q_worpitzky [in mathcomp_eulerian.qworpitzky]
q_bin_step [in mathcomp_eulerian.qworpitzky]
q_intD [in mathcomp_eulerian.qworpitzky]
q_eulerian_rec [in mathcomp_eulerian.qeul_rec]
q_intS [in mathcomp_eulerian.qeul_rec]
q_eulerian_out_of_range [in mathcomp_eulerian.qeul_rec]
q_eulerian_n_0 [in mathcomp_eulerian.qeul_rec]
q_stairE [in mathcomp_eulerian.carlitz]
q_onesub_prod_unit [in mathcomp_eulerian.carlitz]
q_staircase [in mathcomp_eulerian.carlitz]
q_stair_step [in mathcomp_eulerian.carlitz]
q_stair0 [in mathcomp_eulerian.carlitz]

R

rank_shift_psi_comm [in mathcomp_eulerian.psi_comm]
rank_shift_map_comm [in mathcomp_eulerian.psi_comm]
rank_shift_preserves_interior_order [in mathcomp_eulerian.psi_comm]
rank_shift_head_max_to_min [in mathcomp_eulerian.psi_core]
rank_shift_head_min_to_max [in mathcomp_eulerian.psi_core]
rank_shift_seq_involutive [in mathcomp_eulerian.psi_core]
rank_shift_seqE [in mathcomp_eulerian.psi_core]
rank_shift_perm_eq [in mathcomp_eulerian.psi_core]
rat_char0 [in mathcomp_eulerian.stanley_egf]
rev_perm_involutive [in mathcomp_eulerian.eulerian]
rev_perm_inj [in mathcomp_eulerian.eulerian]
rev_ord_lt [in mathcomp_eulerian.inversions]
rev_permE [in mathcomp_eulerian.descent]
rev_perm_ordE [in mathcomp_eulerian.descent]
right_ok_self [in mathcomp_eulerian.beta_omega]
rs_head_min_no_descent [in mathcomp_eulerian.psi_descent_thms]
rs_head_max_descent [in mathcomp_eulerian.psi_descent_thms]

S

secf_deriv [in mathcomp_fps.fps_trig]
secf0 [in mathcomp_fps.fps_trig]
sectan_ode [in mathcomp_fps.fps_trig]
sectan0 [in mathcomp_fps.fps_trig]
sec2f [in mathcomp_fps.fps_trig]
seq_cat_right_eq [in mathcomp_eulerian.psi_cdindex_tree_shape]
seq_cat_left_eq [in mathcomp_eulerian.psi_cdindex_tree_shape]
seq_to_fun_inj [in mathcomp_eulerian.perm_seq_basics]
seq_nth_bound [in mathcomp_eulerian.perm_seq_basics]
setU1_imset_lift_eq [in mathcomp_eulerian.reflection]
set_is_alt_classify [in mathcomp_eulerian.beta_swap]
set_not_altP [in mathcomp_eulerian.beta_swap]
set_is_alt_indicator [in mathcomp_eulerian.reflection]
shift_preserves_ltn [in mathcomp_eulerian.psi_comm]
sign_seq_alt_of_triple_flip [in mathcomp_eulerian.altsub]
sign_flip_at_turn [in mathcomp_eulerian.altsub]
sign_seq_is_alt [in mathcomp_eulerian.altsub]
sign_seq_perm_seq [in mathcomp_eulerian.altsub]
sinf_deriv [in mathcomp_fps.fps_trig]
sinf0 [in mathcomp_fps.fps_trig]
sin2cos2 [in mathcomp_fps.fps_trig]
size_expand_cde_phi_w [in mathcomp_eulerian.psi_cdindex_core]
size_expand_cde [in mathcomp_eulerian.psi_cdindex_core]
size_powerset_internal [in mathcomp_eulerian.psi_cdindex_core]
size_powerset_of [in mathcomp_eulerian.psi_cdindex_core]
size_char_mono [in mathcomp_eulerian.psi_cdindex_core]
size_window_at [in mathcomp_eulerian.psi_descent_thms]
size_mmtree_shape [in mathcomp_eulerian.psi_cdindex_tree_shape]
size_apply_psis [in mathcomp_eulerian.psi_cdindex_defs]
size_pos_seq [in mathcomp_eulerian.altsub]
size_take_drop_skip [in mathcomp_eulerian.altsub]
size_sign_seq_perm [in mathcomp_eulerian.altsub]
size_sign_seq [in mathcomp_eulerian.altsub]
size_perm_seq [in mathcomp_eulerian.altsub]
size_in_expand_cde [in mathcomp_eulerian.psi_cdindex_support_defs]
size_mmtree_to_seq_node [in mathcomp_eulerian.psi_cdindex_tree]
size_witness_perm [in mathcomp_eulerian.psi_cdindex_witness]
size_descent_to_bvec [in mathcomp_eulerian.perm_seq_basics]
size_count_lt_gt [in mathcomp_eulerian.foata]
size_psi [in mathcomp_eulerian.psi_core]
size_rank_shift_seq2 [in mathcomp_eulerian.psi_core]
size_rank_shift_seq [in mathcomp_eulerian.psi_core]
size_inv_pref [in mathcomp_fps.fps]
slot_descent_const_strict [in mathcomp_eulerian.altsub]
slot_descent_const [in mathcomp_eulerian.altsub]
sorted_val_enum_ord [in mathcomp_eulerian.altsub]
sorted_uniq_nth_ltn [in mathcomp_eulerian.psi_comm]
sorted_last_ge [in mathcomp_eulerian.psi_core]
sorted_head_le [in mathcomp_eulerian.psi_core]
sorted_ltn_val_enum [in mathcomp_eulerian.reflection]
sort_perm_eq_leq_seqb [in mathcomp_eulerian.psi_cdindex_core]
sort_enum_subseq_enum [in mathcomp_eulerian.altsub]
sort_enum_strict_sorted [in mathcomp_eulerian.altsub]
sort_map_mono [in mathcomp_eulerian.psi_comm]
sort_rank_shift_seq [in mathcomp_eulerian.psi_core]
split_blocks_inv_eq [in mathcomp_eulerian.foata]
split_blocks_inv_aux_eq [in mathcomp_eulerian.foata]
split_blocks_inv_cyc_wf [in mathcomp_eulerian.foata]
split_blocks_inv_aux_app_notP [in mathcomp_eulerian.foata]
split_blocks_inv_aux_flatten [in mathcomp_eulerian.foata]
split_blocks_gt_strict [in mathcomp_eulerian.foata]
split_blocks_lt_strict [in mathcomp_eulerian.foata]
split_blocks_size_eq [in mathcomp_eulerian.foata]
split_blocks_aux_size_when_last_P [in mathcomp_eulerian.foata]
split_blocks_wf [in mathcomp_eulerian.foata]
split_blocks_aux_wf [in mathcomp_eulerian.foata]
split_blocks_aux_all_nonempty [in mathcomp_eulerian.foata]
split_blocks_flatten [in mathcomp_eulerian.foata]
split_blocks_aux_flatten [in mathcomp_eulerian.foata]
split_embed [in mathcomp_eulerian.reflection]
split_pos_inj [in mathcomp_eulerian.reflection]
stanley_1_6_1_coef [in mathcomp_eulerian.stanley_egf]
stanley_1_6_1 [in mathcomp_eulerian.stanley_egf]
stanley_1_4_inv [in mathcomp_eulerian.stanley_ogf]
stanley_1_4 [in mathcomp_eulerian.stanley_ogf]
stanley_1_4_div [in mathcomp_eulerian.stanley_ogf]
stirling_cycle_egf [in mathcomp_eulerian.stirling_egf]
stirling_ode_convert [in mathcomp_eulerian.stirling_egf]
stirling_egf_ode1 [in mathcomp_eulerian.stirling_egf]
stirling_egf0 [in mathcomp_eulerian.stirling_egf]
stirling_pol_rec [in mathcomp_eulerian.stirling_egf]
stirling_pol0 [in mathcomp_eulerian.stirling_egf]
stirling_c_out [in mathcomp_eulerian.stirling_egf]
stirling_cS0 [in mathcomp_eulerian.stirling_egf]
stirling_c00 [in mathcomp_eulerian.stirling_egf]
stirling_c_row_sum_fact [in mathcomp_eulerian.cycles]
stirling_c_row_sum [in mathcomp_eulerian.cycles]
stirling_c_rec [in mathcomp_eulerian.stirling_fiber]
strict_witness_exists [in mathcomp_eulerian.psi_cdindex_witness]
subseq_powerset_internal [in mathcomp_eulerian.psi_cdindex_core]
subseq_powerset_of [in mathcomp_eulerian.psi_cdindex_core]
subseq_drop_extra [in mathcomp_eulerian.altsub]
subset_powerset_internal [in mathcomp_eulerian.psi_cdindex_core]
subset_powerset_of [in mathcomp_eulerian.psi_cdindex_core]
sub_gt0_n_j [in mathcomp_eulerian.reflection]
sub_succ [in mathcomp_eulerian.reflection]
sum_descent [in mathcomp_eulerian.eulerian]
sum_des_eq_eul_pol [in mathcomp_eulerian.qeul]
sum_beta_eq_fact [in mathcomp_eulerian.beta]
sum_bin_stair [in mathcomp_fps.fps_ogf]
sum_succ_ord_eq_bin2 [in mathcomp_eulerian.inversions]
sum_asc_gaps [in mathcomp_eulerian.qeul_rec]
sum_desc_gaps [in mathcomp_eulerian.qeul_rec]
sum_in_nat_of_bool [in mathcomp_eulerian.qeul_rec]
sum_rank_gt [in mathcomp_eulerian.qeul_rec]
sum_rank_lt [in mathcomp_eulerian.qeul_rec]
sum_geq_p [in mathcomp_eulerian.qfact]
sum_rev_X [in mathcomp_eulerian.qfact]
sum_inv_cyc_gt_blocks [in mathcomp_eulerian.foata]
sum_inv_cyc_lt_blocks [in mathcomp_eulerian.foata]
sum_size_belast_wf [in mathcomp_eulerian.foata]
sum_set_is_alt_eq_andre_sum [in mathcomp_eulerian.reflection]
sum_set_is_alt_ord_max [in mathcomp_eulerian.reflection]
sum_set_is_alt_ord0 [in mathcomp_eulerian.reflection]
sum_descent_set_indicator [in mathcomp_eulerian.reflection]
sum_reindex_inner [in mathcomp_eulerian.reflection]
sum_partition_image_left [in mathcomp_eulerian.reflection]
S_w_seq_decomp_mm [in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_bound [in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_all_lt [in mathcomp_eulerian.perm_seq_bridge]
S_w_seq_witness_perm [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_map_succ [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_shift [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_witness_k0 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_core [in mathcomp_eulerian.psi_cdindex_witness]

T

take_mm_eq [in mathcomp_eulerian.psi_descent_v2]
take_mm_psi [in mathcomp_eulerian.psi_core]
take_psi_perm [in mathcomp_eulerian.psi_core]
take_psi [in mathcomp_eulerian.psi_core]
tanf_deriv [in mathcomp_fps.fps_trig]
tanf0 [in mathcomp_fps.fps_trig]
toggle_at_j_omega_strict_superset [in mathcomp_eulerian.beta_omega]
toggle_at_j_omega_bit_i_new [in mathcomp_eulerian.beta_omega]
toggle_at_omega_strict_superset [in mathcomp_eulerian.beta_omega]
toggle_at_omega_bit_i_new [in mathcomp_eulerian.beta_omega]
toggle_at_other [in mathcomp_eulerian.beta_omega]
toggle_at_self [in mathcomp_eulerian.beta_omega]
toggle_atK [in mathcomp_eulerian.beta_omega]
toggle_at_in [in mathcomp_eulerian.beta_omega]
toggle_at_compl [in mathcomp_eulerian.beta_swap]
transitions_expand_cde_mem [in mathcomp_eulerian.psi_cdindex_support_defs]
tree_structure [in mathcomp_eulerian.psi_descent_v2]
tree_structure_via_tree [in mathcomp_eulerian.psi_descent_v2]
triangle_xor_nat [in mathcomp_eulerian.altsub]
triple_flip_pos_seq [in mathcomp_eulerian.altsub]
turn_image_lt_max [in mathcomp_eulerian.altsub]
turn_inj_inj [in mathcomp_eulerian.altsub]
turn_iv_subset [in mathcomp_eulerian.altsub]
turn_count_alt_desc [in mathcomp_eulerian.altsub]
turn_count_id [in mathcomp_eulerian.altsub]
turn_count_le [in mathcomp_eulerian.altsub]
two_eulerA_split [in mathcomp_eulerian.reflection]
t_embed_right_inj [in mathcomp_eulerian.reflection]
t_embed_inj [in mathcomp_eulerian.reflection]

U

uniq_powerset_internal [in mathcomp_eulerian.psi_cdindex_core]
uniq_powerset_of [in mathcomp_eulerian.psi_cdindex_core]
uniq_map_char_mono_powerset [in mathcomp_eulerian.psi_cdindex_support]
uniq_expand_cde [in mathcomp_eulerian.psi_cdindex_support]
uniq_apply_psis [in mathcomp_eulerian.psi_cdindex_defs]
uniq_adj_of_uniq [in mathcomp_eulerian.altsub]
uniq_adj_head_neq [in mathcomp_eulerian.altsub]
uniq_expand_cde [in mathcomp_eulerian.perm_seq_bridge]
uniq_set_to_seq [in mathcomp_eulerian.beta_bridge]
uniq_psi [in mathcomp_eulerian.psi_core]
uniq_rank_shift_seq [in mathcomp_eulerian.psi_core]

V

valid_mm_build [in mathcomp_eulerian.psi_descent_v2]
val_turn_inj [in mathcomp_eulerian.altsub]

W

wa_bridge_right [in mathcomp_eulerian.psi_descent_v2]
wa_bridge_root [in mathcomp_eulerian.psi_descent_v2]
wa_bridge_left [in mathcomp_eulerian.psi_descent_v2]
wf_block_decomp [in mathcomp_eulerian.foata]
wf_block_rcons [in mathcomp_eulerian.foata]
widenSn_neq_ord_max [in mathcomp_eulerian.eulerian]
widenSn_inj [in mathcomp_eulerian.eulerian]
widen_inj [in mathcomp_eulerian.reflection]
window_size_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
window_at_uniq [in mathcomp_eulerian.psi_descent_thms]
window_size_of_shape [in mathcomp_eulerian.psi_cdindex_tree_shape]
window_size_t_eq [in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_gt [in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_eq [in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_lt [in mathcomp_eulerian.psi_cdindex_tree]
window_size_last [in mathcomp_eulerian.psi_cdindex_tree]
window_size_last_fuel [in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ancestor [in mathcomp_eulerian.psi_comm]
window_at_psi_disjoint [in mathcomp_eulerian.psi_comm]
window_size_psi [in mathcomp_eulerian.psi_comm]
window_size_order_iso [in mathcomp_eulerian.psi_core]
window_trichotomy [in mathcomp_eulerian.psi_core]
window_head_extremum [in mathcomp_eulerian.psi_core]
window_at_psi_self [in mathcomp_eulerian.psi_core]
window_size_psi_self [in mathcomp_eulerian.psi_core]
window_fits_left [in mathcomp_eulerian.psi_core]
window_at_cons [in mathcomp_eulerian.psi_core]
window_size_cons [in mathcomp_eulerian.psi_core]
window_size_fuel_monotone [in mathcomp_eulerian.psi_core]
window_size_oor [in mathcomp_eulerian.psi_core]
window_size_bound [in mathcomp_eulerian.psi_core]
window_size_gt0 [in mathcomp_eulerian.psi_core]
window_size_fuel_bound [in mathcomp_eulerian.psi_core]
witness_perm_uniq [in mathcomp_eulerian.psi_cdindex_witness]
worpitzky [in mathcomp_eulerian.eulerian]
worpitzky [in mathcomp_eulerian.worpitzky]
worpitzky_binom_id [in mathcomp_eulerian.eulerian]
worpitzky_bin_step [in mathcomp_eulerian.worpitzky]
ws_core_1 [in mathcomp_eulerian.psi_cdindex_witness]
ws_bridge_right [in mathcomp_eulerian.psi_descent_v2]
ws_bridge_root [in mathcomp_eulerian.psi_descent_v2]
ws_bridge_left [in mathcomp_eulerian.psi_descent_v2]
ws_lt_size [in mathcomp_eulerian.psi_core]

X

xone_desc_eq [in mathcomp_eulerian.psi_descent_v2]

---

Constructor Index

C

C_letter [in mathcomp_eulerian.psi_cdindex_defs]

D

D_letter [in mathcomp_eulerian.psi_cdindex_defs]

E

E_letter [in mathcomp_eulerian.psi_cdindex_defs]

L

Leaf [in mathcomp_eulerian.mmtree]

N

Node [in mathcomp_eulerian.mmtree]

---

Inductive Index

C

cde [in mathcomp_eulerian.psi_cdindex_defs]

M

mmtree [in mathcomp_eulerian.mmtree]

---

Projection Index

F

fpscoef [in mathcomp_fps.fps]

---

Section Index

A

AltDesc [in mathcomp_eulerian.altsub]
AndreInterior [in mathcomp_eulerian.reflection]
AsPermMaxBounds [in mathcomp_eulerian.altsub]
AsPermMaxBoundsM [in mathcomp_eulerian.altsub]
AssembleDecompFull [in mathcomp_eulerian.reflection]
AssembleForwardLeft [in mathcomp_eulerian.reflection]
AssembleForwardRight [in mathcomp_eulerian.reflection]
AssemblePermLeftRT [in mathcomp_eulerian.reflection]
AssembleRoundTrip [in mathcomp_eulerian.reflection]
AssembleUnique [in mathcomp_eulerian.reflection]

B

Bridges [in mathcomp_eulerian.psi_descent_v2]

C

Cancellation [in mathcomp_eulerian.perm_compress]
CycleBasic [in mathcomp_eulerian.cycles]
CycleCountInsertAfter [in mathcomp_eulerian.stirling_fiber]

D

Descent [in mathcomp_eulerian.descent]
DescentDrop [in mathcomp_eulerian.descent]
DescentReverse [in mathcomp_eulerian.descent]
DescentSplit [in mathcomp_eulerian.reflection]
DescentSplitRight [in mathcomp_eulerian.reflection]
DescentTranslate [in mathcomp_eulerian.reflection]
DescentTranslateRight [in mathcomp_eulerian.reflection]
DesInsertMax [in mathcomp_eulerian.eulerian]
DropPerm [in mathcomp_eulerian.perm_compress]

E

Egf [in mathcomp_fps.fps_egf]
Equidistribution [in mathcomp_eulerian.foata]
Equidistribution.FoataPerm [in mathcomp_eulerian.foata]
EulerianBasic [in mathcomp_eulerian.eulerian]
ExistenceLB [in mathcomp_eulerian.altsub]
ExtractMax [in mathcomp_eulerian.eulerian]

F

FoataBlocks [in mathcomp_eulerian.beta_omega]
FpsComp [in mathcomp_fps.fps_comp]
FpsCompUnit [in mathcomp_fps.fps_comp]
FpsDeriv [in mathcomp_fps.fps_deriv]
FpsDerivChar0 [in mathcomp_fps.fps_deriv]
FpsExpLog [in mathcomp_fps.fps_explog]
FpsExt [in mathcomp_fps.fps]
FpsOde [in mathcomp_fps.fps_ode]
FpsRing [in mathcomp_fps.fps]
FpsUnitRing [in mathcomp_fps.fps]
FpsZmod [in mathcomp_fps.fps]

G

Geometric [in mathcomp_fps.fps]
GeomPowers [in mathcomp_fps.fps_ogf]

H

hb_instance_4.hb_instance_4 [in mathcomp_fps.fps]
hb_instance_1.hb_instance_1 [in mathcomp_fps.fps]
H1 [in mathcomp_eulerian.cycles_rec]

I

ImageLeft [in mathcomp_eulerian.reflection]
ImageRight [in mathcomp_eulerian.reflection]
InnerReindexBij [in mathcomp_eulerian.reflection]
InsertAfter [in mathcomp_eulerian.stirling_fiber]
InsertExtractBij [in mathcomp_eulerian.eulerian]
InsertMax [in mathcomp_eulerian.eulerian]
InterTurn [in mathcomp_eulerian.altsub]
Inversions [in mathcomp_eulerian.inversions]
InvInsertMax [in mathcomp_eulerian.qfact]
InvMajBoundsRev [in mathcomp_eulerian.inversions]

L

LiftOrd [in mathcomp_eulerian.ordinal_reindex]
LiftPerm [in mathcomp_eulerian.perm_compress]
LowerBound [in mathcomp_eulerian.altsub]

M

MajorIndex [in mathcomp_eulerian.inversions]
MaxAlternation [in mathcomp_eulerian.altsub]
MMTree [in mathcomp_eulerian.mmtree]

P

PermOfLeft [in mathcomp_eulerian.reflection]
PermOfRight [in mathcomp_eulerian.reflection]
PhaseA [in mathcomp_eulerian.reflection]
PhaseARight [in mathcomp_eulerian.reflection]
PhaseB [in mathcomp_eulerian.reflection]
PickSeqFull [in mathcomp_eulerian.altsub]
PolyFps [in mathcomp_fps.fps]

S

SeqToPerm [in mathcomp_eulerian.perm_seq_basics]
SignPerm [in mathcomp_eulerian.altsub]
SlotInterval [in mathcomp_eulerian.altsub]

T

Trig [in mathcomp_fps.fps_trig]
TurnDefs [in mathcomp_eulerian.altsub]
TurnLemmas [in mathcomp_eulerian.altsub]

U

UnliftOrd [in mathcomp_eulerian.ordinal_reindex]
UpperBound [in mathcomp_eulerian.altsub]
UpperBoundAssembly [in mathcomp_eulerian.altsub]
UpperBoundChain [in mathcomp_eulerian.altsub]

---

Abbreviation Index

Q

qpow [in mathcomp_eulerian.qeul]

S

sigma [in mathcomp_eulerian.stirling_fiber]

other

σ [in mathcomp_eulerian.qfact]

---

Definition Index

A

all_D_transitions [in mathcomp_eulerian.psi_cdindex_support_defs]
alt_desc_set [in mathcomp_eulerian.beta_swap]
alt_321_sub [in mathcomp_eulerian.altsub]
alt_31425 [in mathcomp_eulerian.altsub]
alt_3142 [in mathcomp_eulerian.altsub]
alt_321 [in mathcomp_eulerian.altsub]
alt_312 [in mathcomp_eulerian.altsub]
alt_aux [in mathcomp_eulerian.altsub]
andre_target [in mathcomp_eulerian.reflection]
apply_psis [in mathcomp_eulerian.psi_cdindex_defs]
asc [in mathcomp_eulerian.descent]
assemble_perm [in mathcomp_eulerian.reflection]
assemble_fun [in mathcomp_eulerian.reflection]
as_perm [in mathcomp_eulerian.altsub]
as_perm_max [in mathcomp_eulerian.altsub]

B

beta [in mathcomp_eulerian.beta]
block_right [in mathcomp_eulerian.beta_omega]
block_left [in mathcomp_eulerian.beta_omega]
bwdAss [in mathcomp_eulerian.reflection]

C

card_image_left_eq [in mathcomp_eulerian.reflection]
castL [in mathcomp_eulerian.reflection]
castR [in mathcomp_eulerian.reflection]
cast_to_subj [in mathcomp_eulerian.reflection]
cast_to_j [in mathcomp_eulerian.reflection]
cde_sind [in mathcomp_eulerian.psi_cdindex_defs]
cde_rec [in mathcomp_eulerian.psi_cdindex_defs]
cde_ind [in mathcomp_eulerian.psi_cdindex_defs]
cde_rect [in mathcomp_eulerian.psi_cdindex_defs]
cde_offset [in mathcomp_eulerian.psi_cdindex_support_defs]
cde_total_width [in mathcomp_eulerian.psi_cdindex_support_defs]
cde_width [in mathcomp_eulerian.psi_cdindex_support_defs]
char_mono [in mathcomp_eulerian.psi_cdindex_defs]
check_fact3 [in mathcomp_eulerian.psi_cdindex_core]
check_sw_5_2 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_1 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_0 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_4_1 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_4_0 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_3_0 [in mathcomp_eulerian.psi_cdindex_witness]
check_strict_witness [in mathcomp_eulerian.psi_cdindex_witness]
classify_vertex_cde [in mathcomp_eulerian.psi_cdindex_defs]
class_map [in mathcomp_eulerian.perm_seq_bridge]
coinv_set [in mathcomp_eulerian.inversions]
compl_perm [in mathcomp_eulerian.beta_swap]
cosf [in mathcomp_fps.fps_trig]
count_lt [in mathcomp_eulerian.foata]
count_gt [in mathcomp_eulerian.foata]
cross_inv [in mathcomp_eulerian.foata]
cycle_count [in mathcomp_eulerian.cycles]
cyc_first_to_back [in mathcomp_eulerian.foata]
cyc_last_to_front [in mathcomp_eulerian.foata]

D

des [in mathcomp_eulerian.descent]
descent_psi_LR_swap1_ex [in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap2_ex [in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_remove_ex [in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_add_ex [in mathcomp_eulerian.psi_descent_thms]
descent_to_bvec [in mathcomp_eulerian.perm_seq_basics]
descent_set [in mathcomp_eulerian.descent]
descent_right_part_R [in mathcomp_eulerian.reflection]
descent_right_part [in mathcomp_eulerian.reflection]
descent_boundary_part [in mathcomp_eulerian.reflection]
descent_left_part [in mathcomp_eulerian.reflection]
drop_perm [in mathcomp_eulerian.perm_compress]
drop_fun [in mathcomp_eulerian.perm_compress]
D_offsets [in mathcomp_eulerian.psi_cdindex_support_defs]

E

egf [in mathcomp_fps.fps_egf]
embed_desc_right [in mathcomp_eulerian.reflection]
embed_desc_left [in mathcomp_eulerian.reflection]
embed_right [in mathcomp_eulerian.reflection]
embed_left [in mathcomp_eulerian.reflection]
endpoint_next_has_left_child_ex2 [in mathcomp_eulerian.psi_cdindex_tree]
endpoint_next_has_left_child_ex [in mathcomp_eulerian.psi_cdindex_tree]
euler [in mathcomp_eulerian.reflection]
eulerA [in mathcomp_eulerian.reflection]
eulerian [in mathcomp_eulerian.eulerian]
euler_egf [in mathcomp_eulerian.stanley_egf]
euler_rec_n2_via [in mathcomp_eulerian.reflection]
euler_rec_n1_via [in mathcomp_eulerian.reflection]
euler_rec_n0_direct [in mathcomp_eulerian.reflection]
euler_rec_n0 [in mathcomp_eulerian.reflection]
eul_pol [in mathcomp_eulerian.qeul]
exactly_one_descent_LR_ex [in mathcomp_eulerian.psi_descent_v2]
expand_cde [in mathcomp_eulerian.psi_cdindex_defs]
expf [in mathcomp_fps.fps_trig]
extract_max_perm [in mathcomp_eulerian.eulerian]
extract_max_fun [in mathcomp_eulerian.eulerian]
ex_roundtrip_compute [in mathcomp_eulerian.mmtree]
ex_roundtrip [in mathcomp_eulerian.mmtree]
ex_nontrivial [in mathcomp_eulerian.mmtree]
ex_seq [in mathcomp_eulerian.mmtree]

F

fact3_ex_213 [in mathcomp_eulerian.psi_cdindex_support]
fact3_ex_315426 [in mathcomp_eulerian.psi_cdindex_support]
find_ss [in mathcomp_eulerian.perm_seq_bridge]
flip_count [in mathcomp_eulerian.altsub]
foata [in mathcomp_eulerian.foata]
foata_perm [in mathcomp_eulerian.foata]
foata_inv [in mathcomp_eulerian.foata]
foata_inv_aux [in mathcomp_eulerian.foata]
foata_step_undo [in mathcomp_eulerian.foata]
foata_step [in mathcomp_eulerian.foata]
fps_log [in mathcomp_fps.fps_explog]
fps_exp [in mathcomp_fps.fps_explog]
fps_l [in mathcomp_fps.fps_explog]
fps_e [in mathcomp_fps.fps_explog]
fps_prim [in mathcomp_fps.fps_deriv]
fps_deriv [in mathcomp_fps.fps_deriv]
fps_comp [in mathcomp_fps.fps_comp]
fps_geom [in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComUnitAlgebra [in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComUnitRing [in mathcomp_fps.fps]
fps_fps__canonical__GRing_UnitAlgebra [in mathcomp_fps.fps]
fps_fps__canonical__GRing_UnitRing [in mathcomp_fps.fps]
fps_inv [in mathcomp_fps.fps]
fps_unit [in mathcomp_fps.fps]
fps_inv_coef [in mathcomp_fps.fps]
fps_poly_fps__canonical__GRing_RMorphism [in mathcomp_fps.fps]
fps_poly_fps__canonical__Algebra_Additive [in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComAlgebra [in mathcomp_fps.fps]
fps_fps__canonical__GRing_Algebra [in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComSemiAlgebra [in mathcomp_fps.fps]
fps_fps__canonical__GRing_SemiAlgebra [in mathcomp_fps.fps]
fps_fps__canonical__GRing_Lalgebra [in mathcomp_fps.fps]
fps_fps__canonical__GRing_LSemiAlgebra [in mathcomp_fps.fps]
fps_fps__canonical__GRing_Lmodule [in mathcomp_fps.fps]
fps_fps__canonical__GRing_LSemiModule [in mathcomp_fps.fps]
fps_scale [in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComNzRing [in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComNzSemiRing [in mathcomp_fps.fps]
fps_fps__canonical__GRing_NzRing [in mathcomp_fps.fps]
fps_fps__canonical__GRing_NzSemiRing [in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComPzRing [in mathcomp_fps.fps]
fps_fps__canonical__GRing_ComPzSemiRing [in mathcomp_fps.fps]
fps_fps__canonical__GRing_PzRing [in mathcomp_fps.fps]
fps_fps__canonical__GRing_PzSemiRing [in mathcomp_fps.fps]
fps_trunc [in mathcomp_fps.fps]
fps_mul [in mathcomp_fps.fps]
fps_one [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_Zmodule [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_Nmodule [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_AddUMagma [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_BaseZmodule [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_ChoiceBaseAddUMagma [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_BaseAddUMagma [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_AddSemigroup [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_AddMagma [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_ChoiceBaseAddMagma [in mathcomp_fps.fps]
fps_fps__canonical__Algebra_BaseAddMagma [in mathcomp_fps.fps]
fps_opp [in mathcomp_fps.fps]
fps_add [in mathcomp_fps.fps]
fps_zero [in mathcomp_fps.fps]
fps_fps__canonical__choice_Choice [in mathcomp_fps.fps]
fps_fps__canonical__eqtype_Equality [in mathcomp_fps.fps]
fwdAss [in mathcomp_eulerian.reflection]

G

GRing_ComNzRing_hasMulInverse__to__GRing_NzRing_hasMulInverse [in mathcomp_fps.fps]
GRing_isZmodMorphism__to__Algebra_isNmodMorphism [in mathcomp_fps.fps]
GRing_Lalgebra_isAlgebra__to__GRing_LSemiAlgebra_isSemiAlgebra [in mathcomp_fps.fps]
GRing_Lmodule_isLalgebra__to__GRing_LSemiModule_isLSemiAlgebra [in mathcomp_fps.fps]
GRing_Zmodule_isLmodule__to__GRing_Nmodule_isLSemiModule [in mathcomp_fps.fps]
GRing_Zmodule_isComNzRing__to__GRing_PzSemiRing_isNonZero [in mathcomp_fps.fps]
GRing_Zmodule_isComNzRing__to__GRing_Nmodule_isPzSemiRing [in mathcomp_fps.fps]
GRing_Zmodule_isComNzRing__to__GRing_PzSemiRing_hasCommutativeMul [in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_hasZero [in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_BaseAddUMagma_isAddUMagma [in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_BaseAddMagma_isAddMagma [in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_AddMagma_isAddSemigroup [in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_hasAdd [in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_BaseZmoduleNmodule_isZmodule [in mathcomp_fps.fps]
GRing_isZmodule__to__Algebra_hasOpp [in mathcomp_fps.fps]

H

has_transition [in mathcomp_eulerian.psi_cdindex_support_defs]
has_left_child_t [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_psi_ex [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_true [in mathcomp_eulerian.psi_descent_v2]
has_left_child_false [in mathcomp_eulerian.psi_descent_v2]
has_left_child [in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel [in mathcomp_eulerian.psi_descent_v2]
HB_unnamed_mixin_45 [in mathcomp_fps.fps]
HB_unnamed_factory_43 [in mathcomp_fps.fps]
HB_unnamed_factory_41 [in mathcomp_fps.fps]
HB_unnamed_mixin_40 [in mathcomp_fps.fps]
HB_unnamed_factory_38 [in mathcomp_fps.fps]
HB_unnamed_mixin_37 [in mathcomp_fps.fps]
HB_unnamed_factory_35 [in mathcomp_fps.fps]
HB_unnamed_mixin_34 [in mathcomp_fps.fps]
HB_unnamed_factory_32 [in mathcomp_fps.fps]
HB_unnamed_mixin_31 [in mathcomp_fps.fps]
HB_unnamed_factory_29 [in mathcomp_fps.fps]
HB_unnamed_mixin_28 [in mathcomp_fps.fps]
HB_unnamed_mixin_27 [in mathcomp_fps.fps]
HB_unnamed_mixin_26 [in mathcomp_fps.fps]
HB_unnamed_factory_22 [in mathcomp_fps.fps]
HB_unnamed_mixin_21 [in mathcomp_fps.fps]
HB_unnamed_mixin_20 [in mathcomp_fps.fps]
HB_unnamed_mixin_19 [in mathcomp_fps.fps]
HB_unnamed_mixin_18 [in mathcomp_fps.fps]
HB_unnamed_mixin_17 [in mathcomp_fps.fps]
HB_unnamed_mixin_16 [in mathcomp_fps.fps]
HB_unnamed_mixin_15 [in mathcomp_fps.fps]
HB_unnamed_factory_7 [in mathcomp_fps.fps]
HB_unnamed_factory_5 [in mathcomp_fps.fps]
HB_unnamed_factory_2 [in mathcomp_fps.fps]

I

image_right [in mathcomp_eulerian.reflection]
image_left [in mathcomp_eulerian.reflection]
insert_max_perm [in mathcomp_eulerian.eulerian]
insert_max_fun [in mathcomp_eulerian.eulerian]
insert_after [in mathcomp_eulerian.stirling_fiber]
insert_after_fun [in mathcomp_eulerian.stirling_fiber]
internal_vertices [in mathcomp_eulerian.psi_cdindex_defs]
inv [in mathcomp_eulerian.inversions]
inv_set [in mathcomp_eulerian.inversions]
inv_seq [in mathcomp_eulerian.foata]
inv_pref [in mathcomp_fps.fps]
is_internal [in mathcomp_eulerian.psi_cdindex_defs]
is_alt_bool [in mathcomp_eulerian.altsub]
is_alt_bool_aux [in mathcomp_eulerian.altsub]
is_alt [in mathcomp_eulerian.altsub]
is_turn [in mathcomp_eulerian.altsub]
is_internal_t [in mathcomp_eulerian.psi_cdindex_tree]
is_D_letter [in mathcomp_eulerian.psi_cdindex_witness]
is_descent_seq_ex [in mathcomp_eulerian.psi_descent_v2]
is_inv [in mathcomp_eulerian.inversions]
is_descent_seq [in mathcomp_eulerian.perm_seq_basics]
is_desc_seq [in mathcomp_eulerian.foata]
is_descent [in mathcomp_eulerian.descent]

L

left_ok [in mathcomp_eulerian.beta_omega]
leqj [in mathcomp_eulerian.reflection]
leqj_n1 [in mathcomp_eulerian.reflection]
leq_seqb [in mathcomp_eulerian.psi_cdindex_defs]
lift_perm [in mathcomp_eulerian.perm_compress]
lift_fun [in mathcomp_eulerian.perm_compress]
LR_pred_is_endpoint_ex3 [in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_ex2 [in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_ex [in mathcomp_eulerian.psi_cdindex_tree]

M

maj [in mathcomp_eulerian.inversions]
maj_seq [in mathcomp_eulerian.foata]
max_pos [in mathcomp_eulerian.psi_core]
min_pos [in mathcomp_eulerian.mmtree]
mmtree_shape [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_fuel [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_of_seq [in mathcomp_eulerian.mmtree]
mmtree_of_seq_fuel [in mathcomp_eulerian.mmtree]
mmtree_to_seq [in mathcomp_eulerian.mmtree]
mmtree_sind [in mathcomp_eulerian.mmtree]
mmtree_rec [in mathcomp_eulerian.mmtree]
mmtree_ind [in mathcomp_eulerian.mmtree]
mmtree_rect [in mathcomp_eulerian.mmtree]
mmtree_of_seq_mm [in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm_fuel [in mathcomp_eulerian.psi_core]
mm_pos [in mathcomp_eulerian.psi_core]

O

omega_set [in mathcomp_eulerian.beta_omega]
omega_seq [in mathcomp_eulerian.psi_cdindex_witness]
omega_seq_local [in mathcomp_eulerian.beta_bridge]
onesubX_pow_t [in mathcomp_eulerian.stirling_egf]

P

perm_seq [in mathcomp_eulerian.altsub]
perm_to_seq [in mathcomp_eulerian.perm_seq_basics]
perm_right [in mathcomp_eulerian.reflection]
perm_right_fun [in mathcomp_eulerian.reflection]
perm_left [in mathcomp_eulerian.reflection]
perm_left_fun [in mathcomp_eulerian.reflection]
phi_w [in mathcomp_eulerian.psi_cdindex_defs]
phi_w_support_ex1 [in mathcomp_eulerian.psi_cdindex_witness]
phi'_w [in mathcomp_eulerian.psi_cdindex_defs]
pick_seq [in mathcomp_eulerian.altsub]
poly_fps [in mathcomp_fps.fps]
post_window_extremum_ex [in mathcomp_eulerian.psi_descent_v2]
pos_seq [in mathcomp_eulerian.altsub]
powerset_internal [in mathcomp_eulerian.psi_cdindex_defs]
pow_ogf [in mathcomp_eulerian.stanley_ogf]
pre_window_gt_min_ex [in mathcomp_eulerian.psi_descent_v2]
psi [in mathcomp_eulerian.psi_core]
psi_comm_nontrivial [in mathcomp_eulerian.psi_comm]
psi_comm_ex [in mathcomp_eulerian.psi_comm]
psi_comm_nested_ex [in mathcomp_eulerian.psi_comm]
psi_comm_disjoint_ex [in mathcomp_eulerian.psi_comm]
psi_involutive_ex [in mathcomp_eulerian.psi_core]
psi_nontrivial [in mathcomp_eulerian.psi_core]

Q

qbin [in mathcomp_eulerian.qbin]
q_eul_pol [in mathcomp_eulerian.qeul]
q_eulerian [in mathcomp_eulerian.qeul_rec]
q_fact [in mathcomp_eulerian.qfact]
q_int [in mathcomp_eulerian.qfact]
q_pow_ogf [in mathcomp_eulerian.carlitz]
q_stair [in mathcomp_eulerian.carlitz]
q_onesub_prod [in mathcomp_eulerian.carlitz]
q1_subst [in mathcomp_eulerian.qeul]

R

rank_shift_interior_order_ex [in mathcomp_eulerian.psi_descent_v2]
rank_shift_seq [in mathcomp_eulerian.psi_core]
rank_left [in mathcomp_eulerian.reflection]
rev_perm [in mathcomp_eulerian.descent]
rev_perm_ord [in mathcomp_eulerian.descent]
right_ok [in mathcomp_eulerian.beta_omega]

S

secf [in mathcomp_fps.fps_trig]
seq_to_perm [in mathcomp_eulerian.perm_seq_basics]
seq_to_fun [in mathcomp_eulerian.perm_seq_basics]
set_is_alt [in mathcomp_eulerian.beta_swap]
set_to_seq [in mathcomp_eulerian.beta_bridge]
sign_seq [in mathcomp_eulerian.altsub]
sinf [in mathcomp_fps.fps_trig]
slot_iv [in mathcomp_eulerian.altsub]
split_blocks_inv [in mathcomp_eulerian.foata]
split_blocks_inv_aux [in mathcomp_eulerian.foata]
split_blocks [in mathcomp_eulerian.foata]
split_blocks_aux [in mathcomp_eulerian.foata]
split_pos [in mathcomp_eulerian.reflection]
stirling_egf [in mathcomp_eulerian.stirling_egf]
stirling_pol [in mathcomp_eulerian.stirling_egf]
stirling_c [in mathcomp_eulerian.cycles]
strict_witness_ex3 [in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_ex2 [in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_ex1 [in mathcomp_eulerian.psi_cdindex_witness]
sym_diff [in mathcomp_eulerian.beta_omega]
S_w_seq_ex4 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex3 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex2 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex1 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq [in mathcomp_eulerian.psi_cdindex_witness]

T

tanf [in mathcomp_fps.fps_trig]
tcs_12345 [in mathcomp_eulerian.altsub]
tcs_321 [in mathcomp_eulerian.altsub]
tcs_3142 [in mathcomp_eulerian.altsub]
tcs_312 [in mathcomp_eulerian.altsub]
toggle_at [in mathcomp_eulerian.beta_omega]
tree_props [in mathcomp_eulerian.psi_descent_v2]
turn_witness [in mathcomp_eulerian.altsub]
turn_inj [in mathcomp_eulerian.altsub]
turn_iv [in mathcomp_eulerian.altsub]
turn_count_seq [in mathcomp_eulerian.altsub]
turn_count [in mathcomp_eulerian.altsub]

U

uniq_adj [in mathcomp_eulerian.altsub]

V

valid_mm [in mathcomp_eulerian.psi_descent_v2]

W

wf_block [in mathcomp_eulerian.foata]
window_size_t [in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex3 [in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex2 [in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex1 [in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ancestor_ex [in mathcomp_eulerian.psi_comm]
window_trichotomy_ex [in mathcomp_eulerian.psi_core]
window_at [in mathcomp_eulerian.psi_core]
window_size [in mathcomp_eulerian.psi_core]
window_size_fuel [in mathcomp_eulerian.psi_core]
witness_perm [in mathcomp_eulerian.psi_cdindex_witness]

---

Record Index

F

fps [in mathcomp_fps.fps]

---

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

(1583 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

(4 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

(186 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

(49 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

(914 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

(5 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

(2 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

(1 entry)

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

(78 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

(3 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

(340 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

(1 entry)

---

This page has been generated by coqdoc