Integral basis one gcd

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Data.Int.GCD
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination

section
open scoped NumberField
open Module

namespace D1Bound5

variable {K : Type*} [Field K] [NumberField K]


theorem _root_.D1Bound5.integral_basis_one_gcd (hK : finrank ℚ K = 2)
    (B : Basis (Fin 2) ℤ (𝓞 K)) :
    Int.gcd (B.repr 1 0) (B.repr 1 1) = 1 := by sorry








end D1Bound5
end