Helper
expr_modn
Signature
Lemma expr_modn (k : nat) : g ^+ k = g ^+ (k %% n)%N.
Description
Exponentiation of g depends only on exponent mod n
Uses (0)
This lemma does not use any other lemmas from the stats.
Used By (0)
No lemmas in the stats use this lemma.
Coq Source Code
View on GitHubLoading source code...