Theorem: Fin.sum_zero (GMLInit/Data/Fin/Basic.lean)

State before:
n : Nat
α : Type u_1
inst✝¹ : Add α
inst✝ : OfNat α 0
f : Fin 0 → α
⊢ sum f = 0
Tactic:
simp [sum]
State after:
no goals