English
The product incMatrix^T incMatrix is a matrix whose (a,b) entry is deg(a) if a=b, 1 if a and b are adjacent, and 0 otherwise.
Русский
Произведение incMatrix^T incMatrix — это матрица, у которой элемент (a,b) равен deg(a) если a=b, равен 1 если a и b смежны, и 0 иначе.
LaTeX
$$$\forall a,b,\; (G.incMatrix R)^T * (G.incMatrix R) a b = \begin{cases} \deg(a) & \text{если } a=b \\ 1 & \text{если } G.Adj a b \\ 0 & \text{иначе} \end{cases}$$$
Lean4
theorem incMatrix_mul_transpose [∀ a, Fintype (neighborSet G a)] :
G.incMatrix R * (G.incMatrix R)ᵀ = of fun a b => if a = b then (G.degree a : R) else if G.Adj a b then 1 else 0 :=
by
ext a b
dsimp
split_ifs with h h'
· subst b
exact incMatrix_mul_transpose_diag (R := R) G
· exact G.incMatrix_mul_transpose_apply_of_adj h'
·
simp only [Matrix.mul_apply, Matrix.transpose_apply, G.incMatrix_apply_mul_incMatrix_apply_of_not_adj h h',
sum_const_zero]
