toLinearMap₂' — Mathlib

English

If M is a nondegenerate matrix, then the associated bilinear form given by Matrix.toLinearMap₂' is separatingLeft.

Русский

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

LaTeX

$$$M.Nondegenerate \Rightarrow (Matrix.toLinearMap₂'\ R\ M).SeparatingLeft$$$

Lean4

theorem _root_.Matrix.Nondegenerate.toLinearMap₂' {M : Matrix ι ι R₁} (h : M.Nondegenerate) :
    (Matrix.toLinearMap₂' R₁ M).SeparatingLeft (R := R₁) := fun x hx =>
  h.eq_zero_of_ortho fun y => by simpa only [toLinearMap₂'_apply'] using hx y

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