| 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 | (600 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (473 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 | (5 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 | (9 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 | (72 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 | (10 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 | (31 entries) |
Global Index
A
A [definition, in Friendship.combinatorics]adj [definition, in Friendship.combinatorics]
adjT_cover_noT [lemma, in Friendship.combinatorics]
adjT_subs_cover [lemma, in Friendship.combinatorics]
adj_cover [definition, in Friendship.combinatorics]
adj_mtx_char_poly [lemma, in Friendship.adj2_matrix]
adj_diag_block_form [lemma, in Friendship.adj2_matrix]
adj' [definition, in Friendship.combinatorics]
adj'_card [lemma, in Friendship.combinatorics]
adj'_and_t_disj [lemma, in Friendship.combinatorics]
adj'_and_tU [lemma, in Friendship.combinatorics]
adj'_disjoint [lemma, in Friendship.combinatorics]
adj2 [definition, in Friendship.adj2_matrix]
adj2n [definition, in Friendship.divisibility]
adj2_eq [lemma, in Friendship.combinatorics]
adj2_block_form [lemma, in Friendship.adj2_matrix]
adj2_diag [definition, in Friendship.adj2_matrix]
adj2_matrix_props [section, in Friendship.adj2_matrix]
adj2_matrix [library]
adj:12 [binder, in Friendship.adj2_matrix]
all_covered [lemma, in Friendship.combinatorics]
all2_nseq [lemma, in Friendship.divisibility]
almost_almost_regular [lemma, in Friendship.combinatorics]
almost_regular_eq [lemma, in Friendship.combinatorics]
almost_regular_leq [lemma, in Friendship.combinatorics]
andWl [lemma, in Friendship.combinatorics]
andWr [lemma, in Friendship.combinatorics]
Asqrt [lemma, in Friendship.combinatorics]
A_tr0:7 [binder, in Friendship.divisibility]
A_sqr:6 [binder, in Friendship.divisibility]
A_tr [lemma, in Friendship.combinatorics]
A_diag [lemma, in Friendship.combinatorics]
A' [definition, in Friendship.combinatorics]
A'_tr [lemma, in Friendship.combinatorics]
A2_off_diag [lemma, in Friendship.combinatorics]
A2_diag [lemma, in Friendship.combinatorics]
A:11 [binder, in Friendship.adj2_matrix]
a:19 [binder, in Friendship.divisibility]
a:26 [binder, in Friendship.combinatorics]
a:28 [binder, in Friendship.combinatorics]
a:3 [binder, in Friendship.square_char_poly]
A:33 [binder, in Friendship.matrix_lemmas]
a:4 [binder, in Friendship.bigops]
A:5 [binder, in Friendship.divisibility]
A:5 [binder, in Friendship.matrix_casts]
A:7 [binder, in Friendship.matrix_lemmas]
a:9 [binder, in Friendship.matrix_casts]
B
bigops [section, in Friendship.bigops]bigops [library]
big_bool [lemma, in Friendship.bigops]
b1:10 [binder, in Friendship.statement_reduction]
b:11 [binder, in Friendship.statement_reduction]
b:12 [binder, in Friendship.statement_reduction]
b:27 [binder, in Friendship.combinatorics]
b:28 [binder, in Friendship.divisibility]
b:29 [binder, in Friendship.divisibility]
b:29 [binder, in Friendship.combinatorics]
b:30 [binder, in Friendship.divisibility]
B:34 [binder, in Friendship.matrix_lemmas]
B:6 [binder, in Friendship.matrix_casts]
B:8 [binder, in Friendship.matrix_lemmas]
C
card_cover [lemma, in Friendship.combinatorics]casts [section, in Friendship.matrix_casts]
casts.R [variable, in Friendship.matrix_casts]
cast_eq [lemma, in Friendship.combinatorics]
cast:7 [binder, in Friendship.matrix_casts]
cast:8 [binder, in Friendship.matrix_casts]
charpoly_uconj [lemma, in Friendship.matrix_lemmas]
char_poly_adj2 [lemma, in Friendship.adj2_matrix]
Co [definition, in Friendship.statement_reduction]
Col [definition, in Friendship.statement_reduction]
Colr [lemma, in Friendship.statement_reduction]
Col:12 [binder, in Friendship.combinatorics]
Col:9 [binder, in Friendship.friendship_theorem]
combinatorics [library]
Cor [definition, in Friendship.statement_reduction]
Cor:12 [binder, in Friendship.friendship_theorem]
Cor:16 [binder, in Friendship.combinatorics]
CoUnique [lemma, in Friendship.statement_reduction]
CoUnique:16 [binder, in Friendship.friendship_theorem]
CoUnique:21 [binder, in Friendship.combinatorics]
Co_sym [lemma, in Friendship.combinatorics]
co_nodiag [definition, in Friendship.statement_reduction]
co_set_gt0 [definition, in Friendship.statement_reduction]
co_set:9 [binder, in Friendship.statement_reduction]
Co:6 [binder, in Friendship.friendship_theorem]
Co:8 [binder, in Friendship.combinatorics]
C:35 [binder, in Friendship.matrix_lemmas]
D
deg [definition, in Friendship.combinatorics]det_block [lemma, in Friendship.matrix_lemmas]
det_dotmul.R [variable, in Friendship.matrix_lemmas]
det_dotmul [section, in Friendship.matrix_lemmas]
diagonalizable_m [lemma, in Friendship.adj2_matrix]
diag_vec [definition, in Friendship.adj2_matrix]
Dinv:37 [binder, in Friendship.matrix_lemmas]
disjoint_cover [lemma, in Friendship.combinatorics]
dist2 [definition, in Friendship.combinatorics]
dist2_card [lemma, in Friendship.combinatorics]
div [section, in Friendship.divisibility]
divisibility [library]
div.k [variable, in Friendship.divisibility]
div.n [variable, in Friendship.divisibility]
dotmul [lemma, in Friendship.matrix_lemmas]
D_m_P_eq [lemma, in Friendship.adj2_matrix]
d:19 [binder, in Friendship.square_char_poly]
D:36 [binder, in Friendship.matrix_lemmas]
E
exists_hub_sig [lemma, in Friendship.combinatorics]exists_hub [lemma, in Friendship.combinatorics]
e:15 [binder, in Friendship.statement_reduction]
e:25 [binder, in Friendship.statement_reduction]
e:30 [binder, in Friendship.statement_reduction]
e:38 [binder, in Friendship.statement_reduction]
e:43 [binder, in Friendship.statement_reduction]
e:46 [binder, in Friendship.statement_reduction]
F
Feq [lemma, in Friendship.combinatorics]Firr:23 [binder, in Friendship.friendship_theorem]
Firr:5 [binder, in Friendship.combinatorics]
Firr:5 [binder, in Friendship.friendship_theorem]
Firr:5 [binder, in Friendship.statement_reduction]
fls [lemma, in Friendship.combinatorics]
Friendship [lemma, in Friendship.friendship_theorem]
friendship_sec.assume_contra [section, in Friendship.combinatorics]
friendship_sec [section, in Friendship.combinatorics]
friendship_theorem [library]
Friendship' [lemma, in Friendship.friendship_theorem]
Fsym:22 [binder, in Friendship.friendship_theorem]
Fsym:4 [binder, in Friendship.combinatorics]
Fsym:4 [binder, in Friendship.friendship_theorem]
Fsym:4 [binder, in Friendship.statement_reduction]
f_nodiag:26 [binder, in Friendship.statement_reduction]
f_total_agrees_with_f [lemma, in Friendship.statement_reduction]
f_nodiag:16 [binder, in Friendship.statement_reduction]
f_total [definition, in Friendship.statement_reduction]
F:21 [binder, in Friendship.friendship_theorem]
F:3 [binder, in Friendship.combinatorics]
F:3 [binder, in Friendship.friendship_theorem]
F:3 [binder, in Friendship.statement_reduction]
f:4 [binder, in Friendship.matrix_lemmas]
F:5 [binder, in Friendship.bigops]
I
idomain_sqrt [lemma, in Friendship.divisibility]idP' [definition, in Friendship.statement_reduction]
is_square_root [definition, in Friendship.adj2_matrix]
i_μ_ln:15 [binder, in Friendship.square_char_poly]
i_μ:14 [binder, in Friendship.square_char_poly]
i_ln:7 [binder, in Friendship.square_char_poly]
i:18 [binder, in Friendship.divisibility]
i:21 [binder, in Friendship.matrix_lemmas]
i:23 [binder, in Friendship.matrix_lemmas]
i:25 [binder, in Friendship.divisibility]
i:25 [binder, in Friendship.matrix_lemmas]
i:26 [binder, in Friendship.divisibility]
i:27 [binder, in Friendship.divisibility]
i:27 [binder, in Friendship.matrix_lemmas]
i:28 [binder, in Friendship.matrix_lemmas]
i:29 [binder, in Friendship.matrix_lemmas]
I:3 [binder, in Friendship.bigops]
i:31 [binder, in Friendship.divisibility]
i:32 [binder, in Friendship.divisibility]
i:33 [binder, in Friendship.divisibility]
i:49 [binder, in Friendship.divisibility]
i:5 [binder, in Friendship.square_char_poly]
i:50 [binder, in Friendship.divisibility]
i:51 [binder, in Friendship.divisibility]
i:52 [binder, in Friendship.divisibility]
i:53 [binder, in Friendship.divisibility]
i:53 [binder, in Friendship.adj2_matrix]
i:54 [binder, in Friendship.divisibility]
i:54 [binder, in Friendship.adj2_matrix]
i:55 [binder, in Friendship.adj2_matrix]
i:6 [binder, in Friendship.bigops]
i:64 [binder, in Friendship.combinatorics]
i:66 [binder, in Friendship.combinatorics]
i:67 [binder, in Friendship.combinatorics]
i:7 [binder, in Friendship.bigops]
i:8 [binder, in Friendship.bigops]
i:85 [binder, in Friendship.combinatorics]
J
j:20 [binder, in Friendship.matrix_lemmas]j:22 [binder, in Friendship.matrix_lemmas]
j:24 [binder, in Friendship.matrix_lemmas]
j:26 [binder, in Friendship.matrix_lemmas]
j:62 [binder, in Friendship.square_char_poly]
j:63 [binder, in Friendship.square_char_poly]
j:64 [binder, in Friendship.square_char_poly]
j:65 [binder, in Friendship.square_char_poly]
j:65 [binder, in Friendship.combinatorics]
j:66 [binder, in Friendship.square_char_poly]
j:67 [binder, in Friendship.square_char_poly]
j:68 [binder, in Friendship.combinatorics]
j:69 [binder, in Friendship.combinatorics]
j:70 [binder, in Friendship.combinatorics]
j:86 [binder, in Friendship.combinatorics]
K
k [definition, in Friendship.combinatorics]kge1 [lemma, in Friendship.combinatorics]
kge1:3 [binder, in Friendship.divisibility]
kge1:3 [binder, in Friendship.adj2_matrix]
kn_1 [lemma, in Friendship.divisibility]
k_is_2 [lemma, in Friendship.divisibility]
k_not_2 [lemma, in Friendship.combinatorics]
k_not_1 [lemma, in Friendship.combinatorics]
k:2 [binder, in Friendship.adj2_matrix]
L
lams [definition, in Friendship.adj2_matrix]lams_prod [lemma, in Friendship.adj2_matrix]
list_insert [definition, in Friendship.square_char_poly]
li:16 [binder, in Friendship.divisibility]
li:34 [binder, in Friendship.divisibility]
li:35 [binder, in Friendship.divisibility]
li:36 [binder, in Friendship.divisibility]
l_len:6 [binder, in Friendship.square_char_poly]
l:10 [binder, in Friendship.adj2_matrix]
l:12 [binder, in Friendship.divisibility]
l:19 [binder, in Friendship.combinatorics]
l:2 [binder, in Friendship.square_char_poly]
l:8 [binder, in Friendship.adj2_matrix]
l:9 [binder, in Friendship.adj2_matrix]
M
map_adj_inj [lemma, in Friendship.combinatorics]map_adj_im [lemma, in Friendship.combinatorics]
matN [definition, in Friendship.adj2_matrix]
matrix_lemmas [library]
matrix_casts [library]
mNn:11 [binder, in Friendship.combinatorics]
mNn:15 [binder, in Friendship.combinatorics]
mNn:20 [binder, in Friendship.combinatorics]
mNn:24 [binder, in Friendship.combinatorics]
mulmx_castmx [lemma, in Friendship.matrix_casts]
m:13 [binder, in Friendship.combinatorics]
m:17 [binder, in Friendship.combinatorics]
m:22 [binder, in Friendship.combinatorics]
m:6 [binder, in Friendship.combinatorics]
m:9 [binder, in Friendship.combinatorics]
N
n [definition, in Friendship.combinatorics]nFuv:38 [binder, in Friendship.combinatorics]
nFuv:46 [binder, in Friendship.combinatorics]
nge1 [lemma, in Friendship.combinatorics]
nge1:4 [binder, in Friendship.divisibility]
nge1:4 [binder, in Friendship.adj2_matrix]
nk [lemma, in Friendship.combinatorics]
nk_eq:8 [binder, in Friendship.divisibility]
nn [definition, in Friendship.combinatorics]
nNm:25 [binder, in Friendship.combinatorics]
nn':4 [binder, in Friendship.matrix_casts]
nn:15 [binder, in Friendship.divisibility]
nn:38 [binder, in Friendship.matrix_lemmas]
no_hub [lemma, in Friendship.combinatorics]
no_hub':56 [binder, in Friendship.combinatorics]
n_eq [lemma, in Friendship.combinatorics]
n':3 [binder, in Friendship.matrix_casts]
n1:31 [binder, in Friendship.matrix_lemmas]
n2:32 [binder, in Friendship.matrix_lemmas]
n:1 [binder, in Friendship.adj2_matrix]
n:10 [binder, in Friendship.combinatorics]
n:11 [binder, in Friendship.square_char_poly]
n:14 [binder, in Friendship.combinatorics]
n:18 [binder, in Friendship.combinatorics]
n:2 [binder, in Friendship.matrix_casts]
n:2 [binder, in Friendship.matrix_lemmas]
n:23 [binder, in Friendship.combinatorics]
n:4 [binder, in Friendship.square_char_poly]
n:5 [binder, in Friendship.matrix_lemmas]
n:7 [binder, in Friendship.combinatorics]
n:9 [binder, in Friendship.matrix_lemmas]
P
P [definition, in Friendship.adj2_matrix]polys_and_squares_technical_lemma [lemma, in Friendship.square_char_poly]
P_unit [lemma, in Friendship.adj2_matrix]
P:13 [binder, in Friendship.divisibility]
P:16 [binder, in Friendship.square_char_poly]
p:22 [binder, in Friendship.square_char_poly]
P:6 [binder, in Friendship.matrix_lemmas]
pλ:58 [binder, in Friendship.square_char_poly]
pλ:59 [binder, in Friendship.square_char_poly]
pλ:60 [binder, in Friendship.square_char_poly]
Q
q:23 [binder, in Friendship.adj2_matrix]q:27 [binder, in Friendship.adj2_matrix]
q:28 [binder, in Friendship.adj2_matrix]
q:42 [binder, in Friendship.square_char_poly]
q:43 [binder, in Friendship.square_char_poly]
q:44 [binder, in Friendship.square_char_poly]
q:56 [binder, in Friendship.adj2_matrix]
q:57 [binder, in Friendship.adj2_matrix]
q:58 [binder, in Friendship.adj2_matrix]
R
R [definition, in Friendship.combinatorics]R [definition, in Friendship.adj2_matrix]
regular [lemma, in Friendship.combinatorics]
RR [definition, in Friendship.square_char_poly]
R:1 [binder, in Friendship.bigops]
R:8 [binder, in Friendship.square_char_poly]
S
scalar_mx_castmx [lemma, in Friendship.matrix_casts]simmx_charpoly [lemma, in Friendship.matrix_lemmas]
sim_char_poly.F [variable, in Friendship.matrix_lemmas]
sim_char_poly [section, in Friendship.matrix_lemmas]
split_tuples [lemma, in Friendship.square_char_poly]
square_polys [section, in Friendship.square_char_poly]
square_char_poly [library]
StatementReduction [section, in Friendship.statement_reduction]
statement_reduction [library]
summx_castmx [lemma, in Friendship.matrix_casts]
sum_of_roots [lemma, in Friendship.divisibility]
sz_λ:13 [binder, in Friendship.square_char_poly]
sz_μ:12 [binder, in Friendship.square_char_poly]
S:2 [binder, in Friendship.bigops]
T
tr_adj_rel_nat [lemma, in Friendship.divisibility]tr_adj_rel [lemma, in Friendship.divisibility]
tr_castmx [lemma, in Friendship.matrix_casts]
T_size [lemma, in Friendship.combinatorics]
T_elem [definition, in Friendship.combinatorics]
T_nonempty:2 [binder, in Friendship.combinatorics]
T_nonempty:20 [binder, in Friendship.friendship_theorem]
T_nonempty:2 [binder, in Friendship.friendship_theorem]
T_elem [definition, in Friendship.statement_reduction]
T_nonempty:2 [binder, in Friendship.statement_reduction]
T:1 [binder, in Friendship.square_char_poly]
T:1 [binder, in Friendship.combinatorics]
T:1 [binder, in Friendship.friendship_theorem]
T:1 [binder, in Friendship.statement_reduction]
T:11 [binder, in Friendship.divisibility]
T:19 [binder, in Friendship.friendship_theorem]
U
uNv:45 [binder, in Friendship.combinatorics]u1:78 [binder, in Friendship.combinatorics]
u2:79 [binder, in Friendship.combinatorics]
u:10 [binder, in Friendship.friendship_theorem]
u:104 [binder, in Friendship.combinatorics]
u:108 [binder, in Friendship.combinatorics]
u:109 [binder, in Friendship.combinatorics]
u:110 [binder, in Friendship.combinatorics]
u:114 [binder, in Friendship.combinatorics]
u:118 [binder, in Friendship.combinatorics]
u:13 [binder, in Friendship.friendship_theorem]
u:13 [binder, in Friendship.statement_reduction]
u:152 [binder, in Friendship.combinatorics]
u:17 [binder, in Friendship.friendship_theorem]
u:18 [binder, in Friendship.statement_reduction]
u:21 [binder, in Friendship.statement_reduction]
u:23 [binder, in Friendship.statement_reduction]
u:24 [binder, in Friendship.friendship_theorem]
u:27 [binder, in Friendship.friendship_theorem]
u:28 [binder, in Friendship.statement_reduction]
u:30 [binder, in Friendship.combinatorics]
u:31 [binder, in Friendship.statement_reduction]
u:32 [binder, in Friendship.combinatorics]
u:33 [binder, in Friendship.combinatorics]
u:34 [binder, in Friendship.statement_reduction]
u:36 [binder, in Friendship.combinatorics]
u:36 [binder, in Friendship.statement_reduction]
u:39 [binder, in Friendship.statement_reduction]
u:41 [binder, in Friendship.combinatorics]
u:41 [binder, in Friendship.statement_reduction]
u:43 [binder, in Friendship.combinatorics]
u:44 [binder, in Friendship.statement_reduction]
u:47 [binder, in Friendship.combinatorics]
u:47 [binder, in Friendship.statement_reduction]
u:50 [binder, in Friendship.combinatorics]
u:52 [binder, in Friendship.combinatorics]
u:57 [binder, in Friendship.combinatorics]
u:6 [binder, in Friendship.statement_reduction]
u:61 [binder, in Friendship.combinatorics]
u:62 [binder, in Friendship.combinatorics]
u:7 [binder, in Friendship.friendship_theorem]
u:76 [binder, in Friendship.combinatorics]
u:80 [binder, in Friendship.combinatorics]
u:81 [binder, in Friendship.combinatorics]
u:82 [binder, in Friendship.combinatorics]
u:83 [binder, in Friendship.combinatorics]
V
viete_sum [lemma, in Friendship.matrix_lemmas]v_not_in_adj_u [lemma, in Friendship.combinatorics]
v:100 [binder, in Friendship.combinatorics]
v:101 [binder, in Friendship.combinatorics]
v:105 [binder, in Friendship.combinatorics]
v:106 [binder, in Friendship.combinatorics]
v:107 [binder, in Friendship.combinatorics]
v:11 [binder, in Friendship.friendship_theorem]
v:111 [binder, in Friendship.combinatorics]
v:112 [binder, in Friendship.combinatorics]
v:113 [binder, in Friendship.combinatorics]
v:115 [binder, in Friendship.combinatorics]
v:116 [binder, in Friendship.combinatorics]
v:117 [binder, in Friendship.combinatorics]
v:119 [binder, in Friendship.combinatorics]
v:120 [binder, in Friendship.combinatorics]
v:121 [binder, in Friendship.combinatorics]
v:123 [binder, in Friendship.combinatorics]
v:124 [binder, in Friendship.combinatorics]
v:125 [binder, in Friendship.combinatorics]
v:127 [binder, in Friendship.combinatorics]
v:128 [binder, in Friendship.combinatorics]
v:129 [binder, in Friendship.combinatorics]
v:131 [binder, in Friendship.combinatorics]
v:132 [binder, in Friendship.combinatorics]
v:133 [binder, in Friendship.combinatorics]
v:135 [binder, in Friendship.combinatorics]
v:136 [binder, in Friendship.combinatorics]
v:137 [binder, in Friendship.combinatorics]
v:139 [binder, in Friendship.combinatorics]
v:14 [binder, in Friendship.friendship_theorem]
v:14 [binder, in Friendship.statement_reduction]
v:140 [binder, in Friendship.combinatorics]
v:141 [binder, in Friendship.combinatorics]
v:143 [binder, in Friendship.combinatorics]
v:144 [binder, in Friendship.combinatorics]
v:145 [binder, in Friendship.combinatorics]
v:146 [binder, in Friendship.combinatorics]
v:147 [binder, in Friendship.combinatorics]
v:148 [binder, in Friendship.combinatorics]
v:149 [binder, in Friendship.combinatorics]
v:150 [binder, in Friendship.combinatorics]
v:151 [binder, in Friendship.combinatorics]
v:153 [binder, in Friendship.combinatorics]
v:18 [binder, in Friendship.friendship_theorem]
v:19 [binder, in Friendship.statement_reduction]
v:22 [binder, in Friendship.statement_reduction]
v:24 [binder, in Friendship.statement_reduction]
v:25 [binder, in Friendship.friendship_theorem]
v:28 [binder, in Friendship.friendship_theorem]
v:29 [binder, in Friendship.statement_reduction]
V:3 [binder, in Friendship.matrix_lemmas]
v:32 [binder, in Friendship.statement_reduction]
v:34 [binder, in Friendship.combinatorics]
v:35 [binder, in Friendship.statement_reduction]
v:37 [binder, in Friendship.combinatorics]
v:37 [binder, in Friendship.statement_reduction]
v:40 [binder, in Friendship.statement_reduction]
v:42 [binder, in Friendship.combinatorics]
v:42 [binder, in Friendship.statement_reduction]
v:44 [binder, in Friendship.combinatorics]
v:45 [binder, in Friendship.statement_reduction]
v:48 [binder, in Friendship.combinatorics]
v:48 [binder, in Friendship.statement_reduction]
v:51 [binder, in Friendship.combinatorics]
v:53 [binder, in Friendship.combinatorics]
v:54 [binder, in Friendship.combinatorics]
v:55 [binder, in Friendship.combinatorics]
v:58 [binder, in Friendship.combinatorics]
v:59 [binder, in Friendship.combinatorics]
v:63 [binder, in Friendship.combinatorics]
v:7 [binder, in Friendship.statement_reduction]
v:8 [binder, in Friendship.friendship_theorem]
v:99 [binder, in Friendship.combinatorics]
W
wAdjU:40 [binder, in Friendship.combinatorics]w:15 [binder, in Friendship.friendship_theorem]
w:26 [binder, in Friendship.friendship_theorem]
w:31 [binder, in Friendship.combinatorics]
w:33 [binder, in Friendship.statement_reduction]
w:35 [binder, in Friendship.combinatorics]
w:39 [binder, in Friendship.combinatorics]
w:49 [binder, in Friendship.statement_reduction]
w:77 [binder, in Friendship.combinatorics]
w:8 [binder, in Friendship.statement_reduction]
X
x2:10 [binder, in Friendship.divisibility]x:102 [binder, in Friendship.combinatorics]
x:103 [binder, in Friendship.combinatorics]
x:122 [binder, in Friendship.combinatorics]
x:126 [binder, in Friendship.combinatorics]
x:130 [binder, in Friendship.combinatorics]
x:134 [binder, in Friendship.combinatorics]
x:138 [binder, in Friendship.combinatorics]
x:14 [binder, in Friendship.divisibility]
x:142 [binder, in Friendship.combinatorics]
x:17 [binder, in Friendship.statement_reduction]
x:20 [binder, in Friendship.statement_reduction]
x:27 [binder, in Friendship.statement_reduction]
x:49 [binder, in Friendship.combinatorics]
x:55 [binder, in Friendship.divisibility]
x:60 [binder, in Friendship.combinatorics]
x:71 [binder, in Friendship.combinatorics]
x:72 [binder, in Friendship.combinatorics]
x:73 [binder, in Friendship.combinatorics]
x:9 [binder, in Friendship.divisibility]
x:98 [binder, in Friendship.combinatorics]
Z
z:20 [binder, in Friendship.adj2_matrix]z:21 [binder, in Friendship.adj2_matrix]
z:22 [binder, in Friendship.adj2_matrix]
other
α:87 [binder, in Friendship.combinatorics]α:88 [binder, in Friendship.combinatorics]
α:89 [binder, in Friendship.combinatorics]
α:90 [binder, in Friendship.combinatorics]
α:91 [binder, in Friendship.combinatorics]
α:92 [binder, in Friendship.combinatorics]
λs:10 [binder, in Friendship.square_char_poly]
λs:20 [binder, in Friendship.square_char_poly]
λ0:80 [binder, in Friendship.square_char_poly]
λ0:81 [binder, in Friendship.square_char_poly]
λ0:82 [binder, in Friendship.square_char_poly]
λ0:83 [binder, in Friendship.square_char_poly]
λ0:84 [binder, in Friendship.square_char_poly]
λ0:85 [binder, in Friendship.square_char_poly]
λ:18 [binder, in Friendship.square_char_poly]
λ:19 [binder, in Friendship.adj2_matrix]
λ:21 [binder, in Friendship.divisibility]
λ:23 [binder, in Friendship.square_char_poly]
λ:24 [binder, in Friendship.square_char_poly]
λ:25 [binder, in Friendship.square_char_poly]
λ:38 [binder, in Friendship.square_char_poly]
λ:39 [binder, in Friendship.square_char_poly]
λ:40 [binder, in Friendship.square_char_poly]
λ:41 [binder, in Friendship.square_char_poly]
λ:45 [binder, in Friendship.square_char_poly]
λ:46 [binder, in Friendship.square_char_poly]
λ:47 [binder, in Friendship.square_char_poly]
λ:48 [binder, in Friendship.square_char_poly]
λ:49 [binder, in Friendship.square_char_poly]
λ:50 [binder, in Friendship.square_char_poly]
λ:51 [binder, in Friendship.square_char_poly]
λ:52 [binder, in Friendship.square_char_poly]
λ:53 [binder, in Friendship.square_char_poly]
λ:54 [binder, in Friendship.square_char_poly]
λ:55 [binder, in Friendship.square_char_poly]
λ:56 [binder, in Friendship.square_char_poly]
λ:57 [binder, in Friendship.square_char_poly]
λ:68 [binder, in Friendship.square_char_poly]
λ:69 [binder, in Friendship.square_char_poly]
λ:70 [binder, in Friendship.square_char_poly]
λ:71 [binder, in Friendship.square_char_poly]
λ:72 [binder, in Friendship.square_char_poly]
λ:73 [binder, in Friendship.square_char_poly]
λ:74 [binder, in Friendship.square_char_poly]
λ:75 [binder, in Friendship.square_char_poly]
λ:76 [binder, in Friendship.square_char_poly]
μs':13 [binder, in Friendship.adj2_matrix]
μs':17 [binder, in Friendship.adj2_matrix]
μs':29 [binder, in Friendship.square_char_poly]
μs':36 [binder, in Friendship.square_char_poly]
μs:10 [binder, in Friendship.matrix_lemmas]
μs:17 [binder, in Friendship.divisibility]
μs:21 [binder, in Friendship.square_char_poly]
μs:9 [binder, in Friendship.square_char_poly]
μ':33 [binder, in Friendship.square_char_poly]
μ':34 [binder, in Friendship.square_char_poly]
μ':35 [binder, in Friendship.square_char_poly]
μ:11 [binder, in Friendship.matrix_lemmas]
μ:12 [binder, in Friendship.matrix_lemmas]
μ:13 [binder, in Friendship.matrix_lemmas]
μ:14 [binder, in Friendship.matrix_lemmas]
μ:14 [binder, in Friendship.adj2_matrix]
μ:15 [binder, in Friendship.matrix_lemmas]
μ:15 [binder, in Friendship.adj2_matrix]
μ:16 [binder, in Friendship.matrix_lemmas]
μ:16 [binder, in Friendship.adj2_matrix]
μ:17 [binder, in Friendship.square_char_poly]
μ:17 [binder, in Friendship.matrix_lemmas]
μ:18 [binder, in Friendship.matrix_lemmas]
μ:18 [binder, in Friendship.adj2_matrix]
μ:19 [binder, in Friendship.matrix_lemmas]
μ:20 [binder, in Friendship.divisibility]
μ:22 [binder, in Friendship.divisibility]
μ:23 [binder, in Friendship.divisibility]
μ:24 [binder, in Friendship.divisibility]
μ:24 [binder, in Friendship.adj2_matrix]
μ:25 [binder, in Friendship.adj2_matrix]
μ:26 [binder, in Friendship.square_char_poly]
μ:26 [binder, in Friendship.adj2_matrix]
μ:27 [binder, in Friendship.square_char_poly]
μ:28 [binder, in Friendship.square_char_poly]
μ:29 [binder, in Friendship.adj2_matrix]
μ:30 [binder, in Friendship.square_char_poly]
μ:30 [binder, in Friendship.adj2_matrix]
μ:31 [binder, in Friendship.square_char_poly]
μ:31 [binder, in Friendship.adj2_matrix]
μ:32 [binder, in Friendship.square_char_poly]
μ:32 [binder, in Friendship.adj2_matrix]
μ:33 [binder, in Friendship.adj2_matrix]
μ:34 [binder, in Friendship.adj2_matrix]
μ:35 [binder, in Friendship.adj2_matrix]
μ:36 [binder, in Friendship.adj2_matrix]
μ:37 [binder, in Friendship.square_char_poly]
μ:37 [binder, in Friendship.divisibility]
μ:37 [binder, in Friendship.adj2_matrix]
μ:38 [binder, in Friendship.divisibility]
μ:38 [binder, in Friendship.adj2_matrix]
μ:39 [binder, in Friendship.divisibility]
μ:39 [binder, in Friendship.adj2_matrix]
μ:40 [binder, in Friendship.divisibility]
μ:40 [binder, in Friendship.adj2_matrix]
μ:41 [binder, in Friendship.divisibility]
μ:41 [binder, in Friendship.adj2_matrix]
μ:42 [binder, in Friendship.divisibility]
μ:42 [binder, in Friendship.adj2_matrix]
μ:43 [binder, in Friendship.divisibility]
μ:43 [binder, in Friendship.adj2_matrix]
μ:44 [binder, in Friendship.divisibility]
μ:44 [binder, in Friendship.adj2_matrix]
μ:45 [binder, in Friendship.divisibility]
μ:45 [binder, in Friendship.adj2_matrix]
μ:46 [binder, in Friendship.divisibility]
μ:46 [binder, in Friendship.adj2_matrix]
μ:47 [binder, in Friendship.divisibility]
μ:47 [binder, in Friendship.adj2_matrix]
μ:48 [binder, in Friendship.divisibility]
μ:48 [binder, in Friendship.adj2_matrix]
μ:49 [binder, in Friendship.adj2_matrix]
μ:50 [binder, in Friendship.adj2_matrix]
μ:51 [binder, in Friendship.adj2_matrix]
μ:52 [binder, in Friendship.adj2_matrix]
μ:59 [binder, in Friendship.adj2_matrix]
μ:60 [binder, in Friendship.adj2_matrix]
μ:61 [binder, in Friendship.adj2_matrix]
μ:65 [binder, in Friendship.adj2_matrix]
μ:66 [binder, in Friendship.adj2_matrix]
μ:67 [binder, in Friendship.adj2_matrix]
μ:68 [binder, in Friendship.adj2_matrix]
μ:77 [binder, in Friendship.square_char_poly]
μ:78 [binder, in Friendship.square_char_poly]
μ:79 [binder, in Friendship.square_char_poly]
Binder Index
A
adj:12 [in Friendship.adj2_matrix]A_tr0:7 [in Friendship.divisibility]
A_sqr:6 [in Friendship.divisibility]
A:11 [in Friendship.adj2_matrix]
a:19 [in Friendship.divisibility]
a:26 [in Friendship.combinatorics]
a:28 [in Friendship.combinatorics]
a:3 [in Friendship.square_char_poly]
A:33 [in Friendship.matrix_lemmas]
a:4 [in Friendship.bigops]
A:5 [in Friendship.divisibility]
A:5 [in Friendship.matrix_casts]
A:7 [in Friendship.matrix_lemmas]
a:9 [in Friendship.matrix_casts]
B
b1:10 [in Friendship.statement_reduction]b:11 [in Friendship.statement_reduction]
b:12 [in Friendship.statement_reduction]
b:27 [in Friendship.combinatorics]
b:28 [in Friendship.divisibility]
b:29 [in Friendship.divisibility]
b:29 [in Friendship.combinatorics]
b:30 [in Friendship.divisibility]
B:34 [in Friendship.matrix_lemmas]
B:6 [in Friendship.matrix_casts]
B:8 [in Friendship.matrix_lemmas]
C
cast:7 [in Friendship.matrix_casts]cast:8 [in Friendship.matrix_casts]
Col:12 [in Friendship.combinatorics]
Col:9 [in Friendship.friendship_theorem]
Cor:12 [in Friendship.friendship_theorem]
Cor:16 [in Friendship.combinatorics]
CoUnique:16 [in Friendship.friendship_theorem]
CoUnique:21 [in Friendship.combinatorics]
co_set:9 [in Friendship.statement_reduction]
Co:6 [in Friendship.friendship_theorem]
Co:8 [in Friendship.combinatorics]
C:35 [in Friendship.matrix_lemmas]
D
Dinv:37 [in Friendship.matrix_lemmas]d:19 [in Friendship.square_char_poly]
D:36 [in Friendship.matrix_lemmas]
E
e:15 [in Friendship.statement_reduction]e:25 [in Friendship.statement_reduction]
e:30 [in Friendship.statement_reduction]
e:38 [in Friendship.statement_reduction]
e:43 [in Friendship.statement_reduction]
e:46 [in Friendship.statement_reduction]
F
Firr:23 [in Friendship.friendship_theorem]Firr:5 [in Friendship.combinatorics]
Firr:5 [in Friendship.friendship_theorem]
Firr:5 [in Friendship.statement_reduction]
Fsym:22 [in Friendship.friendship_theorem]
Fsym:4 [in Friendship.combinatorics]
Fsym:4 [in Friendship.friendship_theorem]
Fsym:4 [in Friendship.statement_reduction]
f_nodiag:26 [in Friendship.statement_reduction]
f_nodiag:16 [in Friendship.statement_reduction]
F:21 [in Friendship.friendship_theorem]
F:3 [in Friendship.combinatorics]
F:3 [in Friendship.friendship_theorem]
F:3 [in Friendship.statement_reduction]
f:4 [in Friendship.matrix_lemmas]
F:5 [in Friendship.bigops]
I
i_μ_ln:15 [in Friendship.square_char_poly]i_μ:14 [in Friendship.square_char_poly]
i_ln:7 [in Friendship.square_char_poly]
i:18 [in Friendship.divisibility]
i:21 [in Friendship.matrix_lemmas]
i:23 [in Friendship.matrix_lemmas]
i:25 [in Friendship.divisibility]
i:25 [in Friendship.matrix_lemmas]
i:26 [in Friendship.divisibility]
i:27 [in Friendship.divisibility]
i:27 [in Friendship.matrix_lemmas]
i:28 [in Friendship.matrix_lemmas]
i:29 [in Friendship.matrix_lemmas]
I:3 [in Friendship.bigops]
i:31 [in Friendship.divisibility]
i:32 [in Friendship.divisibility]
i:33 [in Friendship.divisibility]
i:49 [in Friendship.divisibility]
i:5 [in Friendship.square_char_poly]
i:50 [in Friendship.divisibility]
i:51 [in Friendship.divisibility]
i:52 [in Friendship.divisibility]
i:53 [in Friendship.divisibility]
i:53 [in Friendship.adj2_matrix]
i:54 [in Friendship.divisibility]
i:54 [in Friendship.adj2_matrix]
i:55 [in Friendship.adj2_matrix]
i:6 [in Friendship.bigops]
i:64 [in Friendship.combinatorics]
i:66 [in Friendship.combinatorics]
i:67 [in Friendship.combinatorics]
i:7 [in Friendship.bigops]
i:8 [in Friendship.bigops]
i:85 [in Friendship.combinatorics]
J
j:20 [in Friendship.matrix_lemmas]j:22 [in Friendship.matrix_lemmas]
j:24 [in Friendship.matrix_lemmas]
j:26 [in Friendship.matrix_lemmas]
j:62 [in Friendship.square_char_poly]
j:63 [in Friendship.square_char_poly]
j:64 [in Friendship.square_char_poly]
j:65 [in Friendship.square_char_poly]
j:65 [in Friendship.combinatorics]
j:66 [in Friendship.square_char_poly]
j:67 [in Friendship.square_char_poly]
j:68 [in Friendship.combinatorics]
j:69 [in Friendship.combinatorics]
j:70 [in Friendship.combinatorics]
j:86 [in Friendship.combinatorics]
K
kge1:3 [in Friendship.divisibility]kge1:3 [in Friendship.adj2_matrix]
k:2 [in Friendship.adj2_matrix]
L
li:16 [in Friendship.divisibility]li:34 [in Friendship.divisibility]
li:35 [in Friendship.divisibility]
li:36 [in Friendship.divisibility]
l_len:6 [in Friendship.square_char_poly]
l:10 [in Friendship.adj2_matrix]
l:12 [in Friendship.divisibility]
l:19 [in Friendship.combinatorics]
l:2 [in Friendship.square_char_poly]
l:8 [in Friendship.adj2_matrix]
l:9 [in Friendship.adj2_matrix]
M
mNn:11 [in Friendship.combinatorics]mNn:15 [in Friendship.combinatorics]
mNn:20 [in Friendship.combinatorics]
mNn:24 [in Friendship.combinatorics]
m:13 [in Friendship.combinatorics]
m:17 [in Friendship.combinatorics]
m:22 [in Friendship.combinatorics]
m:6 [in Friendship.combinatorics]
m:9 [in Friendship.combinatorics]
N
nFuv:38 [in Friendship.combinatorics]nFuv:46 [in Friendship.combinatorics]
nge1:4 [in Friendship.divisibility]
nge1:4 [in Friendship.adj2_matrix]
nk_eq:8 [in Friendship.divisibility]
nNm:25 [in Friendship.combinatorics]
nn':4 [in Friendship.matrix_casts]
nn:15 [in Friendship.divisibility]
nn:38 [in Friendship.matrix_lemmas]
no_hub':56 [in Friendship.combinatorics]
n':3 [in Friendship.matrix_casts]
n1:31 [in Friendship.matrix_lemmas]
n2:32 [in Friendship.matrix_lemmas]
n:1 [in Friendship.adj2_matrix]
n:10 [in Friendship.combinatorics]
n:11 [in Friendship.square_char_poly]
n:14 [in Friendship.combinatorics]
n:18 [in Friendship.combinatorics]
n:2 [in Friendship.matrix_casts]
n:2 [in Friendship.matrix_lemmas]
n:23 [in Friendship.combinatorics]
n:4 [in Friendship.square_char_poly]
n:5 [in Friendship.matrix_lemmas]
n:7 [in Friendship.combinatorics]
n:9 [in Friendship.matrix_lemmas]
P
P:13 [in Friendship.divisibility]P:16 [in Friendship.square_char_poly]
p:22 [in Friendship.square_char_poly]
P:6 [in Friendship.matrix_lemmas]
pλ:58 [in Friendship.square_char_poly]
pλ:59 [in Friendship.square_char_poly]
pλ:60 [in Friendship.square_char_poly]
Q
q:23 [in Friendship.adj2_matrix]q:27 [in Friendship.adj2_matrix]
q:28 [in Friendship.adj2_matrix]
q:42 [in Friendship.square_char_poly]
q:43 [in Friendship.square_char_poly]
q:44 [in Friendship.square_char_poly]
q:56 [in Friendship.adj2_matrix]
q:57 [in Friendship.adj2_matrix]
q:58 [in Friendship.adj2_matrix]
R
R:1 [in Friendship.bigops]R:8 [in Friendship.square_char_poly]
S
sz_λ:13 [in Friendship.square_char_poly]sz_μ:12 [in Friendship.square_char_poly]
S:2 [in Friendship.bigops]
T
T_nonempty:2 [in Friendship.combinatorics]T_nonempty:20 [in Friendship.friendship_theorem]
T_nonempty:2 [in Friendship.friendship_theorem]
T_nonempty:2 [in Friendship.statement_reduction]
T:1 [in Friendship.square_char_poly]
T:1 [in Friendship.combinatorics]
T:1 [in Friendship.friendship_theorem]
T:1 [in Friendship.statement_reduction]
T:11 [in Friendship.divisibility]
T:19 [in Friendship.friendship_theorem]
U
uNv:45 [in Friendship.combinatorics]u1:78 [in Friendship.combinatorics]
u2:79 [in Friendship.combinatorics]
u:10 [in Friendship.friendship_theorem]
u:104 [in Friendship.combinatorics]
u:108 [in Friendship.combinatorics]
u:109 [in Friendship.combinatorics]
u:110 [in Friendship.combinatorics]
u:114 [in Friendship.combinatorics]
u:118 [in Friendship.combinatorics]
u:13 [in Friendship.friendship_theorem]
u:13 [in Friendship.statement_reduction]
u:152 [in Friendship.combinatorics]
u:17 [in Friendship.friendship_theorem]
u:18 [in Friendship.statement_reduction]
u:21 [in Friendship.statement_reduction]
u:23 [in Friendship.statement_reduction]
u:24 [in Friendship.friendship_theorem]
u:27 [in Friendship.friendship_theorem]
u:28 [in Friendship.statement_reduction]
u:30 [in Friendship.combinatorics]
u:31 [in Friendship.statement_reduction]
u:32 [in Friendship.combinatorics]
u:33 [in Friendship.combinatorics]
u:34 [in Friendship.statement_reduction]
u:36 [in Friendship.combinatorics]
u:36 [in Friendship.statement_reduction]
u:39 [in Friendship.statement_reduction]
u:41 [in Friendship.combinatorics]
u:41 [in Friendship.statement_reduction]
u:43 [in Friendship.combinatorics]
u:44 [in Friendship.statement_reduction]
u:47 [in Friendship.combinatorics]
u:47 [in Friendship.statement_reduction]
u:50 [in Friendship.combinatorics]
u:52 [in Friendship.combinatorics]
u:57 [in Friendship.combinatorics]
u:6 [in Friendship.statement_reduction]
u:61 [in Friendship.combinatorics]
u:62 [in Friendship.combinatorics]
u:7 [in Friendship.friendship_theorem]
u:76 [in Friendship.combinatorics]
u:80 [in Friendship.combinatorics]
u:81 [in Friendship.combinatorics]
u:82 [in Friendship.combinatorics]
u:83 [in Friendship.combinatorics]
V
v:100 [in Friendship.combinatorics]v:101 [in Friendship.combinatorics]
v:105 [in Friendship.combinatorics]
v:106 [in Friendship.combinatorics]
v:107 [in Friendship.combinatorics]
v:11 [in Friendship.friendship_theorem]
v:111 [in Friendship.combinatorics]
v:112 [in Friendship.combinatorics]
v:113 [in Friendship.combinatorics]
v:115 [in Friendship.combinatorics]
v:116 [in Friendship.combinatorics]
v:117 [in Friendship.combinatorics]
v:119 [in Friendship.combinatorics]
v:120 [in Friendship.combinatorics]
v:121 [in Friendship.combinatorics]
v:123 [in Friendship.combinatorics]
v:124 [in Friendship.combinatorics]
v:125 [in Friendship.combinatorics]
v:127 [in Friendship.combinatorics]
v:128 [in Friendship.combinatorics]
v:129 [in Friendship.combinatorics]
v:131 [in Friendship.combinatorics]
v:132 [in Friendship.combinatorics]
v:133 [in Friendship.combinatorics]
v:135 [in Friendship.combinatorics]
v:136 [in Friendship.combinatorics]
v:137 [in Friendship.combinatorics]
v:139 [in Friendship.combinatorics]
v:14 [in Friendship.friendship_theorem]
v:14 [in Friendship.statement_reduction]
v:140 [in Friendship.combinatorics]
v:141 [in Friendship.combinatorics]
v:143 [in Friendship.combinatorics]
v:144 [in Friendship.combinatorics]
v:145 [in Friendship.combinatorics]
v:146 [in Friendship.combinatorics]
v:147 [in Friendship.combinatorics]
v:148 [in Friendship.combinatorics]
v:149 [in Friendship.combinatorics]
v:150 [in Friendship.combinatorics]
v:151 [in Friendship.combinatorics]
v:153 [in Friendship.combinatorics]
v:18 [in Friendship.friendship_theorem]
v:19 [in Friendship.statement_reduction]
v:22 [in Friendship.statement_reduction]
v:24 [in Friendship.statement_reduction]
v:25 [in Friendship.friendship_theorem]
v:28 [in Friendship.friendship_theorem]
v:29 [in Friendship.statement_reduction]
V:3 [in Friendship.matrix_lemmas]
v:32 [in Friendship.statement_reduction]
v:34 [in Friendship.combinatorics]
v:35 [in Friendship.statement_reduction]
v:37 [in Friendship.combinatorics]
v:37 [in Friendship.statement_reduction]
v:40 [in Friendship.statement_reduction]
v:42 [in Friendship.combinatorics]
v:42 [in Friendship.statement_reduction]
v:44 [in Friendship.combinatorics]
v:45 [in Friendship.statement_reduction]
v:48 [in Friendship.combinatorics]
v:48 [in Friendship.statement_reduction]
v:51 [in Friendship.combinatorics]
v:53 [in Friendship.combinatorics]
v:54 [in Friendship.combinatorics]
v:55 [in Friendship.combinatorics]
v:58 [in Friendship.combinatorics]
v:59 [in Friendship.combinatorics]
v:63 [in Friendship.combinatorics]
v:7 [in Friendship.statement_reduction]
v:8 [in Friendship.friendship_theorem]
v:99 [in Friendship.combinatorics]
W
wAdjU:40 [in Friendship.combinatorics]w:15 [in Friendship.friendship_theorem]
w:26 [in Friendship.friendship_theorem]
w:31 [in Friendship.combinatorics]
w:33 [in Friendship.statement_reduction]
w:35 [in Friendship.combinatorics]
w:39 [in Friendship.combinatorics]
w:49 [in Friendship.statement_reduction]
w:77 [in Friendship.combinatorics]
w:8 [in Friendship.statement_reduction]
X
x2:10 [in Friendship.divisibility]x:102 [in Friendship.combinatorics]
x:103 [in Friendship.combinatorics]
x:122 [in Friendship.combinatorics]
x:126 [in Friendship.combinatorics]
x:130 [in Friendship.combinatorics]
x:134 [in Friendship.combinatorics]
x:138 [in Friendship.combinatorics]
x:14 [in Friendship.divisibility]
x:142 [in Friendship.combinatorics]
x:17 [in Friendship.statement_reduction]
x:20 [in Friendship.statement_reduction]
x:27 [in Friendship.statement_reduction]
x:49 [in Friendship.combinatorics]
x:55 [in Friendship.divisibility]
x:60 [in Friendship.combinatorics]
x:71 [in Friendship.combinatorics]
x:72 [in Friendship.combinatorics]
x:73 [in Friendship.combinatorics]
x:9 [in Friendship.divisibility]
x:98 [in Friendship.combinatorics]
Z
z:20 [in Friendship.adj2_matrix]z:21 [in Friendship.adj2_matrix]
z:22 [in Friendship.adj2_matrix]
other
α:87 [in Friendship.combinatorics]α:88 [in Friendship.combinatorics]
α:89 [in Friendship.combinatorics]
α:90 [in Friendship.combinatorics]
α:91 [in Friendship.combinatorics]
α:92 [in Friendship.combinatorics]
λs:10 [in Friendship.square_char_poly]
λs:20 [in Friendship.square_char_poly]
λ0:80 [in Friendship.square_char_poly]
λ0:81 [in Friendship.square_char_poly]
λ0:82 [in Friendship.square_char_poly]
λ0:83 [in Friendship.square_char_poly]
λ0:84 [in Friendship.square_char_poly]
λ0:85 [in Friendship.square_char_poly]
λ:18 [in Friendship.square_char_poly]
λ:19 [in Friendship.adj2_matrix]
λ:21 [in Friendship.divisibility]
λ:23 [in Friendship.square_char_poly]
λ:24 [in Friendship.square_char_poly]
λ:25 [in Friendship.square_char_poly]
λ:38 [in Friendship.square_char_poly]
λ:39 [in Friendship.square_char_poly]
λ:40 [in Friendship.square_char_poly]
λ:41 [in Friendship.square_char_poly]
λ:45 [in Friendship.square_char_poly]
λ:46 [in Friendship.square_char_poly]
λ:47 [in Friendship.square_char_poly]
λ:48 [in Friendship.square_char_poly]
λ:49 [in Friendship.square_char_poly]
λ:50 [in Friendship.square_char_poly]
λ:51 [in Friendship.square_char_poly]
λ:52 [in Friendship.square_char_poly]
λ:53 [in Friendship.square_char_poly]
λ:54 [in Friendship.square_char_poly]
λ:55 [in Friendship.square_char_poly]
λ:56 [in Friendship.square_char_poly]
λ:57 [in Friendship.square_char_poly]
λ:68 [in Friendship.square_char_poly]
λ:69 [in Friendship.square_char_poly]
λ:70 [in Friendship.square_char_poly]
λ:71 [in Friendship.square_char_poly]
λ:72 [in Friendship.square_char_poly]
λ:73 [in Friendship.square_char_poly]
λ:74 [in Friendship.square_char_poly]
λ:75 [in Friendship.square_char_poly]
λ:76 [in Friendship.square_char_poly]
μs':13 [in Friendship.adj2_matrix]
μs':17 [in Friendship.adj2_matrix]
μs':29 [in Friendship.square_char_poly]
μs':36 [in Friendship.square_char_poly]
μs:10 [in Friendship.matrix_lemmas]
μs:17 [in Friendship.divisibility]
μs:21 [in Friendship.square_char_poly]
μs:9 [in Friendship.square_char_poly]
μ':33 [in Friendship.square_char_poly]
μ':34 [in Friendship.square_char_poly]
μ':35 [in Friendship.square_char_poly]
μ:11 [in Friendship.matrix_lemmas]
μ:12 [in Friendship.matrix_lemmas]
μ:13 [in Friendship.matrix_lemmas]
μ:14 [in Friendship.matrix_lemmas]
μ:14 [in Friendship.adj2_matrix]
μ:15 [in Friendship.matrix_lemmas]
μ:15 [in Friendship.adj2_matrix]
μ:16 [in Friendship.matrix_lemmas]
μ:16 [in Friendship.adj2_matrix]
μ:17 [in Friendship.square_char_poly]
μ:17 [in Friendship.matrix_lemmas]
μ:18 [in Friendship.matrix_lemmas]
μ:18 [in Friendship.adj2_matrix]
μ:19 [in Friendship.matrix_lemmas]
μ:20 [in Friendship.divisibility]
μ:22 [in Friendship.divisibility]
μ:23 [in Friendship.divisibility]
μ:24 [in Friendship.divisibility]
μ:24 [in Friendship.adj2_matrix]
μ:25 [in Friendship.adj2_matrix]
μ:26 [in Friendship.square_char_poly]
μ:26 [in Friendship.adj2_matrix]
μ:27 [in Friendship.square_char_poly]
μ:28 [in Friendship.square_char_poly]
μ:29 [in Friendship.adj2_matrix]
μ:30 [in Friendship.square_char_poly]
μ:30 [in Friendship.adj2_matrix]
μ:31 [in Friendship.square_char_poly]
μ:31 [in Friendship.adj2_matrix]
μ:32 [in Friendship.square_char_poly]
μ:32 [in Friendship.adj2_matrix]
μ:33 [in Friendship.adj2_matrix]
μ:34 [in Friendship.adj2_matrix]
μ:35 [in Friendship.adj2_matrix]
μ:36 [in Friendship.adj2_matrix]
μ:37 [in Friendship.square_char_poly]
μ:37 [in Friendship.divisibility]
μ:37 [in Friendship.adj2_matrix]
μ:38 [in Friendship.divisibility]
μ:38 [in Friendship.adj2_matrix]
μ:39 [in Friendship.divisibility]
μ:39 [in Friendship.adj2_matrix]
μ:40 [in Friendship.divisibility]
μ:40 [in Friendship.adj2_matrix]
μ:41 [in Friendship.divisibility]
μ:41 [in Friendship.adj2_matrix]
μ:42 [in Friendship.divisibility]
μ:42 [in Friendship.adj2_matrix]
μ:43 [in Friendship.divisibility]
μ:43 [in Friendship.adj2_matrix]
μ:44 [in Friendship.divisibility]
μ:44 [in Friendship.adj2_matrix]
μ:45 [in Friendship.divisibility]
μ:45 [in Friendship.adj2_matrix]
μ:46 [in Friendship.divisibility]
μ:46 [in Friendship.adj2_matrix]
μ:47 [in Friendship.divisibility]
μ:47 [in Friendship.adj2_matrix]
μ:48 [in Friendship.divisibility]
μ:48 [in Friendship.adj2_matrix]
μ:49 [in Friendship.adj2_matrix]
μ:50 [in Friendship.adj2_matrix]
μ:51 [in Friendship.adj2_matrix]
μ:52 [in Friendship.adj2_matrix]
μ:59 [in Friendship.adj2_matrix]
μ:60 [in Friendship.adj2_matrix]
μ:61 [in Friendship.adj2_matrix]
μ:65 [in Friendship.adj2_matrix]
μ:66 [in Friendship.adj2_matrix]
μ:67 [in Friendship.adj2_matrix]
μ:68 [in Friendship.adj2_matrix]
μ:77 [in Friendship.square_char_poly]
μ:78 [in Friendship.square_char_poly]
μ:79 [in Friendship.square_char_poly]
Variable Index
C
casts.R [in Friendship.matrix_casts]D
det_dotmul.R [in Friendship.matrix_lemmas]div.k [in Friendship.divisibility]
div.n [in Friendship.divisibility]
S
sim_char_poly.F [in Friendship.matrix_lemmas]Library Index
A
adj2_matrixB
bigopsC
combinatoricsD
divisibilityF
friendship_theoremM
matrix_lemmasmatrix_casts
S
square_char_polystatement_reduction
Lemma Index
A
adjT_cover_noT [in Friendship.combinatorics]adjT_subs_cover [in Friendship.combinatorics]
adj_mtx_char_poly [in Friendship.adj2_matrix]
adj_diag_block_form [in Friendship.adj2_matrix]
adj'_card [in Friendship.combinatorics]
adj'_and_t_disj [in Friendship.combinatorics]
adj'_and_tU [in Friendship.combinatorics]
adj'_disjoint [in Friendship.combinatorics]
adj2_eq [in Friendship.combinatorics]
adj2_block_form [in Friendship.adj2_matrix]
all_covered [in Friendship.combinatorics]
all2_nseq [in Friendship.divisibility]
almost_almost_regular [in Friendship.combinatorics]
almost_regular_eq [in Friendship.combinatorics]
almost_regular_leq [in Friendship.combinatorics]
andWl [in Friendship.combinatorics]
andWr [in Friendship.combinatorics]
Asqrt [in Friendship.combinatorics]
A_tr [in Friendship.combinatorics]
A_diag [in Friendship.combinatorics]
A'_tr [in Friendship.combinatorics]
A2_off_diag [in Friendship.combinatorics]
A2_diag [in Friendship.combinatorics]
B
big_bool [in Friendship.bigops]C
card_cover [in Friendship.combinatorics]cast_eq [in Friendship.combinatorics]
charpoly_uconj [in Friendship.matrix_lemmas]
char_poly_adj2 [in Friendship.adj2_matrix]
Colr [in Friendship.statement_reduction]
CoUnique [in Friendship.statement_reduction]
Co_sym [in Friendship.combinatorics]
D
det_block [in Friendship.matrix_lemmas]diagonalizable_m [in Friendship.adj2_matrix]
disjoint_cover [in Friendship.combinatorics]
dist2_card [in Friendship.combinatorics]
dotmul [in Friendship.matrix_lemmas]
D_m_P_eq [in Friendship.adj2_matrix]
E
exists_hub_sig [in Friendship.combinatorics]exists_hub [in Friendship.combinatorics]
F
Feq [in Friendship.combinatorics]fls [in Friendship.combinatorics]
Friendship [in Friendship.friendship_theorem]
Friendship' [in Friendship.friendship_theorem]
f_total_agrees_with_f [in Friendship.statement_reduction]
I
idomain_sqrt [in Friendship.divisibility]K
kge1 [in Friendship.combinatorics]kn_1 [in Friendship.divisibility]
k_is_2 [in Friendship.divisibility]
k_not_2 [in Friendship.combinatorics]
k_not_1 [in Friendship.combinatorics]
L
lams_prod [in Friendship.adj2_matrix]M
map_adj_inj [in Friendship.combinatorics]map_adj_im [in Friendship.combinatorics]
mulmx_castmx [in Friendship.matrix_casts]
N
nge1 [in Friendship.combinatorics]nk [in Friendship.combinatorics]
no_hub [in Friendship.combinatorics]
n_eq [in Friendship.combinatorics]
P
polys_and_squares_technical_lemma [in Friendship.square_char_poly]P_unit [in Friendship.adj2_matrix]
R
regular [in Friendship.combinatorics]S
scalar_mx_castmx [in Friendship.matrix_casts]simmx_charpoly [in Friendship.matrix_lemmas]
split_tuples [in Friendship.square_char_poly]
summx_castmx [in Friendship.matrix_casts]
sum_of_roots [in Friendship.divisibility]
T
tr_adj_rel_nat [in Friendship.divisibility]tr_adj_rel [in Friendship.divisibility]
tr_castmx [in Friendship.matrix_casts]
T_size [in Friendship.combinatorics]
V
viete_sum [in Friendship.matrix_lemmas]v_not_in_adj_u [in Friendship.combinatorics]
Section Index
A
adj2_matrix_props [in Friendship.adj2_matrix]B
bigops [in Friendship.bigops]C
casts [in Friendship.matrix_casts]D
det_dotmul [in Friendship.matrix_lemmas]div [in Friendship.divisibility]
F
friendship_sec.assume_contra [in Friendship.combinatorics]friendship_sec [in Friendship.combinatorics]
S
sim_char_poly [in Friendship.matrix_lemmas]square_polys [in Friendship.square_char_poly]
StatementReduction [in Friendship.statement_reduction]
Definition Index
A
A [in Friendship.combinatorics]adj [in Friendship.combinatorics]
adj_cover [in Friendship.combinatorics]
adj' [in Friendship.combinatorics]
adj2 [in Friendship.adj2_matrix]
adj2n [in Friendship.divisibility]
adj2_diag [in Friendship.adj2_matrix]
A' [in Friendship.combinatorics]
C
Co [in Friendship.statement_reduction]Col [in Friendship.statement_reduction]
Cor [in Friendship.statement_reduction]
co_nodiag [in Friendship.statement_reduction]
co_set_gt0 [in Friendship.statement_reduction]
D
deg [in Friendship.combinatorics]diag_vec [in Friendship.adj2_matrix]
dist2 [in Friendship.combinatorics]
F
f_total [in Friendship.statement_reduction]I
idP' [in Friendship.statement_reduction]is_square_root [in Friendship.adj2_matrix]
K
k [in Friendship.combinatorics]L
lams [in Friendship.adj2_matrix]list_insert [in Friendship.square_char_poly]
M
matN [in Friendship.adj2_matrix]N
n [in Friendship.combinatorics]nn [in Friendship.combinatorics]
P
P [in Friendship.adj2_matrix]R
R [in Friendship.combinatorics]R [in Friendship.adj2_matrix]
RR [in Friendship.square_char_poly]
T
T_elem [in Friendship.combinatorics]T_elem [in Friendship.statement_reduction]
| 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 | (600 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (473 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 | (5 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 | (9 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 | (72 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 | (10 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 | (31 entries) |