coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Laurent Thery <Laurent.Thery AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Intermixing of Nat and Z
- Date: Fri, 18 Dec 2020 12:47:12 +0100
On 12/18/20 3:30 AM, mukesh tiwari wrote:
> I need to use Euler_exp_totient [2]
Hi,
I don't know if this can help. Your theorem is also available in the
library CoqPrime in a Z version.
https://github.com/thery/coqprime/blob/d0ee27bc9e98254392331583e94a3eea32c2a5d0/src/Coqprime/PrimalityTest/Zp.v#L367
--
Laurent
- [Coq-Club] Intermixing of Nat and Z, mukesh tiwari, 12/18/2020
- Re: [Coq-Club] Intermixing of Nat and Z, Laurent Thery, 12/18/2020
- Re: [Coq-Club] Intermixing of Nat and Z, mukesh tiwari, 12/29/2020
- Re: [Coq-Club] Intermixing of Nat and Z, Laurent Thery, 12/18/2020
Archive powered by MHonArc 2.6.19+.