separatingLeft_of_det_ne_zero — Mathlib

English

If a matrix M has nonzero determinant, then the associated linear map toLinearMap₂' is SeparatingLeft.

Русский

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

LaTeX

$$(M.det ≠ 0) → (Matrix.toLinearMap₂' R M).SeparatingLeft$$

Lean4

theorem separatingLeft_of_det_ne_zero {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) (h : (toMatrix₂ b b B).det ≠ 0) :
    B.SeparatingLeft :=
  (separatingLeft_iff_det_ne_zero b).mpr h

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