no goals
V : Type u_2
α : Type u_1
β : Type ?u.3595
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
i j : V
⊢ ¬A i j = 1 ↔ A i j = 0
obtain h | h := h.zero_or_one i j <;> simp [h]