Skip to content

Latest commit

 

History

History
24 lines (16 loc) · 1.13 KB

README.md

File metadata and controls

24 lines (16 loc) · 1.13 KB
Raw

Asymptotic Lower Bound of Euler Totient Function φ

Overview

This repository contains a Coq proof of:

where is Euler's totient function.

Part of code is modified from Daniel de Rauglaudre's proof.

Build Instructions

Compilation requires Coq and the Interval package. We recommend installing both with the opam package manager using the commands below.

opam update
opam install coq coq-interval

Run make to compile the proofs. We have tested compilation with Coq versions 8.10.1-8.16.1 and Interval versions 4.0.0-4.6.1.

To use this repository as a library, run opam pin coq-euler https://github.com/taorunz/euler.git. Then, to import files into your Coq project, use Require Import euler.FILENAME. Subsequent updates can be pulled using opam install coq-euler.