Scaled Root Matrix det

import Mathlib.Data.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_DeterminantNormalization_Definitions

section
open scoped BigOperators
open Matrix

namespace D1Bound5






theorem _root_.D1Bound5.scaledRootMatrix_det {R n : Type*} [CommRing R]
    [Fintype n] [DecidableEq n] (u : n → R) (M : Matrix n n R) :
    (scaledRootMatrix u M).det = (∏ i, u i)^2 * M.det := by sorry













end D1Bound5
end