# Transcendental Numbers

This project is to prove several theorems in transcendental number theory:

- Countability argument: abstract existence of transcendental number;
- Liouvielle theorem and hence is transcendental;
- is transcendental;
- is transcendental.

## Part 1, countability argument

The main theorem is in algebraic_countable_over_Z.lean

```
theorem transcendental_number_exists : ∃ x : real, ¬ (is_algebraic ℤ x)
```

The other version is in algebraic_countable_over_Q.lean

```
theorem transcendental_number_exists : ∃ x : real, ¬ (is_algebraic ℚ x)
```

## Part 2, Liouville theorem and an explicit Liouville number

Definition of the explicit Liouville number is in liouville_theorem.lean

```
def α := ∑' n, ten_pow_n_fact_inverse n
```

The main theorem is in liouville_theorem.lean:

```
theorem liouville_numbers_transcendental : ∀ x : real, liouville_number x -> ¬(is_algebraic ℤ x)
theorem transcendental_α : transcendental α := liouville_numbers_transcendental α liouville_α
```

## Part 3, the transcendence of e

We defined e in e_transcendental.lean as :

```
def e : ℝ := real.exp 1
```

The main theorem is at e_transcendental.lean:

```
theorem e_transcendental : ¬ is_algebraic ℤ e :=
```

Almost immediately, we can prove

```
theorem e_irrational : irrational e
theorem e_pow_transcendental (n : ℕ) (hn : n ≥ 1) : transcendental (e^n)
theorem e_pow_n_irrational (n : ℕ) (hn : n ≥ 1) : irrational (e ^ n)
```

Please see this for an explanation of the proof of transcendence of $e$ with reference to Lean code.

I haven’t finished documentation (not even close), but you can click around the proves I documented so far at e_trans_helpers2.lean ande_transcendental.lean.