Square division in full ring

import Mathlib.Algebra.Polynomial.Monic
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Squarefree.Basic
import Mathlib.Data.Int.GCD
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
open scoped NumberField
open Module Polynomial

namespace D1Bound5

variable {K : Type*} [Field K]



variable [NumberField K]


theorem _root_.D1Bound5.square_division_in_full_ring {tau nu : ℤ}
    (e : QuadInt tau nu ≃+* 𝓞 K) (a m : ℤ) (ha : a ≠ 0)
    {z : QuadInt tau nu} (hz : z*z = ((a*a*m : ℤ) : QuadInt tau nu)) :
    ∃ y : QuadInt tau nu, (a : QuadInt tau nu)*y = z := by sorry







end D1Bound5
end