separatingLeft_toLinearMap₂'_iff

English

For any matrix M, the left-separating property of the linear map Matrix.toLinearMap₂' R₁ M is equivalent to M being nondegenerate.

Русский

Для любой матрицы M свойство разделения слева для линейного отображения Matrix.toLinearMap₂' R₁ M эквивалентно тому, что M не вырождается.

LaTeX

$$$(Matrix.toLinearMap₂' R_1 M).SeparatingLeft \iff M.Nondegenerate$$$

Lean4

@[simp]
theorem _root_.Matrix.separatingLeft_toLinearMap₂'_iff {M : Matrix ι ι R₁} :
    (Matrix.toLinearMap₂' R₁ M).SeparatingLeft (R := R₁) ↔ M.Nondegenerate :=
  by
  refine ⟨fun h ↦ Matrix.nondegenerate_def.mpr ?_, Matrix.Nondegenerate.toLinearMap₂'⟩
  exact fun v hv => h v fun w => (M.toLinearMap₂'_apply' _ _).trans <| hv w

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