Theorem: HTPI.prod_seq_base (HTPILib/Chap7.lean)

State before:
m k : ℕ
f : ℕ → ZMod m
⊢ prod_seq 0 k f = [1]_m
Tactic:
rfl
State after:
no goals