nondegenerate_of_det_ne_zero — Mathlib

English

If B.Nondegenerate, then there exists a basis b such that BilinForm.toMatrix b B is nondegenerate.

Русский

Если B неразложима, найдется база b такая, что BilinForm.toMatrix b B неразложима.

LaTeX

$$$$B.Nondegenerate \Rightarrow \exists b:\; (BilinForm.toMatrix b B).Nondegenerate.$$$$

Lean4

theorem nondegenerate_of_det_ne_zero (b : Basis ι A M₂) (h : (BilinForm.toMatrix b B₃).det ≠ 0) : B₃.Nondegenerate :=
  (nondegenerate_iff_det_ne_zero b).mpr h

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