Theorems · Inductive type · combinatorics

Matrix.IsAdjMatrix

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

A : Matrix V V α is qualified as an "adjacency matrix" if (1) every entry of A is 0 or 1, (2) A is symmetric, (3) every diagonal entry of A is 0.

Defined in

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Cited by

28 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

ZeroOne