pi

Stream: mathlib4

[BANGJI HU]

Has pi been formalized as a transcendental number?

[BANGJI HU]

Has pi been formalized as a transcendental number?

import Mathlib

open Real Polynomial

theorem pi_transcendental : Transcendental ℚ π := by
sorry

[Michael Rothgang]

#6718 (which is still on its way to mathlib) proves this (and a much more general statement). I think the transcendence of e or pi has been proven separately, but don't remember the details. "Lindemann-Weierstrass" is a good keyword to search for.

[Bhavik Mehta]

There's the irrationality of pi in mathlib, but the special case of Lindemann-Weierstrass for pi isn't in mathlib yet: docs#irrational_pi

[BANGJI HU]

also transcendental is irrational is also proved

[Michael Rothgang]

Is this a question or a statement? Can you please be more precise in your questions? You have been told this before.

[Michael Rothgang]

On your question: loogle can easily answer this - search for all results mentioning transcendental and irrational, and you'll find it. Would you like to try?

[Michael Rothgang]

Loogle for Transcendental, "Irrational" and you'll find docs#Transcendental.irrational

[BANGJI HU]

It has been proven that transcendental numbers are irrational and that pi is irrational. I think I can combine them.

[Michael Rothgang]

Deducing "transcendental numbers are irrational and pi is irrational, hence pi is transcendental" is not a correct argument: that statement is false. Can you think of a counterexample? (What do you need to do to exhibit one?)

[BANGJI HU]

If I am from New York, it can be concluded that I am from the United States, but if I am from the United States, it does not necessarily mean that I am from New York.？