Theorem: SimpleGraph.degOn_empty (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Degree.lean)

State before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ a : α
⊢ G.degOn ∅ a = 0
Tactic:
simp [degOn]
State after:
no goals