Helper

Zp_unitP

Section Zp_unit_extra

Type Lemma

Proof Lines 4

Lemma Zp_unitP (m : nat) (x : 'Z_m) : (1 < m)%N -> (x \is a GRing.unit) = coprime x m.

Equivalence form: unit status iff coprime (when m > 1)

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

No lemmas in the stats use this lemma.

Loading source code...