toLinearMap₂ — Mathlib

English

If M is nondegenerate, then for any basis b, the bilinear form given by toLinearMap₂ b b M is separatingLeft.

Русский

Если M не вырождается, то билинейная форма, заданная toLinearMap₂ b b M, является разделяющей слева.

LaTeX

$$(h : M.Nondegenerate) (b) : (toLinearMap₂ b b M).SeparatingLeft$$

Lean4

theorem _root_.Matrix.Nondegenerate.toLinearMap₂ {M : Matrix ι ι R₁} (h : M.Nondegenerate) (b : Basis ι R₁ M₁) :
    (toLinearMap₂ b b M).SeparatingLeft :=
  (Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂ b).mp h.toLinearMap₂'

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