Helper

Zp_mulrn_nat

Section Top-level

Type Lemma

Proof Lines 6

Lemma Zp_mulrn_nat (n : nat) (n_gt1 : (1 < n)%N) (m : 'Z_n) (k : nat) : ((m *+ k)%R : nat) = (((m : nat) * k) %% (Zp_trunc n).+2)%N.

Helper: (m *+ k : 'Z_n) as nat equals (m * k) %% (Zp_trunc n).+2

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

No lemmas in the stats use this lemma.

Loading source code...