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

State before:
m k : ℕ
f : ℕ → ZMod m
⊢ prod_seq 1 k f = f k
Tactic:
rewrite [prod_seq_step, prod_seq_base, add_zero, mul_comm, Theorem_7_3_6_7]
State after:
m k : ℕ
f : ℕ → ZMod m
⊢ f k = f k

State before:
m k : ℕ
f : ℕ → ZMod m
⊢ f k = f k
Tactic:
rfl
State after:
no goals