no goals
V : Type u_2
α : Type u_1
β : Type ?u.6455
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
i j : V
⊢ ¬A i j = 0 ↔ A i j = 1
rw [← apply_ne_one_iff h, Classical.not_not]