11.24. SharpFiveExponentials.Statement🔗

def Conjecture : Prop :=
  ∀ (x y : Fin 2 → ℂ) (α γ : ℂ) (β : Fin 2 → Fin 2 → ℂ),
    LinearIndependent ℚ x → LinearIndependent ℚ y →
    IsAlgebraic ℚ α → IsAlgebraic ℚ γ → γ ≠ 0 →
    (∀ i j, IsAlgebraic ℚ (β i j)) →
    (∀ i j, IsAlgebraic ℚ (Complex.exp (x i * y j - β i j))) →
    IsAlgebraic ℚ (Complex.exp (γ * x 1 / x 0 - α)) →
    (∀ i j, x i * y j = β i j) ∧ γ * x 1 = α * x 0

end SharpFiveExponentials