Library Stdlib.Zmod.ZstarDef

From Stdlib Require Import ZArith Zdivisibility ZModOffset Lia.
From Stdlib Require Import Bool.Bool Lists.List.
Import ListNotations.
Local Open Scope Z_scope.
From Stdlib Require Import ZmodDef.

Module Zstar.
Import Zmod.

#[projections(primitive)]
Record Zstar (m : Z) := mk {
  Private_to_Z : Z ;
  Private_range : Is_true (ZmodDef.Zmod.small Private_to_Z m &&
                             (Z.gcd Private_to_Z m =? 1)) }.
Arguments Private_to_Z {m}.
#[global] Add Printing Constructor Zstar.

Coercion to_Zmod {m : Z} (a : Zstar m) : Zmod m := Zmod.of_small_Z m (Private_to_Z a).

Definition of_coprime_Zmod_dep {m} (a : Zmod m) (H : True -> Z.gcd a m = 1) : Zstar m.
Defined.

Definition of_Zmod {m} (x : Zmod m) : Zstar m.
Defined.

Definition eqb {m} (x y : Zstar m) := Zmod.eqb x y.

Definition one {m} : Zstar m := of_Zmod Zmod.one.

Definition opp {m} (x : Zstar m) : Zstar m := of_Zmod (Zmod.opp x).

Definition abs {m} (x : Zstar m) : Zstar m := of_Zmod (Zmod.abs x).

Definition mul {m} (a b : Zstar m) : Zstar m.
Defined.

Definition inv {m} (x : Zstar m) : Zstar m := of_Zmod (Zmod.inv x).

Definition div {m} (x y : Zstar m) : Zstar m := mul x (inv y).

Definition pow {m} (a : Zstar m) z := of_Zmod (Zmod.pow a z).

Definition prod {m} xs : Zstar m := List.fold_right mul one xs.

Definition elements m : list (Zstar m) :=
  if Z.eqb m 0 then [one; opp one] else
  map of_Zmod (filter (fun x : Zmod _ => Z.eqb (Z.gcd x m) 1) (Zmod.elements m)).

Definition positives m :=
  map of_Zmod (filter (fun x : Zmod m => Z.gcd x m =? 1) (Zmod.positives m)).

Definition negatives m :=
  map of_Zmod (filter (fun x : Zmod m => Z.gcd x m =? 1) (Zmod.negatives m)).

End Zstar.

Notation Zstar := Zstar.Zstar.