11.23. FourExponentials.Statement🔗

def Conjecture : Prop :=
  ∀ x y : Fin 2 → ℂ, LinearIndependent ℚ x → LinearIndependent ℚ y →
    ∃ i j, Transcendental ℚ (Complex.exp (x i * y j))

/-- The normalized form, with the first pair written as 1 and t. -/

def NormalizedConjecture : Prop :=
  ∀ (t : ℂ) (y : Fin 2 → ℂ),
    LinearIndependent ℚ ![1, t] → LinearIndependent ℚ y →
    ∃ j, Transcendental ℚ (Complex.exp (y j)) ∨
      Transcendental ℚ (Complex.exp (t * y j))

end FourExponentials