Commit 2025-05-15 14:23 b34b1c01

feat(Combinatorics/SimpleGraph): add IsCompleteMultipartite definition and related results (#24092) A graph is complete multipartite if non-adjacency is transitive. We add this definition, the associated Setoid, and the graph isomorphism to the corresponding completeMultipartiteGraph. We also add the definition of a minimal witness to non-complete-multipartiteness: IsP2Complement. We will need this for our proof of the Andrásfai–Erdős–Sós theorem, where the interesting case is when the graph is not complete-multipartite.