Transcendental ℚ π

Stream: Is there code for X?

[张守信(Shouxin Zhang)]

It seems a good resultTranscendental ℤ π has been proved in "#6718". But the API for this classic result doesn't seem to have been pushed to master yet.

Is this easy to prove using the latest library API?

[Junyan Xu]

It follows from this lemma that Transcendental ℤ π is equivalent to Transcendental ℚ π. The PR was merged 7 hours ago and the lemma doesn't yet show up in the online docs.

[张守信(Shouxin Zhang)]

Junyan Xu said:

It follows from this lemma that Transcendental ℤ π is equivalent to Transcendental ℚ π. The PR was merged 7 hours ago and the lemma doesn't yet show up in the online docs.

Thank you for your reply! I will take a careful look once I get free from my semester assignments. :grinning_face_with_smiling_eyes: