Helper

Zp_mulrn_eqmod

Section Top-level

Type Lemma

Proof Lines 9

Lemma Zp_mulrn_eqmod (n : nat) (n_gt1 : (1 < n)%N) (m1 : 'Z_n) (m2 : nat) : (m1 : nat) * m2 = (m1 *+ m2)%R %[mod n].

Helper: nat mult of Z_n element by nat equals Z_n scalar mult mod n

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...