Matrix.nondegenerate_toBilin'_iff

theorem Matrix.nondegenerate_toBilin'_iff : ∀ {R₃ : Type u_7} [inst : CommRing R₃] {ι : Type u_12} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {M : Matrix ι ι R₃}, (Matrix.toBilin' M).Nondegenerate ↔ M.Nondegenerate

This theorem states that for any commutative ring `R₃`, any type `ι` which has decidable equality and is finite, and any matrix `M` with indices and entries from these types, the bilinear form obtained from the matrix `M` using the linear equivalence `Matrix.toBilin'` is nondegenerate if and only if the matrix `M` is nondegenerate. Here, a matrix `M` is said to be nondegenerate if for any non-zero vector `v`, there exists a non-zero vector `w` such that the dot product of `v` with the result of multiplying `M` by `w` is non-zero. Similarly, a bilinear form is considered nondegenerate if it is non-zero for all non-zero pair of vectors.

More concisely: For any commutative ring `R₃`, a matrix `M` with finite, decidably equal indices and entries from `R₃` is nondegenerate if and only if the bilinear form obtained from `M` is nondegenerate.