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

State before:
m a i : ℕ
⊢ G m a i = a * i % m
Tactic:
rfl
State after:
no goals