# Matrices and linear equivalences #

This file gives the map Matrix.toLinearEquiv from matrices with invertible determinant, to linear equivs.

## Main definitions #

• Matrix.toLinearEquiv: a matrix with an invertible determinant forms a linear equiv

## Main results #

• Matrix.exists_mulVec_eq_zero_iff: M maps some v ≠ 0 to zero iff det M = 0

## Tags #

matrix, linear_equiv, determinant, inverse

def Matrix.toLinearEquiv' {n : Type u_1} [] {R : Type u_2} [] [] (P : Matrix n n R) :
(nR) ≃ₗ[R] nR

An invertible matrix yields a linear equivalence from the free module to itself.

See Matrix.toLinearEquiv for the same map on arbitrary modules.

Equations
• P.toLinearEquiv' x = () (Matrix.GeneralLinearGroup.toLinear ())
Instances For
@[simp]
theorem Matrix.toLinearEquiv'_apply {n : Type u_1} [] {R : Type u_2} [] [] (P : Matrix n n R) (h : ) :
(P.toLinearEquiv' h) = Matrix.toLin' P
@[simp]
theorem Matrix.toLinearEquiv'_symm_apply {n : Type u_1} [] {R : Type u_2} [] [] (P : Matrix n n R) (h : ) :
(P.toLinearEquiv' h).symm = Matrix.toLin' P
@[simp]
theorem Matrix.toLinearEquiv_apply {n : Type u_1} [] {R : Type u_2} {M : Type u_3} [] [] [Module R M] (b : Basis n R M) [] (A : Matrix n n R) (hA : IsUnit A.det) (a : M) :
() a = (() A) a
noncomputable def Matrix.toLinearEquiv {n : Type u_1} [] {R : Type u_2} {M : Type u_3} [] [] [Module R M] (b : Basis n R M) [] (A : Matrix n n R) (hA : IsUnit A.det) :

Given hA : IsUnit A.det and b : Basis R b, A.toLinearEquiv b hA is the LinearEquiv arising from toLin b b A.

See Matrix.toLinearEquiv' for this result on n → R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Matrix.ker_toLin_eq_bot {n : Type u_1} [] {R : Type u_2} {M : Type u_3} [] [] [Module R M] (b : Basis n R M) [] (A : Matrix n n R) (hA : IsUnit A.det) :
theorem Matrix.range_toLin_eq_top {n : Type u_1} [] {R : Type u_2} {M : Type u_3} [] [] [Module R M] (b : Basis n R M) [] (A : Matrix n n R) (hA : IsUnit A.det) :
theorem Matrix.exists_mulVec_eq_zero_iff_aux {n : Type u_1} [] {K : Type u_4} [] [] {M : Matrix n n K} :
(∃ (v : nK), v 0 M.mulVec v = 0) M.det = 0

This holds for all integral domains (see Matrix.exists_mulVec_eq_zero_iff), not just fields, but it's easier to prove it for the field of fractions first.

theorem Matrix.exists_mulVec_eq_zero_iff' {n : Type u_1} [] {A : Type u_4} (K : Type u_5) [] [] [] [] [Algebra A K] [] {M : Matrix n n A} :
(∃ (v : nA), v 0 M.mulVec v = 0) M.det = 0
theorem Matrix.exists_mulVec_eq_zero_iff {n : Type u_1} [] {A : Type u_4} [] [] [] {M : Matrix n n A} :
(∃ (v : nA), v 0 M.mulVec v = 0) M.det = 0
theorem Matrix.exists_vecMul_eq_zero_iff {n : Type u_1} [] {A : Type u_4} [] [] [] {M : Matrix n n A} :
(∃ (v : nA), v 0 = 0) M.det = 0
theorem Matrix.nondegenerate_iff_det_ne_zero {n : Type u_1} [] {A : Type u_4} [] [] [] {M : Matrix n n A} :
M.Nondegenerate M.det 0
theorem Matrix.Nondegenerate.det_ne_zero {n : Type u_1} [] {A : Type u_4} [] [] [] {M : Matrix n n A} :
M.NondegenerateM.det 0

Alias of the forward direction of Matrix.nondegenerate_iff_det_ne_zero.

theorem Matrix.Nondegenerate.of_det_ne_zero {n : Type u_1} [] {A : Type u_4} [] [] [] {M : Matrix n n A} :
M.det 0M.Nondegenerate

Alias of the reverse direction of Matrix.nondegenerate_iff_det_ne_zero.

theorem Matrix.det_ne_zero_of_sum_col_pos {n : Type u_1} [] [] {S : Type u_2} {A : Matrix n n S} (h1 : Pairwise fun (i j : n) => A i j < 0) (h2 : ∀ (j : n), 0 < i : n, A i j) :
A.det 0

A matrix whose nondiagonal entries are negative with the sum of the entries of each column positive has nonzero determinant.

theorem Matrix.det_ne_zero_of_sum_row_pos {n : Type u_1} [] [] {S : Type u_2} {A : Matrix n n S} (h1 : Pairwise fun (i j : n) => A i j < 0) (h2 : ∀ (i : n), 0 < j : n, A i j) :
A.det 0

A matrix whose nondiagonal entries are negative with the sum of the entries of each row positive has nonzero determinant.