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

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