# Documentation

Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

# 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.

Instances For
@[simp]
theorem Matrix.toLinearEquiv'_apply {n : Type u_1} [] {R : Type u_2} [] [] (P : Matrix n n R) (h : ) :
↑() = Matrix.toLin' P
@[simp]
theorem Matrix.toLinearEquiv'_symm_apply {n : Type u_1} [] {R : Type u_2} [] [] (P : Matrix n n R) (h : ) :
↑() = 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 : 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 ()) :

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.

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 ()) :
LinearMap.ker (↑() A) =
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 ()) :
theorem Matrix.exists_mulVec_eq_zero_iff_aux {n : Type u_1} [] {K : Type u_4} [] [] {M : Matrix n n K} :
(v x, = 0) = 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 x, = 0) = 0
theorem Matrix.exists_mulVec_eq_zero_iff {n : Type u_1} [] {A : Type u_4} [] [] [] {M : Matrix n n A} :
(v x, = 0) = 0
theorem Matrix.exists_vecMul_eq_zero_iff {n : Type u_1} [] {A : Type u_4} [] [] [] {M : Matrix n n A} :
(v x, = 0) = 0
theorem Matrix.nondegenerate_iff_det_ne_zero {n : Type u_1} [] {A : Type u_4} [] [] [] {M : Matrix n n A} :
theorem Matrix.Nondegenerate.det_ne_zero {n : Type u_1} [] {A : Type u_4} [] [] [] {M : Matrix n n A} :
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} :
0

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 : ∀ (i j : n), i jA i j < 0) (h2 : ∀ (j : n), 0 < Finset.sum Finset.univ fun i => A i j) :
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 : ∀ (i j : n), i jA i j < 0) (h2 : ∀ (i : n), 0 < Finset.sum Finset.univ fun j => A i j) :
0

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