| 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 | (354 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 | (23 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 | (20 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 | (196 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (2 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 | (109 entries) |
Global Index
A
adj_coef_jacobi [lemma, in PrimeGapS1.CharPoly]adj_coef_trace [lemma, in PrimeGapS1.CharPoly]
adj_coef_formula [lemma, in PrimeGapS1.CharPoly]
adj_coef [definition, in PrimeGapS1.CharPoly]
all_empty [definition, in PrimeGapS1.IntMat]
all_rows_len_mmul [lemma, in PrimeGapS1.CharPoly]
all_rows_len_meye [lemma, in PrimeGapS1.CharPoly]
all_rows_len_meye_aux [lemma, in PrimeGapS1.CharPoly]
all_rows_len_mzero [lemma, in PrimeGapS1.CharPoly]
all_rows_len_mzero_aux [lemma, in PrimeGapS1.CharPoly]
all_rows_len_madd [lemma, in PrimeGapS1.CharPoly]
all_rows_len_mscale [lemma, in PrimeGapS1.CharPoly]
all_rows_len_to_at_least [lemma, in PrimeGapS1.CharPoly]
all_empty_false_of_Sk [lemma, in PrimeGapS1.CharPoly]
all_rows_at_least_tails [lemma, in PrimeGapS1.CharPoly]
all_rows_at_least [definition, in PrimeGapS1.CharPoly]
all_rows_len [definition, in PrimeGapS1.CharPoly]
all_match_M2Z_true [lemma, in PrimeGapS1.MaynardVerify]
all_match_M1Z_true [lemma, in PrimeGapS1.MaynardVerify.Def]
all_match_M2Z [definition, in PrimeGapS1.MaynardVerify.Def]
all_match_M1Z [definition, in PrimeGapS1.MaynardVerify.Def]
alpha [definition, in PrimeGapS1.MaynardSpec]
alphaZ [definition, in PrimeGapS1.MaynardSpec]
alphaZ_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
A_int [definition, in PrimeGapS1.Witness]
B
basis [definition, in PrimeGapS1.Witness]binQ [definition, in PrimeGapS1.MaynardFactQ]
binQ_factQ [lemma, in PrimeGapS1.MaynardSpecBridge]
binZ [definition, in PrimeGapS1.MaynardSpec]
binZ_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
bin_dvd_fact [lemma, in PrimeGapS1.MaynardSpecBridge]
C
canonical_basis_spec [lemma, in PrimeGapS1.MaynardBasis]canonical_basis [definition, in PrimeGapS1.MaynardBasis]
Cert [library]
CertRayleigh [library]
cff [definition, in PrimeGapS1.MaynardSpec]
cffZ [definition, in PrimeGapS1.MaynardSpec]
cffZ_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
CharPoly [library]
charpoly_int [definition, in PrimeGapS1.Witness]
charpoly_of_A_int [definition, in PrimeGapS1.Witness]
charpoly_of_A_int_bigZ [definition, in PrimeGapS1.Witness]
char_poly_int_correct [lemma, in PrimeGapS1.CharPoly]
char_poly_newton [lemma, in PrimeGapS1.CharPoly]
char_poly_int [definition, in PrimeGapS1.CharPoly]
compositions [definition, in PrimeGapS1.MaynardSpec]
compositionsZ [definition, in PrimeGapS1.MaynardSpec]
compositionsZ_eq_compositions [lemma, in PrimeGapS1.MaynardSpecBridge]
compositions_auxZ_eq [lemma, in PrimeGapS1.MaynardSpecBridge]
compositions_auxZ [definition, in PrimeGapS1.MaynardSpec]
compositions_aux [definition, in PrimeGapS1.MaynardSpec]
D
dblratZ [definition, in PrimeGapS1.MaynardSpec]dblratZ_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
Def [library]
dot_int [definition, in PrimeGapS1.IntMat]
D_q [definition, in PrimeGapS1.Witness]
D_A [definition, in PrimeGapS1.Witness]
D_M2 [definition, in PrimeGapS1.Witness]
D_M1 [definition, in PrimeGapS1.Witness]
D_M2_pos [lemma, in PrimeGapS1.Cert]
D_M1_pos [lemma, in PrimeGapS1.Cert]
E
eye_row [definition, in PrimeGapS1.IntMat]F
factQ [definition, in PrimeGapS1.MaynardFactQ]factQ_neq0 [lemma, in PrimeGapS1.MaynardFactQ]
factZ [definition, in PrimeGapS1.MaynardSpec]
factZ_factZ_pos [lemma, in PrimeGapS1.MaynardSpecBridge]
factZ_factZ_dvd [lemma, in PrimeGapS1.MaynardSpecBridge]
factZ_pos [lemma, in PrimeGapS1.MaynardSpecBridge]
factZ_dvd_double [lemma, in PrimeGapS1.MaynardSpecBridge]
factZ_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
factZ_eq_Z_of_nat [lemma, in PrimeGapS1.MaynardSpecBridge]
fact_dvd_fact [lemma, in PrimeGapS1.MaynardSpecBridge]
flatten_concat [lemma, in PrimeGapS1.MaynardSpecBridge]
flat_map_concat_map [lemma, in PrimeGapS1.MaynardSpecBridge]
FLRat [section, in PrimeGapS1.CharPoly]
FLRat.A [variable, in PrimeGapS1.CharPoly]
FLRat.n [variable, in PrimeGapS1.CharPoly]
fl_loop_eq_fl_state [lemma, in PrimeGapS1.CharPoly]
fl_divisibility_L2 [lemma, in PrimeGapS1.CharPoly]
fl_invariant_L2 [lemma, in PrimeGapS1.CharPoly]
fl_combined [lemma, in PrimeGapS1.CharPoly]
fl_c_rat_is_int [lemma, in PrimeGapS1.CharPoly]
fl_c_int_k_step [lemma, in PrimeGapS1.CharPoly]
fl_M_int_k_step [lemma, in PrimeGapS1.CharPoly]
fl_c_int_k_base [lemma, in PrimeGapS1.CharPoly]
fl_M_int_k_base [lemma, in PrimeGapS1.CharPoly]
fl_M_int_k_rows [lemma, in PrimeGapS1.CharPoly]
fl_M_int_k_dim [lemma, in PrimeGapS1.CharPoly]
fl_M_int_k_wf [lemma, in PrimeGapS1.CharPoly]
fl_loop_rat_is_char_poly_L2 [lemma, in PrimeGapS1.CharPoly]
fl_c_rat_eq_char_poly [lemma, in PrimeGapS1.CharPoly]
fl_trace_identity [lemma, in PrimeGapS1.CharPoly]
FL_CharPoly_Core.Hlead_cp [variable, in PrimeGapS1.CharPoly]
fl_M_expansion [lemma, in PrimeGapS1.CharPoly]
FL_CharPoly_Core.cp [variable, in PrimeGapS1.CharPoly]
FL_CharPoly_Core.B [variable, in PrimeGapS1.CharPoly]
FL_CharPoly_Core.n [variable, in PrimeGapS1.CharPoly]
FL_CharPoly_Core [section, in PrimeGapS1.CharPoly]
fl_c_rat [definition, in PrimeGapS1.CharPoly]
fl_M_rat [definition, in PrimeGapS1.CharPoly]
fl_loop_rat [definition, in PrimeGapS1.CharPoly]
fl_step_rat [definition, in PrimeGapS1.CharPoly]
fl_c_int_k [definition, in PrimeGapS1.CharPoly]
fl_M_int_k [definition, in PrimeGapS1.CharPoly]
fl_state [definition, in PrimeGapS1.CharPoly]
fl_loop [definition, in PrimeGapS1.CharPoly]
fold_left_qplus_den_pos [lemma, in PrimeGapS1.MaynardSpecBridge]
fold_left_pointwise_eq [lemma, in PrimeGapS1.MaynardSpecBridge]
fold_left_inner_to_map [lemma, in PrimeGapS1.MaynardSpecBridge]
fold_left_qplus_den_neq0 [lemma, in PrimeGapS1.MaynardSpecBridge]
fold_left_qplus_qfrac [lemma, in PrimeGapS1.MaynardSpecBridge]
fold_left_Zadd_sum [lemma, in PrimeGapS1.MaynardSpecBridge]
fold_left_Zadd_acc [lemma, in PrimeGapS1.MaynardSpecBridge]
forallb_seq_in [lemma, in PrimeGapS1.MaynardVerify.Def]
G
G_2 [definition, in PrimeGapS1.MaynardSpec]G2Z [definition, in PrimeGapS1.MaynardSpec]
G2Z_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
H
heads [definition, in PrimeGapS1.IntMat]I
inner_row_sum [lemma, in PrimeGapS1.MaynardSpecBridge]IntMat [library]
IntPoly [library]
intr_injective_rat [lemma, in PrimeGapS1.CharPoly]
iota_seq_eq [lemma, in PrimeGapS1.MaynardSpecBridge]
K
K1 [definition, in PrimeGapS1.MaynardSpec]K1n [definition, in PrimeGapS1.MaynardSpec]
K2 [definition, in PrimeGapS1.MaynardSpec]
K2n [definition, in PrimeGapS1.MaynardSpec]
L
length_eye_row [lemma, in PrimeGapS1.CharPoly]length_vadd [lemma, in PrimeGapS1.CharPoly]
length_vscale [lemma, in PrimeGapS1.CharPoly]
length_zrow [lemma, in PrimeGapS1.CharPoly]
length_mtrans_sq [lemma, in PrimeGapS1.CharPoly]
length_nth_mtrans_fuel [lemma, in PrimeGapS1.CharPoly]
length_mtrans_fuel_exact [lemma, in PrimeGapS1.CharPoly]
length_heads [lemma, in PrimeGapS1.CharPoly]
length_tails [lemma, in PrimeGapS1.CharPoly]
lift_bigZ [definition, in PrimeGapS1.Recompose]
M
madd [definition, in PrimeGapS1.IntMat]mat [definition, in PrimeGapS1.IntMat]
mat_get [definition, in PrimeGapS1.IntMat]
mat_dim [definition, in PrimeGapS1.IntMat]
mat_dim_madd_eq [lemma, in PrimeGapS1.CharPoly]
mat_dim_mmul_eq [lemma, in PrimeGapS1.CharPoly]
mat_dim_mscale_eq [lemma, in PrimeGapS1.CharPoly]
mat_int_to_rat_mmul [lemma, in PrimeGapS1.CharPoly]
mat_get_mmul_sq [lemma, in PrimeGapS1.CharPoly]
mat_int_to_rat_madd [lemma, in PrimeGapS1.CharPoly]
mat_get_madd [lemma, in PrimeGapS1.CharPoly]
mat_int_to_rat_meye [lemma, in PrimeGapS1.CharPoly]
mat_get_meye_neq [lemma, in PrimeGapS1.CharPoly]
mat_get_meye_eq [lemma, in PrimeGapS1.CharPoly]
mat_int_to_rat_mscale [lemma, in PrimeGapS1.CharPoly]
mat_get_mscale [lemma, in PrimeGapS1.CharPoly]
mat_int_to_rat_mzero [lemma, in PrimeGapS1.CharPoly]
mat_get_mzero [lemma, in PrimeGapS1.CharPoly]
mat_dim_mzero [lemma, in PrimeGapS1.CharPoly]
mat_dim_meye [lemma, in PrimeGapS1.CharPoly]
mat_int_to_rat [definition, in PrimeGapS1.CharPoly]
mat_vec_mul [definition, in PrimeGapS1.CertRayleigh]
MaynardBasis [library]
MaynardFactQ [library]
MaynardSpec [library]
MaynardSpecBridge [library]
MaynardVerify [library]
maynard_M105_certified_rayleigh [lemma, in PrimeGapS1.CertRayleigh]
maynard_basis_uniq [lemma, in PrimeGapS1.MaynardBasis]
maynard_basis_spec [lemma, in PrimeGapS1.MaynardBasis]
maynard_basis_perm_canonical [lemma, in PrimeGapS1.MaynardBasis]
maynard_basis_eq_witness [lemma, in PrimeGapS1.MaynardBasis]
maynard_basis_size [lemma, in PrimeGapS1.MaynardBasis]
maynard_basis [definition, in PrimeGapS1.MaynardBasis]
meye [definition, in PrimeGapS1.IntMat]
meye_aux [definition, in PrimeGapS1.IntMat]
meye_aux_len [lemma, in PrimeGapS1.CharPoly]
mmul [definition, in PrimeGapS1.IntMat]
mscale [definition, in PrimeGapS1.IntMat]
mtrace [definition, in PrimeGapS1.IntMat]
mtrace_aux [definition, in PrimeGapS1.IntMat]
mtrace_int_to_rat [lemma, in PrimeGapS1.CharPoly]
mtrace_aux_diag_sum [lemma, in PrimeGapS1.CharPoly]
mtrans [definition, in PrimeGapS1.IntMat]
mtrans_fuel [definition, in PrimeGapS1.IntMat]
mzero [definition, in PrimeGapS1.IntMat]
mzero_aux [definition, in PrimeGapS1.IntMat]
mzero_aux_len [lemma, in PrimeGapS1.CharPoly]
M1_int_cols [lemma, in PrimeGapS1.CertRayleigh]
M1_int_rows [lemma, in PrimeGapS1.CertRayleigh]
M1_int [definition, in PrimeGapS1.Witness]
m1_num_den_at_den_pos [lemma, in PrimeGapS1.MaynardSpecBridge]
m1_num_den_den_pos [lemma, in PrimeGapS1.MaynardSpecBridge]
M1_spec_rat_eq [lemma, in PrimeGapS1.MaynardSpecBridge]
m1_num_den_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
m1_num_den_at [definition, in PrimeGapS1.MaynardSpec]
m1_num_den [definition, in PrimeGapS1.MaynardSpec]
M1_spec_ij [definition, in PrimeGapS1.MaynardSpec]
M1_entry [definition, in PrimeGapS1.MaynardSpec]
M1_spec_eq_int [lemma, in PrimeGapS1.Cert]
M1_entry_match_in_grid [lemma, in PrimeGapS1.MaynardVerify.Def]
M1_entry_matchZ_E [lemma, in PrimeGapS1.MaynardVerify.Def]
M1_entry_matchZ [definition, in PrimeGapS1.MaynardVerify.Def]
m1_den [definition, in PrimeGapS1.MaynardVerify.Def]
m1_num [definition, in PrimeGapS1.MaynardVerify.Def]
M2_check_rows_0_6 [lemma, in PrimeGapS1.MaynardVerify.M2_0]
M2_int_cols [lemma, in PrimeGapS1.CertRayleigh]
M2_int_rows [lemma, in PrimeGapS1.CertRayleigh]
M2_check_rows_28_34 [lemma, in PrimeGapS1.MaynardVerify.M2_4]
M2_check_rows_35_41 [lemma, in PrimeGapS1.MaynardVerify.M2_5]
M2_int [definition, in PrimeGapS1.Witness]
M2_check_rows_14_20 [lemma, in PrimeGapS1.MaynardVerify.M2_2]
M2_entry_match_in_grid [lemma, in PrimeGapS1.MaynardVerify]
M2_check_rows_app [lemma, in PrimeGapS1.MaynardVerify]
m2_num_den_at_den_pos [lemma, in PrimeGapS1.MaynardSpecBridge]
m2_num_den_den_pos [lemma, in PrimeGapS1.MaynardSpecBridge]
m2_term_num_den_den_pos [lemma, in PrimeGapS1.MaynardSpecBridge]
M2_spec_rat_eq [lemma, in PrimeGapS1.MaynardSpecBridge]
m2_num_den_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
m2_outer_qfrac [lemma, in PrimeGapS1.MaynardSpecBridge]
m2_term_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
M2_check_rows_21_27 [lemma, in PrimeGapS1.MaynardVerify.M2_3]
M2_check_rows_7_13 [lemma, in PrimeGapS1.MaynardVerify.M2_1]
m2_num_den_at [definition, in PrimeGapS1.MaynardSpec]
m2_num_den [definition, in PrimeGapS1.MaynardSpec]
m2_term_num_den [definition, in PrimeGapS1.MaynardSpec]
M2_spec_ij [definition, in PrimeGapS1.MaynardSpec]
M2_entry [definition, in PrimeGapS1.MaynardSpec]
M2_spec_eq_int [lemma, in PrimeGapS1.Cert]
M2_entry_matchZ_E [lemma, in PrimeGapS1.MaynardVerify.Def]
M2_check_rows [definition, in PrimeGapS1.MaynardVerify.Def]
M2_entry_matchZ [definition, in PrimeGapS1.MaynardVerify.Def]
m2_den [definition, in PrimeGapS1.MaynardVerify.Def]
m2_num [definition, in PrimeGapS1.MaynardVerify.Def]
M2_5 [library]
M2_4 [library]
M2_2 [library]
M2_1 [library]
M2_0 [library]
M2_3 [library]
N
Nat_leb_leqP [lemma, in PrimeGapS1.MaynardSpecBridge]nth_Z [definition, in PrimeGapS1.IntMat]
nth_nth_mtrans_sq [lemma, in PrimeGapS1.CharPoly]
nth_mtrans_length_sq [lemma, in PrimeGapS1.CharPoly]
nth_nth_mtrans_fuel [lemma, in PrimeGapS1.CharPoly]
nth_heads [lemma, in PrimeGapS1.CharPoly]
nth_tails [lemma, in PrimeGapS1.CharPoly]
nth_madd [lemma, in PrimeGapS1.CharPoly]
nth_Z_vadd [lemma, in PrimeGapS1.CharPoly]
nth_meye_aux [lemma, in PrimeGapS1.CharPoly]
nth_eye_row_neq [lemma, in PrimeGapS1.CharPoly]
nth_eye_row_eq [lemma, in PrimeGapS1.CharPoly]
nth_map_vscale [lemma, in PrimeGapS1.CharPoly]
nth_Z_vscale [lemma, in PrimeGapS1.CharPoly]
nth_mzero_aux_is_zrow [lemma, in PrimeGapS1.CharPoly]
nth_Z_zrow [lemma, in PrimeGapS1.CharPoly]
num_M2 [definition, in PrimeGapS1.CertRayleigh]
num_M1 [definition, in PrimeGapS1.CertRayleigh]
P
peval_at_rat [definition, in PrimeGapS1.IntPoly]peval_at_rat_aux [definition, in PrimeGapS1.IntPoly]
plead [definition, in PrimeGapS1.IntPoly]
plead_aux [definition, in PrimeGapS1.IntPoly]
pol [definition, in PrimeGapS1.IntPoly]
pol_to_polyrat [definition, in PrimeGapS1.CharPoly]
prod_dblratZ_to_rat [lemma, in PrimeGapS1.MaynardSpecBridge]
prod_dblratZ [definition, in PrimeGapS1.MaynardSpec]
Q
qfrac [definition, in PrimeGapS1.MaynardSpecBridge]qfrac_eq_div [lemma, in PrimeGapS1.MaynardSpecBridge]
qfrac_init [lemma, in PrimeGapS1.MaynardSpecBridge]
qfrac_qplus [lemma, in PrimeGapS1.MaynardSpecBridge]
qfrac_qmul [lemma, in PrimeGapS1.MaynardSpecBridge]
qfrac_pair [lemma, in PrimeGapS1.MaynardSpecBridge]
qmul [definition, in PrimeGapS1.MaynardSpec]
qplus [definition, in PrimeGapS1.MaynardSpec]
qplus_den_pos [lemma, in PrimeGapS1.MaynardSpecBridge]
quad [definition, in PrimeGapS1.CertRayleigh]
QuadBridge [section, in PrimeGapS1.CertRayleigh]
QuadBridge.HM_cols [variable, in PrimeGapS1.CertRayleigh]
QuadBridge.HM_rows [variable, in PrimeGapS1.CertRayleigh]
QuadBridge.Hv_len [variable, in PrimeGapS1.CertRayleigh]
QuadBridge.M [variable, in PrimeGapS1.CertRayleigh]
quad_M2_spec_eq_Z [lemma, in PrimeGapS1.CertRayleigh]
quad_M1_spec_eq_Z [lemma, in PrimeGapS1.CertRayleigh]
quad_spec_eq_Z [lemma, in PrimeGapS1.CertRayleigh]
quad_cell_identity [lemma, in PrimeGapS1.CertRayleigh]
quad_M2_spec [abbreviation, in PrimeGapS1.CertRayleigh]
quad_M1_spec [abbreviation, in PrimeGapS1.CertRayleigh]
quad_spec [definition, in PrimeGapS1.CertRayleigh]
R
RayleighLift [section, in PrimeGapS1.CertRayleigh]RayleighLift.a1Z [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.a2Z [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.d1Z [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.d2Z [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.Ha1 [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.Ha2 [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.Hcmp [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.Hd1 [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.Hd2 [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.Hv [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.q1 [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.q2 [variable, in PrimeGapS1.CertRayleigh]
RayleighLift.v [variable, in PrimeGapS1.CertRayleigh]
rayleigh_lt_main [lemma, in PrimeGapS1.CertRayleigh]
rayleigh_lift_generic [lemma, in PrimeGapS1.CertRayleigh]
rayleigh_witness_holds_rat [lemma, in PrimeGapS1.CertRayleigh]
rayleigh_witness_holds [lemma, in PrimeGapS1.CertRayleigh]
rayleigh_witness_M1_positive [lemma, in PrimeGapS1.CertRayleigh]
Recompose [library]
row_dot [definition, in PrimeGapS1.CertRayleigh]
S
seq_split_42 [lemma, in PrimeGapS1.MaynardVerify]seq_map_eq [lemma, in PrimeGapS1.MaynardSpecBridge]
T
tails [definition, in PrimeGapS1.IntMat]V
vadd [definition, in PrimeGapS1.IntMat]vscale [definition, in PrimeGapS1.IntMat]
v_den_neq0_rat [lemma, in PrimeGapS1.CertRayleigh]
v_num_length [lemma, in PrimeGapS1.CertRayleigh]
v_rat [definition, in PrimeGapS1.CertRayleigh]
v_den_pos [lemma, in PrimeGapS1.CertRayleigh]
v_num [definition, in PrimeGapS1.CertRayleigh]
v_den [definition, in PrimeGapS1.CertRayleigh]
v_witness [definition, in PrimeGapS1.Witness_Rayleigh]
W
Witness [library]Witness_Rayleigh [library]
Z
zrow [definition, in PrimeGapS1.IntMat]Z_rem_of_intr_eq [lemma, in PrimeGapS1.CharPoly]
Z_to_int_injective [lemma, in PrimeGapS1.CharPoly]
Z_to_int_1_rat [lemma, in PrimeGapS1.CharPoly]
Z_to_int_of_nat [lemma, in PrimeGapS1.CharPoly]
Z_div_exact_rat [lemma, in PrimeGapS1.CharPoly]
Z_to_int_opp [lemma, in PrimeGapS1.CharPoly]
Z_to_int_dot_int_sum [lemma, in PrimeGapS1.CharPoly]
Z_to_int_add [lemma, in PrimeGapS1.CharPoly]
Z_pos_sub_int [lemma, in PrimeGapS1.CharPoly]
Z_to_int_mul [lemma, in PrimeGapS1.CharPoly]
Z_to_int_pos_pos [lemma, in PrimeGapS1.CharPoly]
Z_to_int_neg_pos [lemma, in PrimeGapS1.CharPoly]
Z_to_int_1 [lemma, in PrimeGapS1.CharPoly]
Z_to_int_0 [lemma, in PrimeGapS1.CharPoly]
Z_to_int [definition, in PrimeGapS1.CharPoly]
Z_to_int_m2_term_den_neq0 [lemma, in PrimeGapS1.MaynardSpecBridge]
Z_to_int_alphaZ_den_neq0 [lemma, in PrimeGapS1.MaynardSpecBridge]
Z_to_int_qmul_den_neq0 [lemma, in PrimeGapS1.MaynardSpecBridge]
Z_to_int_qplus_den_neq0 [lemma, in PrimeGapS1.MaynardSpecBridge]
Z_to_int_factZ_neq0 [lemma, in PrimeGapS1.MaynardSpecBridge]
Z_to_int_div_exact [lemma, in PrimeGapS1.MaynardSpecBridge]
Z_to_int_pos_rat_neq0 [lemma, in PrimeGapS1.MaynardSpecBridge]
Z_to_int_pos_neq0 [lemma, in PrimeGapS1.MaynardSpecBridge]
Z_of_nat_dvd [lemma, in PrimeGapS1.MaynardSpecBridge]
Z_to_int_factZ [lemma, in PrimeGapS1.MaynardSpecBridge]
Z2rat [definition, in PrimeGapS1.MaynardSpecBridge]
Z2rat_lt [lemma, in PrimeGapS1.CertRayleigh]
Z2rat_pos [lemma, in PrimeGapS1.CertRayleigh]
Z2rat_quad_eq_sum [lemma, in PrimeGapS1.CertRayleigh]
Z2rat_row_dot_eq_sum [lemma, in PrimeGapS1.CertRayleigh]
Z2rat_0 [lemma, in PrimeGapS1.CertRayleigh]
Z2rat_add [lemma, in PrimeGapS1.CertRayleigh]
Z2rat_mul [lemma, in PrimeGapS1.CertRayleigh]
Variable Index
F
FLRat.A [in PrimeGapS1.CharPoly]FLRat.n [in PrimeGapS1.CharPoly]
FL_CharPoly_Core.Hlead_cp [in PrimeGapS1.CharPoly]
FL_CharPoly_Core.cp [in PrimeGapS1.CharPoly]
FL_CharPoly_Core.B [in PrimeGapS1.CharPoly]
FL_CharPoly_Core.n [in PrimeGapS1.CharPoly]
Q
QuadBridge.HM_cols [in PrimeGapS1.CertRayleigh]QuadBridge.HM_rows [in PrimeGapS1.CertRayleigh]
QuadBridge.Hv_len [in PrimeGapS1.CertRayleigh]
QuadBridge.M [in PrimeGapS1.CertRayleigh]
R
RayleighLift.a1Z [in PrimeGapS1.CertRayleigh]RayleighLift.a2Z [in PrimeGapS1.CertRayleigh]
RayleighLift.d1Z [in PrimeGapS1.CertRayleigh]
RayleighLift.d2Z [in PrimeGapS1.CertRayleigh]
RayleighLift.Ha1 [in PrimeGapS1.CertRayleigh]
RayleighLift.Ha2 [in PrimeGapS1.CertRayleigh]
RayleighLift.Hcmp [in PrimeGapS1.CertRayleigh]
RayleighLift.Hd1 [in PrimeGapS1.CertRayleigh]
RayleighLift.Hd2 [in PrimeGapS1.CertRayleigh]
RayleighLift.Hv [in PrimeGapS1.CertRayleigh]
RayleighLift.q1 [in PrimeGapS1.CertRayleigh]
RayleighLift.q2 [in PrimeGapS1.CertRayleigh]
RayleighLift.v [in PrimeGapS1.CertRayleigh]
Library Index
C
CertCertRayleigh
CharPoly
D
DefI
IntMatIntPoly
M
MaynardBasisMaynardFactQ
MaynardSpec
MaynardSpecBridge
MaynardVerify
M2_5
M2_4
M2_2
M2_1
M2_0
M2_3
R
RecomposeW
WitnessWitness_Rayleigh
Lemma Index
A
adj_coef_jacobi [in PrimeGapS1.CharPoly]adj_coef_trace [in PrimeGapS1.CharPoly]
adj_coef_formula [in PrimeGapS1.CharPoly]
all_rows_len_mmul [in PrimeGapS1.CharPoly]
all_rows_len_meye [in PrimeGapS1.CharPoly]
all_rows_len_meye_aux [in PrimeGapS1.CharPoly]
all_rows_len_mzero [in PrimeGapS1.CharPoly]
all_rows_len_mzero_aux [in PrimeGapS1.CharPoly]
all_rows_len_madd [in PrimeGapS1.CharPoly]
all_rows_len_mscale [in PrimeGapS1.CharPoly]
all_rows_len_to_at_least [in PrimeGapS1.CharPoly]
all_empty_false_of_Sk [in PrimeGapS1.CharPoly]
all_rows_at_least_tails [in PrimeGapS1.CharPoly]
all_match_M2Z_true [in PrimeGapS1.MaynardVerify]
all_match_M1Z_true [in PrimeGapS1.MaynardVerify.Def]
alphaZ_to_rat [in PrimeGapS1.MaynardSpecBridge]
B
binQ_factQ [in PrimeGapS1.MaynardSpecBridge]binZ_to_rat [in PrimeGapS1.MaynardSpecBridge]
bin_dvd_fact [in PrimeGapS1.MaynardSpecBridge]
C
canonical_basis_spec [in PrimeGapS1.MaynardBasis]cffZ_to_rat [in PrimeGapS1.MaynardSpecBridge]
char_poly_int_correct [in PrimeGapS1.CharPoly]
char_poly_newton [in PrimeGapS1.CharPoly]
compositionsZ_eq_compositions [in PrimeGapS1.MaynardSpecBridge]
compositions_auxZ_eq [in PrimeGapS1.MaynardSpecBridge]
D
dblratZ_to_rat [in PrimeGapS1.MaynardSpecBridge]D_M2_pos [in PrimeGapS1.Cert]
D_M1_pos [in PrimeGapS1.Cert]
F
factQ_neq0 [in PrimeGapS1.MaynardFactQ]factZ_factZ_pos [in PrimeGapS1.MaynardSpecBridge]
factZ_factZ_dvd [in PrimeGapS1.MaynardSpecBridge]
factZ_pos [in PrimeGapS1.MaynardSpecBridge]
factZ_dvd_double [in PrimeGapS1.MaynardSpecBridge]
factZ_to_rat [in PrimeGapS1.MaynardSpecBridge]
factZ_eq_Z_of_nat [in PrimeGapS1.MaynardSpecBridge]
fact_dvd_fact [in PrimeGapS1.MaynardSpecBridge]
flatten_concat [in PrimeGapS1.MaynardSpecBridge]
flat_map_concat_map [in PrimeGapS1.MaynardSpecBridge]
fl_loop_eq_fl_state [in PrimeGapS1.CharPoly]
fl_divisibility_L2 [in PrimeGapS1.CharPoly]
fl_invariant_L2 [in PrimeGapS1.CharPoly]
fl_combined [in PrimeGapS1.CharPoly]
fl_c_rat_is_int [in PrimeGapS1.CharPoly]
fl_c_int_k_step [in PrimeGapS1.CharPoly]
fl_M_int_k_step [in PrimeGapS1.CharPoly]
fl_c_int_k_base [in PrimeGapS1.CharPoly]
fl_M_int_k_base [in PrimeGapS1.CharPoly]
fl_M_int_k_rows [in PrimeGapS1.CharPoly]
fl_M_int_k_dim [in PrimeGapS1.CharPoly]
fl_M_int_k_wf [in PrimeGapS1.CharPoly]
fl_loop_rat_is_char_poly_L2 [in PrimeGapS1.CharPoly]
fl_c_rat_eq_char_poly [in PrimeGapS1.CharPoly]
fl_trace_identity [in PrimeGapS1.CharPoly]
fl_M_expansion [in PrimeGapS1.CharPoly]
fold_left_qplus_den_pos [in PrimeGapS1.MaynardSpecBridge]
fold_left_pointwise_eq [in PrimeGapS1.MaynardSpecBridge]
fold_left_inner_to_map [in PrimeGapS1.MaynardSpecBridge]
fold_left_qplus_den_neq0 [in PrimeGapS1.MaynardSpecBridge]
fold_left_qplus_qfrac [in PrimeGapS1.MaynardSpecBridge]
fold_left_Zadd_sum [in PrimeGapS1.MaynardSpecBridge]
fold_left_Zadd_acc [in PrimeGapS1.MaynardSpecBridge]
forallb_seq_in [in PrimeGapS1.MaynardVerify.Def]
G
G2Z_to_rat [in PrimeGapS1.MaynardSpecBridge]I
inner_row_sum [in PrimeGapS1.MaynardSpecBridge]intr_injective_rat [in PrimeGapS1.CharPoly]
iota_seq_eq [in PrimeGapS1.MaynardSpecBridge]
L
length_eye_row [in PrimeGapS1.CharPoly]length_vadd [in PrimeGapS1.CharPoly]
length_vscale [in PrimeGapS1.CharPoly]
length_zrow [in PrimeGapS1.CharPoly]
length_mtrans_sq [in PrimeGapS1.CharPoly]
length_nth_mtrans_fuel [in PrimeGapS1.CharPoly]
length_mtrans_fuel_exact [in PrimeGapS1.CharPoly]
length_heads [in PrimeGapS1.CharPoly]
length_tails [in PrimeGapS1.CharPoly]
M
mat_dim_madd_eq [in PrimeGapS1.CharPoly]mat_dim_mmul_eq [in PrimeGapS1.CharPoly]
mat_dim_mscale_eq [in PrimeGapS1.CharPoly]
mat_int_to_rat_mmul [in PrimeGapS1.CharPoly]
mat_get_mmul_sq [in PrimeGapS1.CharPoly]
mat_int_to_rat_madd [in PrimeGapS1.CharPoly]
mat_get_madd [in PrimeGapS1.CharPoly]
mat_int_to_rat_meye [in PrimeGapS1.CharPoly]
mat_get_meye_neq [in PrimeGapS1.CharPoly]
mat_get_meye_eq [in PrimeGapS1.CharPoly]
mat_int_to_rat_mscale [in PrimeGapS1.CharPoly]
mat_get_mscale [in PrimeGapS1.CharPoly]
mat_int_to_rat_mzero [in PrimeGapS1.CharPoly]
mat_get_mzero [in PrimeGapS1.CharPoly]
mat_dim_mzero [in PrimeGapS1.CharPoly]
mat_dim_meye [in PrimeGapS1.CharPoly]
maynard_M105_certified_rayleigh [in PrimeGapS1.CertRayleigh]
maynard_basis_uniq [in PrimeGapS1.MaynardBasis]
maynard_basis_spec [in PrimeGapS1.MaynardBasis]
maynard_basis_perm_canonical [in PrimeGapS1.MaynardBasis]
maynard_basis_eq_witness [in PrimeGapS1.MaynardBasis]
maynard_basis_size [in PrimeGapS1.MaynardBasis]
meye_aux_len [in PrimeGapS1.CharPoly]
mtrace_int_to_rat [in PrimeGapS1.CharPoly]
mtrace_aux_diag_sum [in PrimeGapS1.CharPoly]
mzero_aux_len [in PrimeGapS1.CharPoly]
M1_int_cols [in PrimeGapS1.CertRayleigh]
M1_int_rows [in PrimeGapS1.CertRayleigh]
m1_num_den_at_den_pos [in PrimeGapS1.MaynardSpecBridge]
m1_num_den_den_pos [in PrimeGapS1.MaynardSpecBridge]
M1_spec_rat_eq [in PrimeGapS1.MaynardSpecBridge]
m1_num_den_to_rat [in PrimeGapS1.MaynardSpecBridge]
M1_spec_eq_int [in PrimeGapS1.Cert]
M1_entry_match_in_grid [in PrimeGapS1.MaynardVerify.Def]
M1_entry_matchZ_E [in PrimeGapS1.MaynardVerify.Def]
M2_check_rows_0_6 [in PrimeGapS1.MaynardVerify.M2_0]
M2_int_cols [in PrimeGapS1.CertRayleigh]
M2_int_rows [in PrimeGapS1.CertRayleigh]
M2_check_rows_28_34 [in PrimeGapS1.MaynardVerify.M2_4]
M2_check_rows_35_41 [in PrimeGapS1.MaynardVerify.M2_5]
M2_check_rows_14_20 [in PrimeGapS1.MaynardVerify.M2_2]
M2_entry_match_in_grid [in PrimeGapS1.MaynardVerify]
M2_check_rows_app [in PrimeGapS1.MaynardVerify]
m2_num_den_at_den_pos [in PrimeGapS1.MaynardSpecBridge]
m2_num_den_den_pos [in PrimeGapS1.MaynardSpecBridge]
m2_term_num_den_den_pos [in PrimeGapS1.MaynardSpecBridge]
M2_spec_rat_eq [in PrimeGapS1.MaynardSpecBridge]
m2_num_den_to_rat [in PrimeGapS1.MaynardSpecBridge]
m2_outer_qfrac [in PrimeGapS1.MaynardSpecBridge]
m2_term_to_rat [in PrimeGapS1.MaynardSpecBridge]
M2_check_rows_21_27 [in PrimeGapS1.MaynardVerify.M2_3]
M2_check_rows_7_13 [in PrimeGapS1.MaynardVerify.M2_1]
M2_spec_eq_int [in PrimeGapS1.Cert]
M2_entry_matchZ_E [in PrimeGapS1.MaynardVerify.Def]
N
Nat_leb_leqP [in PrimeGapS1.MaynardSpecBridge]nth_nth_mtrans_sq [in PrimeGapS1.CharPoly]
nth_mtrans_length_sq [in PrimeGapS1.CharPoly]
nth_nth_mtrans_fuel [in PrimeGapS1.CharPoly]
nth_heads [in PrimeGapS1.CharPoly]
nth_tails [in PrimeGapS1.CharPoly]
nth_madd [in PrimeGapS1.CharPoly]
nth_Z_vadd [in PrimeGapS1.CharPoly]
nth_meye_aux [in PrimeGapS1.CharPoly]
nth_eye_row_neq [in PrimeGapS1.CharPoly]
nth_eye_row_eq [in PrimeGapS1.CharPoly]
nth_map_vscale [in PrimeGapS1.CharPoly]
nth_Z_vscale [in PrimeGapS1.CharPoly]
nth_mzero_aux_is_zrow [in PrimeGapS1.CharPoly]
nth_Z_zrow [in PrimeGapS1.CharPoly]
P
prod_dblratZ_to_rat [in PrimeGapS1.MaynardSpecBridge]Q
qfrac_eq_div [in PrimeGapS1.MaynardSpecBridge]qfrac_init [in PrimeGapS1.MaynardSpecBridge]
qfrac_qplus [in PrimeGapS1.MaynardSpecBridge]
qfrac_qmul [in PrimeGapS1.MaynardSpecBridge]
qfrac_pair [in PrimeGapS1.MaynardSpecBridge]
qplus_den_pos [in PrimeGapS1.MaynardSpecBridge]
quad_M2_spec_eq_Z [in PrimeGapS1.CertRayleigh]
quad_M1_spec_eq_Z [in PrimeGapS1.CertRayleigh]
quad_spec_eq_Z [in PrimeGapS1.CertRayleigh]
quad_cell_identity [in PrimeGapS1.CertRayleigh]
R
rayleigh_lt_main [in PrimeGapS1.CertRayleigh]rayleigh_lift_generic [in PrimeGapS1.CertRayleigh]
rayleigh_witness_holds_rat [in PrimeGapS1.CertRayleigh]
rayleigh_witness_holds [in PrimeGapS1.CertRayleigh]
rayleigh_witness_M1_positive [in PrimeGapS1.CertRayleigh]
S
seq_split_42 [in PrimeGapS1.MaynardVerify]seq_map_eq [in PrimeGapS1.MaynardSpecBridge]
V
v_den_neq0_rat [in PrimeGapS1.CertRayleigh]v_num_length [in PrimeGapS1.CertRayleigh]
v_den_pos [in PrimeGapS1.CertRayleigh]
Z
Z_rem_of_intr_eq [in PrimeGapS1.CharPoly]Z_to_int_injective [in PrimeGapS1.CharPoly]
Z_to_int_1_rat [in PrimeGapS1.CharPoly]
Z_to_int_of_nat [in PrimeGapS1.CharPoly]
Z_div_exact_rat [in PrimeGapS1.CharPoly]
Z_to_int_opp [in PrimeGapS1.CharPoly]
Z_to_int_dot_int_sum [in PrimeGapS1.CharPoly]
Z_to_int_add [in PrimeGapS1.CharPoly]
Z_pos_sub_int [in PrimeGapS1.CharPoly]
Z_to_int_mul [in PrimeGapS1.CharPoly]
Z_to_int_pos_pos [in PrimeGapS1.CharPoly]
Z_to_int_neg_pos [in PrimeGapS1.CharPoly]
Z_to_int_1 [in PrimeGapS1.CharPoly]
Z_to_int_0 [in PrimeGapS1.CharPoly]
Z_to_int_m2_term_den_neq0 [in PrimeGapS1.MaynardSpecBridge]
Z_to_int_alphaZ_den_neq0 [in PrimeGapS1.MaynardSpecBridge]
Z_to_int_qmul_den_neq0 [in PrimeGapS1.MaynardSpecBridge]
Z_to_int_qplus_den_neq0 [in PrimeGapS1.MaynardSpecBridge]
Z_to_int_factZ_neq0 [in PrimeGapS1.MaynardSpecBridge]
Z_to_int_div_exact [in PrimeGapS1.MaynardSpecBridge]
Z_to_int_pos_rat_neq0 [in PrimeGapS1.MaynardSpecBridge]
Z_to_int_pos_neq0 [in PrimeGapS1.MaynardSpecBridge]
Z_of_nat_dvd [in PrimeGapS1.MaynardSpecBridge]
Z_to_int_factZ [in PrimeGapS1.MaynardSpecBridge]
Z2rat_lt [in PrimeGapS1.CertRayleigh]
Z2rat_pos [in PrimeGapS1.CertRayleigh]
Z2rat_quad_eq_sum [in PrimeGapS1.CertRayleigh]
Z2rat_row_dot_eq_sum [in PrimeGapS1.CertRayleigh]
Z2rat_0 [in PrimeGapS1.CertRayleigh]
Z2rat_add [in PrimeGapS1.CertRayleigh]
Z2rat_mul [in PrimeGapS1.CertRayleigh]
Section Index
F
FLRat [in PrimeGapS1.CharPoly]FL_CharPoly_Core [in PrimeGapS1.CharPoly]
Q
QuadBridge [in PrimeGapS1.CertRayleigh]R
RayleighLift [in PrimeGapS1.CertRayleigh]Abbreviation Index
Q
quad_M2_spec [in PrimeGapS1.CertRayleigh]quad_M1_spec [in PrimeGapS1.CertRayleigh]
Definition Index
A
adj_coef [in PrimeGapS1.CharPoly]all_empty [in PrimeGapS1.IntMat]
all_rows_at_least [in PrimeGapS1.CharPoly]
all_rows_len [in PrimeGapS1.CharPoly]
all_match_M2Z [in PrimeGapS1.MaynardVerify.Def]
all_match_M1Z [in PrimeGapS1.MaynardVerify.Def]
alpha [in PrimeGapS1.MaynardSpec]
alphaZ [in PrimeGapS1.MaynardSpec]
A_int [in PrimeGapS1.Witness]
B
basis [in PrimeGapS1.Witness]binQ [in PrimeGapS1.MaynardFactQ]
binZ [in PrimeGapS1.MaynardSpec]
C
canonical_basis [in PrimeGapS1.MaynardBasis]cff [in PrimeGapS1.MaynardSpec]
cffZ [in PrimeGapS1.MaynardSpec]
charpoly_int [in PrimeGapS1.Witness]
charpoly_of_A_int [in PrimeGapS1.Witness]
charpoly_of_A_int_bigZ [in PrimeGapS1.Witness]
char_poly_int [in PrimeGapS1.CharPoly]
compositions [in PrimeGapS1.MaynardSpec]
compositionsZ [in PrimeGapS1.MaynardSpec]
compositions_auxZ [in PrimeGapS1.MaynardSpec]
compositions_aux [in PrimeGapS1.MaynardSpec]
D
dblratZ [in PrimeGapS1.MaynardSpec]dot_int [in PrimeGapS1.IntMat]
D_q [in PrimeGapS1.Witness]
D_A [in PrimeGapS1.Witness]
D_M2 [in PrimeGapS1.Witness]
D_M1 [in PrimeGapS1.Witness]
E
eye_row [in PrimeGapS1.IntMat]F
factQ [in PrimeGapS1.MaynardFactQ]factZ [in PrimeGapS1.MaynardSpec]
fl_c_rat [in PrimeGapS1.CharPoly]
fl_M_rat [in PrimeGapS1.CharPoly]
fl_loop_rat [in PrimeGapS1.CharPoly]
fl_step_rat [in PrimeGapS1.CharPoly]
fl_c_int_k [in PrimeGapS1.CharPoly]
fl_M_int_k [in PrimeGapS1.CharPoly]
fl_state [in PrimeGapS1.CharPoly]
fl_loop [in PrimeGapS1.CharPoly]
G
G_2 [in PrimeGapS1.MaynardSpec]G2Z [in PrimeGapS1.MaynardSpec]
H
heads [in PrimeGapS1.IntMat]K
K1 [in PrimeGapS1.MaynardSpec]K1n [in PrimeGapS1.MaynardSpec]
K2 [in PrimeGapS1.MaynardSpec]
K2n [in PrimeGapS1.MaynardSpec]
L
lift_bigZ [in PrimeGapS1.Recompose]M
madd [in PrimeGapS1.IntMat]mat [in PrimeGapS1.IntMat]
mat_get [in PrimeGapS1.IntMat]
mat_dim [in PrimeGapS1.IntMat]
mat_int_to_rat [in PrimeGapS1.CharPoly]
mat_vec_mul [in PrimeGapS1.CertRayleigh]
maynard_basis [in PrimeGapS1.MaynardBasis]
meye [in PrimeGapS1.IntMat]
meye_aux [in PrimeGapS1.IntMat]
mmul [in PrimeGapS1.IntMat]
mscale [in PrimeGapS1.IntMat]
mtrace [in PrimeGapS1.IntMat]
mtrace_aux [in PrimeGapS1.IntMat]
mtrans [in PrimeGapS1.IntMat]
mtrans_fuel [in PrimeGapS1.IntMat]
mzero [in PrimeGapS1.IntMat]
mzero_aux [in PrimeGapS1.IntMat]
M1_int [in PrimeGapS1.Witness]
m1_num_den_at [in PrimeGapS1.MaynardSpec]
m1_num_den [in PrimeGapS1.MaynardSpec]
M1_spec_ij [in PrimeGapS1.MaynardSpec]
M1_entry [in PrimeGapS1.MaynardSpec]
M1_entry_matchZ [in PrimeGapS1.MaynardVerify.Def]
m1_den [in PrimeGapS1.MaynardVerify.Def]
m1_num [in PrimeGapS1.MaynardVerify.Def]
M2_int [in PrimeGapS1.Witness]
m2_num_den_at [in PrimeGapS1.MaynardSpec]
m2_num_den [in PrimeGapS1.MaynardSpec]
m2_term_num_den [in PrimeGapS1.MaynardSpec]
M2_spec_ij [in PrimeGapS1.MaynardSpec]
M2_entry [in PrimeGapS1.MaynardSpec]
M2_check_rows [in PrimeGapS1.MaynardVerify.Def]
M2_entry_matchZ [in PrimeGapS1.MaynardVerify.Def]
m2_den [in PrimeGapS1.MaynardVerify.Def]
m2_num [in PrimeGapS1.MaynardVerify.Def]
N
nth_Z [in PrimeGapS1.IntMat]num_M2 [in PrimeGapS1.CertRayleigh]
num_M1 [in PrimeGapS1.CertRayleigh]
P
peval_at_rat [in PrimeGapS1.IntPoly]peval_at_rat_aux [in PrimeGapS1.IntPoly]
plead [in PrimeGapS1.IntPoly]
plead_aux [in PrimeGapS1.IntPoly]
pol [in PrimeGapS1.IntPoly]
pol_to_polyrat [in PrimeGapS1.CharPoly]
prod_dblratZ [in PrimeGapS1.MaynardSpec]
Q
qfrac [in PrimeGapS1.MaynardSpecBridge]qmul [in PrimeGapS1.MaynardSpec]
qplus [in PrimeGapS1.MaynardSpec]
quad [in PrimeGapS1.CertRayleigh]
quad_spec [in PrimeGapS1.CertRayleigh]
R
row_dot [in PrimeGapS1.CertRayleigh]T
tails [in PrimeGapS1.IntMat]V
vadd [in PrimeGapS1.IntMat]vscale [in PrimeGapS1.IntMat]
v_rat [in PrimeGapS1.CertRayleigh]
v_num [in PrimeGapS1.CertRayleigh]
v_den [in PrimeGapS1.CertRayleigh]
v_witness [in PrimeGapS1.Witness_Rayleigh]
Z
zrow [in PrimeGapS1.IntMat]Z_to_int [in PrimeGapS1.CharPoly]
Z2rat [in PrimeGapS1.MaynardSpecBridge]
| 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 | (354 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 | (23 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 | (20 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 | (196 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (2 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 | (109 entries) |
This page has been generated by coqdoc