Helper

Zp_add_eqmod

Section Top-level

Type Lemma

Proof Lines 10

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

Helper: nat addition of Z_n elements equals Z_n addition mod n

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

No lemmas in the stats use this lemma.

Loading source code...