Existence_of_Rational_Powers_of_Irrational_Numbers
Provedexistence-of-rational-powers-of-irrational-numbersnumber-theoryproofwikiretryroots-of-numbers
There exist irrational numbers a,b such that a^b is rational.
Preamble
import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Data.Set.Basic def Irrational (x : ℝ) : Prop := x ∉ Set.range ((↑) : ℚ → ℝ)
Formal statement
theorem Existence_of_Rational_Powers_of_Irrational_Numbers : ∃ a b : ℝ, Irrational a ∧ Irrational b ∧ ¬ Irrational (a ^ b) := by sorry