case a.h
V : Type u_2
α : Type u_1
β : Type ?u.79711
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : IsAdjMatrix A
inst✝ : DecidableEq α
i j : V
⊢ adjMatrix α (toGraph h) i j = A i j
V : Type u_2
α : Type u_1
β : Type ?u.79711
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : IsAdjMatrix A
inst✝ : DecidableEq α
⊢ adjMatrix α (toGraph h) = A
ext (i j)
no goals
case a.h
V : Type u_2
α : Type u_1
β : Type ?u.79711
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : IsAdjMatrix A
inst✝ : DecidableEq α
i j : V
⊢ adjMatrix α (toGraph h) i j = A i j
obtain h' | h' := h.zero_or_one i j <;> simp [h']