Quad Int — complex image

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_image (f : QuadInt tau nu →+* ℂ) (z : QuadInt tau nu) :
    f z = (z.re : ℂ)+(z.im : ℂ)*f QuadraticAlgebra.omega := by sorry









end D1Bound5.QuadInt
end