Quad Int — norm formula

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.norm_formula (z : QuadInt tau nu) :
    z.norm = z.re^2 + tau*z.re*z.im + nu*z.im^2 := by sorry













end QuadInt
end D1Bound5
end