# mathlib3documentation

linear_algebra.matrix.to_linear_equiv

# Matrices and linear equivalences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file gives the map matrix.to_linear_equiv from matrices with invertible determinant, to linear equivs.

## Main definitions #

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

## Main results #

• matrix.exists_mul_vec_eq_zero_iff: M maps some v ≠ 0 to zero iff det M = 0

## Tags #

matrix, linear_equiv, determinant, inverse

def matrix.to_linear_equiv' {R : Type u_1} [comm_ring R] {n : Type u_3} [fintype n] [decidable_eq n] (P : n R) (h : invertible P) :
(n R) ≃ₗ[R] n R

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

See matrix.to_linear_equiv for the same map on arbitrary modules.

Equations
@[simp]
theorem matrix.to_linear_equiv'_apply {R : Type u_1} [comm_ring R] {n : Type u_3} [fintype n] [decidable_eq n] (P : n R) (h : invertible P) :
@[simp]
theorem matrix.to_linear_equiv'_symm_apply {R : Type u_1} [comm_ring R] {n : Type u_3} [fintype n] [decidable_eq n] (P : n R) (h : invertible P) :
@[simp]
theorem matrix.to_linear_equiv_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {n : Type u_3} [fintype n] (b : R M) [decidable_eq n] (A : n R) (hA : is_unit A.det) (ᾰ : M) :
hA) = ( b) A)
noncomputable def matrix.to_linear_equiv {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {n : Type u_3} [fintype n] (b : R M) [decidable_eq n] (A : n R) (hA : is_unit A.det) :

Given hA : is_unit A.det and b : basis R b, A.to_linear_equiv b hA is the linear_equiv arising from to_lin b b A.

See matrix.to_linear_equiv' for this result on n → R.

Equations
theorem matrix.ker_to_lin_eq_bot {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {n : Type u_3} [fintype n] (b : R M) [decidable_eq n] (A : n R) (hA : is_unit A.det) :
theorem matrix.range_to_lin_eq_top {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {n : Type u_3} [fintype n] (b : R M) [decidable_eq n] (A : n R) (hA : is_unit A.det) :
theorem matrix.exists_mul_vec_eq_zero_iff_aux {n : Type u_3} [fintype n] {K : Type u_1} [decidable_eq n] [field K] {M : n K} :
( (v : n K) (H : v 0), M.mul_vec v = 0) M.det = 0

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

theorem matrix.exists_mul_vec_eq_zero_iff' {n : Type u_3} [fintype n] {A : Type u_1} (K : Type u_2) [decidable_eq n] [comm_ring A] [nontrivial A] [field K] [ K] [ K] {M : n A} :
( (v : n A) (H : v 0), M.mul_vec v = 0) M.det = 0
theorem matrix.exists_mul_vec_eq_zero_iff {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : n A} :
( (v : n A) (H : v 0), M.mul_vec v = 0) M.det = 0
theorem matrix.exists_vec_mul_eq_zero_iff {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : n A} :
( (v : n A) (H : v 0), = 0) M.det = 0
theorem matrix.nondegenerate_iff_det_ne_zero {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : n A} :
theorem matrix.nondegenerate.det_ne_zero {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : n A} :

Alias of the forward direction of matrix.nondegenerate_iff_det_ne_zero.

theorem matrix.nondegenerate.of_det_ne_zero {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : n A} :

Alias of the reverse direction of matrix.nondegenerate_iff_det_ne_zero.