An irrational power of an irrational number need not be irrational

This file proves that there exist irrational numbers a, b such that a^b is rational.

We use the following famous argument (based on the law of excluded middle and irrationality of √2). Consider c = √2^√2. If c is rational, we are done. If c is irrational, then c^√2 = 2 is rational, so we are done.

theorem Counterexample.not_irrational_rpow : ¬∀ (a b : ℝ), Irrational a → Irrational b → 0 < a → Irrational (a ^ b)

There exist irrational a, b with rational a^b. Note that the positivity assumption on a is imposed because of the definition of rpow for negative bases. See Real.rpow_def_of_neg for more details.