Quad Int — complex generator parameters

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Analysis.Complex.Norm
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5.QuadInt

open scoped QuadraticAlgebra

variable {tau nu : ℤ}




theorem _root_.D1Bound5.QuadInt.complex_generator_parameters (f : QuadInt tau nu →+* ℂ)
    (hi : (f QuadraticAlgebra.omega).im ≠ 0) :
    2*(f QuadraticAlgebra.omega).re = (tau : ℝ) ∧
    (f QuadraticAlgebra.omega).re^2 + (f QuadraticAlgebra.omega).im^2 = (nu : ℝ) ∧
    (discriminant tau nu : ℝ) = 4*(f QuadraticAlgebra.omega).im^2 := by sorry







end D1Bound5.QuadInt
end