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

State before:
m a i : ℕ
⊢ Ginv m a i = G m (inv_mod m a) i
Tactic:
rfl
State after:
no goals