Even root matrix det ne zero

import Mathlib.Algebra.CharP.Frobenius
import Mathlib.Algebra.CharP.Two
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Analysis.Complex.Norm
import Mathlib.Data.Finset.Card
import Mathlib.Data.Int.GCD
import Mathlib.Data.ZMod.Basic
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.LinearAlgebra.Matrix.SchurComplement
import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination

section
open scoped NumberField BigOperators
open Matrix Module

namespace D1Bound5








theorem _root_.D1Bound5.even_root_matrix_det_ne_zero {K n : Type*} [Field K] [NumberField K]
    [Fintype n] [DecidableEq n] (hK : finrank ℚ K = 2)
    (hn : Even (Fintype.card n)) (v : n → 𝓞 K) (M : Matrix n n (𝓞 K))
    (hd : ∀ i, M i i = v i)
    (hs : ∀ i j, i ≠ j → (M i j)^2 = v i*v j+1) : M.det ≠ 0 := by sorry



end D1Bound5
end