Quad Int — four norm

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5



namespace QuadInt

variable {tau nu : ℤ}






theorem _root_.D1Bound5.QuadInt.four_norm (z : QuadInt tau nu) :
    4*z.norm = (2*z.re+tau*z.im)^2 + discriminant tau nu*z.im^2 := by sorry











end QuadInt
end D1Bound5
end