case Adj.h.h.a
V : Type u_2
α : Type u_1
β : Type ?u.18379
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
v w : V
⊢ Adj (toGraph (_ : IsAdjMatrix (Matrix.compl A))) v w ↔ Adj (toGraph hᶜ) v w
V : Type u_2
α : Type u_1
β : Type ?u.18379
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
⊢ toGraph (_ : IsAdjMatrix (Matrix.compl A)) = toGraph hᶜ
ext (v w)
no goals
case Adj.h.h.a
V : Type u_2
α : Type u_1
β : Type ?u.18379
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : IsAdjMatrix A
v w : V
⊢ Adj (toGraph (_ : IsAdjMatrix (Matrix.compl A))) v w ↔ Adj (toGraph hᶜ) v w
cases' h.zero_or_one v w with h h <;> by_cases hvw : v = w <;> simp [Matrix.compl, h, hvw]