Det identity plus two rank one

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.det_identity_plus_two_rank_one {R n : Type*} [CommRing R]
    [Fintype n] [DecidableEq n] (v : n → R) :
    Matrix.det (fun i j => (if i=j then 1 else 0)+1+v i*v j) =
      (1+(Fintype.card n : R))*(1+∑ i, v i^2)-(∑ i, v i)^2 := by sorry









end D1Bound5
end