Library Stdlib.Zmod.ZstarDef
From Stdlib Require Import NArith 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.
From Stdlib Require Import Bool.Bool Lists.List.
Import ListNotations.
Local Open Scope Z_scope.
From Stdlib Require Import ZmodDef.
Module Zstar.
Import Zmod.
See ZStarDef.Zmod.Zmod for notes on efficient construction
#[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.
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.
Inverses and division have a canonical definition
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).
Powers
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.
Enumerating elements
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.