separatingLeft_toLinearMap₂_iff

English

Let B be a bilinear form represented by a matrix M in a basis b. The form is left-nondegenerate if and only if the matrix M is nondegenerate.

Русский

Пусть B — билинейная форма на модуле, представленная матрицей M в базисе b. Тогда форма слева-разделяющая тождественно невырождена тогда и только тогда, когда матрица M невырождена.

LaTeX

$$$ (toLinearMap_2 b b M).SeparatingLeft \iff M \text{ is nondegenerate}$$$

Lean4

@[simp]
theorem _root_.Matrix.separatingLeft_toLinearMap₂_iff {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :
    (toLinearMap₂ b b M).SeparatingLeft ↔ M.Nondegenerate := by
  rw [← Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, Matrix.separatingLeft_toLinearMap₂'_iff]
    -- Lemmas transferring nondegeneracy between a bilinear form and its associated matrix

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