separatingLeft_toLinearMap₂'_of_det_ne_zero'

English

Let B be a bilinear form on M with basis b. Then B is SeparatingLeft if and only if the Gram matrix (toMatrix₂ b b B) has nonzero determinant.

Русский

Пусть B — билинейная форма на M с базисом b. Тогда B является SeparatingLeft тогда и только тогда, когда граммова матрица (toMatrix₂ b b B) имеет ненулевой детерминант.

LaTeX

$$B.SeparatingLeft \iff (toMatrix₂ b b B).det \neq 0$$

Lean4

theorem separatingLeft_toLinearMap₂'_of_det_ne_zero' (M : Matrix ι ι R₁) (h : M.det ≠ 0) :
    (Matrix.toLinearMap₂' R₁ M).SeparatingLeft (R := R₁) :=
  separatingLeft_toLinearMap₂'_iff_det_ne_zero.mpr h

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