separatingLeft_toLinearMap₂'_iff_det_ne_zero

English

For a matrix M, the left-separating property of the associated linear map is equivalent to det M ≠ 0.

Русский

Свойство слева-разделяющего для линейного отображения, ассоциированного с матрицей M, эквивалентно det M ≠ 0.

LaTeX

$$$ (Matrix.toLinearMap_2' R_1 M).SeparatingLeft (R := R_1) \iff M.det \neq 0 $$$

Lean4

theorem separatingLeft_toLinearMap₂'_iff_det_ne_zero {M : Matrix ι ι R₁} :
    (Matrix.toLinearMap₂' R₁ M).SeparatingLeft (R := R₁) ↔ M.det ≠ 0 := by
  rw [Matrix.separatingLeft_toLinearMap₂'_iff, Matrix.nondegenerate_iff_det_ne_zero]

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