toBilin — Mathlib

English

There is a canonical equivalence between nondegenerate matrices and the corresponding bilinear forms, via toBilin' and toMatrix'.

Русский

Существует каноническое эквивалентность между неразложимыми матрицами и соответствующими билинейными формами через toBilin' и toMatrix'.

LaTeX

$$$$M.Nondegenerate \iff (M.toBilin'.Nondegenerate).$$$$

Lean4

theorem _root_.Matrix.Nondegenerate.toBilin {M : Matrix ι ι R₂} (h : M.Nondegenerate) (b : Basis ι R₂ M₂) :
    (Matrix.toBilin b M).Nondegenerate :=
  (Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin b).mp h.toBilin'

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