Complete multipartite graphs
Abstract
Complete multipartite adjacency matrices and polynomial norms.
Theorem 1.1 (Symmetry of adjacency).
Lean statement: D5/S3/Combinatorics/Graph/MultipartiteCHS/Defs.adj_isHermitian
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/MultipartiteCHS/Defs.adj_isHermitian (✓ std3). ∎
Source. Repository-derived.
Commentary.
Vertices are pairs consisting of a part index and a vertex index within that part. Two vertices are adjacent precisely when their part indices differ. The real adjacency matrix is Hermitian, so its eigenvalues define the complete homogeneous symmetric polynomial and its real power norm.