mathlib documentation

linear_algebra.matrix.to_linear_equiv

Matrices and linear equivalences #

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

Main definitions #

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 : matrix n n R) (h : is_unit 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 : matrix n n R) (h : is_unit 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 : matrix n n R) (h : is_unit P) :
@[simp]
theorem matrix.to_linear_equiv_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {n : Type u_3} [fintype n] (b : basis n R M) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) (ᾰ : M) :
def matrix.to_linear_equiv {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {n : Type u_3} [fintype n] (b : basis n R M) [decidable_eq n] (A : matrix n 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] [add_comm_group M] [module R M] {n : Type u_3} [fintype n] (b : basis n R M) [decidable_eq n] (A : matrix n 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] [add_comm_group M] [module R M] {n : Type u_3} [fintype n] (b : basis n R M) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) :