Determinant facts: adjoint, singular values, diagonal and bordered matrices

• LinearMap.det_adjoint — det T* = conj (det T), for an endomorphism of a finite-dimensional inner product space. In an orthonormal basis the matrix of the adjoint is the conjugate transpose, and det Aᴴ = conj (det A).
• LinearMap.det_eq_prod_of_apply_eq_smul — the determinant of an endomorphism that is diagonal in some basis (T (b i) = μ i • b i) is the product ∏ μᵢ.
• Matrix.det_eq_corner_mul_det_submatrix — the bordered determinant: if, above the corner, the last column of a (k+1)×(k+1) matrix is a combination of the first k columns, then det M is the corner entry left after that column operation times the determinant of the top-left k×k block. The elementary column-operation form of the Schur determinant formula, over any commutative ring and with no invertibility hypothesis.

theorem LinearMap.det_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) : LinearMap.det (adjoint T) = (starRingEnd 𝕜) (LinearMap.det T)

det T* = conj (det T). In an orthonormal basis the matrix of the adjoint is the conjugate transpose, and det Aᴴ = conj (det A).

Determinant of an endomorphism diagonal in a basis

theorem LinearMap.det_eq_prod_of_apply_eq_smul {R : Type u_3} {M : Type u_4} {ι : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] (b : Module.Basis ι R M) (T : M →ₗ[R] M) (μ : ι → R) (h : ∀ (i : ι), T (b i) = μ i • b i) : LinearMap.det T = ∏ i : ι, μ i

If a basis b consists of eigenvectors of T, with T (b i) = μ i • b i, then det T = ∏ᵢ μᵢ. (The matrix of T in the basis b is diagonal μ.)

Bordered determinants

If the last column of a (k+1)×(k+1) matrix M is, above the corner, the combination of the first k columns with coefficients w, then subtracting that combination clears the column and Laplace expansion gives det M as the resulting corner entry times the determinant of the top-left k×k block.

theorem Matrix.det_eq_corner_mul_det_submatrix {R : Type u_3} [CommRing R] {k : ℕ} (M : Matrix (Fin (k + 1)) (Fin (k + 1)) R) (w : Fin k → R) (hw : ∀ (i : Fin k), M i.castSucc (Fin.last k) = ∑ j : Fin k, M i.castSucc j.castSucc * w j) : M.det = (M (Fin.last k) (Fin.last k) - ∑ j : Fin k, M (Fin.last k) j.castSucc * w j) * (M.submatrix Fin.castSucc Fin.castSucc).det

Bordered determinant. Let M be a (k+1)×(k+1) matrix and w a vector of k scalars such that the entries of the last column of M above the corner are given by the combination of the first k columns with coefficients w, i.e. M i last = ∑ⱼ M i j · wⱼ for i < k. Then

det M = (M last last - ∑ⱼ M last j · wⱼ) · det (M restricted to the first k rows and columns).

No invertibility of the top-left block is required; this is the elementary column-operation form of the Schur determinant formula.