Helper

Zp_unit_coprime

Section Zp_unit_extra

Type Lemma

Proof Lines 6

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

Uses unitZpE in reverse: (x%:R) \is a GRing.unit = coprime m x

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

No lemmas in the stats use this lemma.

Loading source code...