English
Let G be a finite simple graph on vertex set V and α a semiring. For every n ∈ ℕ and u,v ∈ V, the (u,v)-entry of the n-th power of the adjacency matrix equals the number of walks of length n from u to v in G, where the matrix is taken over α.
Русский
Пусть G — конечный простой граф на множестве вершин V, и α — полугруппа с умножением. Для любого n ∈ ℕ и вершин u, v ∈ V элемент (u,v) в A^n, где A — матрица смежности G над α, равен числу ходов длины n от u к v в G.
LaTeX
$$$ (\operatorname{adjMatrix}_{\alpha}(G))^n_{uv} = \#\{ p : \text{Walk}(u,v) \mid \operatorname{length}(p) = n \} $$$
Lean4
theorem adjMatrix_pow_apply_eq_card_walk [DecidableEq V] [Semiring α] (n : ℕ) (u v : V) :
(G.adjMatrix α ^ n) u v = Fintype.card {p : G.Walk u v | p.length = n} :=
by
rw [card_set_walk_length_eq]
induction n generalizing u v with
| zero => obtain rfl | h := eq_or_ne u v <;> simp [finsetWalkLength, *]
| succ n ih =>
simp only [pow_succ', finsetWalkLength, ih, adjMatrix_mul_apply]
rw [Finset.card_biUnion]
· norm_cast
simp only [Nat.cast_sum, card_map, neighborFinset_def]
apply Finset.sum_toFinset_eq_subtype
· rintro ⟨x, hx⟩ - ⟨y, hy⟩ - hxy
rw [Function.onFun, disjoint_iff_inf_le]
intro p hp
simp only [inf_eq_inter, mem_inter, mem_map, Function.Embedding.coeFn_mk] at hp
obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp
cases hp
simp at hxy
