Transcendence of π

The main theorem: the complex number π (and hence the real number π) is transcendental over ℚ, assembling the analytic and algebraic estimates of the preceding modules into Niven's contradiction argument.

theorem isAlgebraic_pi_of_not_transcendental_pi (hpi : ¬Transcendental ℚ ↑Real.pi) : IsAlgebraic ℚ ↑Real.pi

If π is not transcendental over ℚ, then π is algebraic over ℚ.

theorem isAlgebraic_I_mul_pi_of_isAlgebraic_pi (hpi : IsAlgebraic ℚ ↑Real.pi) : IsAlgebraic ℚ (↑Real.pi * Complex.I)

If π is algebraic over ℚ, then so is π i.

theorem exists_monic_rat_poly_aeval_Ipi_eq_zero (hpi : IsAlgebraic ℚ (↑Real.pi * Complex.I)) : ∃ (B : Polynomial ℚ), B.Monic ∧ (Polynomial.aeval (↑Real.pi * Complex.I)) B = 0

If π i is algebraic over ℚ, there is a monic rational polynomial vanishing at π i.

theorem IsTranscendentalPi : Transcendental ℚ ↑Real.pi

The complex number π is transcendental over ℚ.

theorem IsTranscendentalPiReal : Transcendental ℚ Real.pi

The real number π is transcendental over ℚ.