Theorem: Matrix.det_eq_prod_eigenvalues (CvxLean/Lib/Math/LinearAlgebra/Matrix/Spectrum.lean)

State before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ A.det = ↑(∏ i : n, as i)
Tactic:
apply mul_left_cancel₀ (det_ne_zero_of_left_inverse
  (Basis.toMatrix_mul_toMatrix_flip (Pi.basisFun 𝕜 n) xs.toBasis))
State after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * A.det = (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ↑(∏ i : n, as i)

State before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * A.det = (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ↑(∏ i : n, as i)
Tactic:
rw [← det_mul, spectral_theorem xs as hxs, det_mul, mul_comm, det_diagonal]
State after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ∏ i : n, (RCLike.ofReal ∘ as) i =
    (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ↑(∏ i : n, as i)

State before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ∏ i : n, (RCLike.ofReal ∘ as) i =
    (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ↑(∏ i : n, as i)
Tactic:
simp
State after:
no goals