nondegenerate_toBilin'_iff_det_ne_zero

English

If M det ≠ 0 then M.toBilin'.Nondegenerate, i.e., the bilinear form is nondegenerate.

Русский

Если det M ≠ 0, то M.toBilin' неразложима; билийн форма неразложима.

LaTeX

$$$$\det M \neq 0 \Rightarrow M.toBilin'.Nondegenerate.$$$$

Lean4

theorem nondegenerate_toBilin'_iff_det_ne_zero {M : Matrix ι ι A} : M.toBilin'.Nondegenerate ↔ M.det ≠ 0 := by
  rw [Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero]

Похожие утверждения