Eisenstein trace zero product

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Data.Finset.Card
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5




theorem _root_.D1Bound5.eisenstein_trace_zero_product (z w : QuadInt 1 1)
    (hz : 2 * z.re + z.im = 0) (hw : 2 * w.re + w.im = 0) :
    z * w + 1 = ((1 - 3 * z.re * w.re : ℤ) : QuadInt 1 1) := by sorry







end D1Bound5
end