no goals
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a b : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 0 ↔ ¬e ∈ incidenceSet G a
simp only [incMatrix_apply, Set.indicator_apply_eq_zero, Pi.one_apply, one_ne_zero]