Trace zero tau one product

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5
















theorem _root_.D1Bound5.trace_zero_tau_one_product {nu : ℤ} (z w : QuadInt 1 nu)
    (hz : 2 * z.re + z.im = 0) (hw : 2 * w.re + w.im = 0) :
    z * w + 1 = ((1 - (4 * nu - 1) * z.re * w.re : ℤ) : QuadInt 1 nu) := by sorry







end D1Bound5
end