nondegenerate_toBilin'_iff_nondegenerate_toBilin

English

For M, the nondegeneracy of the bilinear form toBilin' is equivalent to det M ≠ 0.

Русский

Для M неособенная билинейная форма toBilin' эквивалентна det M ≠ 0.

LaTeX

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

Lean4

theorem _root_.Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :
    M.toBilin'.Nondegenerate ↔ (Matrix.toBilin b M).Nondegenerate :=
  (nondegenerate_congr_iff b.equivFun.symm).symm

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