Skip to content
/ euler Public

Asymptotic Upper Bound of Euler Totient Function φ

Notifications You must be signed in to change notification settings

taorunz/euler

Repository files navigation

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.

About

Asymptotic Upper Bound of Euler Totient Function φ

Resources

Stars

Watchers

Forks

Languages