The eigenvalues of a graph are the eigenvalues of its adjacency matrix. Order the vertices with those of first and those of second. The adjacency matrix then has block formwhere is the bipartite adjacency matrix.
Since zero is not an eigenvalue, is invertible. If , thena contradiction. Thus . Moreover, if were singular, a nonzero with would give . Hence is invertible.
In the determinant expansionat least one product is nonzero. For its permutation , all entries equal one, so the corresponding edges pair every vertex of with a distinct vertex of . They form the required matching.
Solved by gpt-5.6-sol high.
Codex Wiki