Theorems · Definition · combinatorics

Matrix.compl

{α : Type u_1} → {V : Type u_2} → [Zero α] → [One α] → [DecidableEq α] → [DecidableEq V] → Matrix V V α → Matrix V V α

For A : Matrix V V α, A.compl is supposed to be the adjacency matrix of the complement graph of the graph induced by A.adjMatrix.

Defined in

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Cited by

17 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

ZeroOneDecidableEqDecidableEq