# Diagonal matrices #

This file contains some results on the linear map corresponding to a diagonal matrix (range, ker and rank).

## Tags #

matrix, diagonal, linear_map

theorem Matrix.proj_diagonal {n : Type u_1} [] [] {R : Type v} [] (i : n) (w : nR) :
∘ₗ Matrix.toLin' () = w i
theorem Matrix.diagonal_comp_stdBasis {n : Type u_1} [] [] {R : Type v} [] (w : nR) (i : n) :
Matrix.toLin' () ∘ₗ LinearMap.stdBasis R (fun (x : n) => R) i = w i LinearMap.stdBasis R (fun (x : n) => R) i
theorem Matrix.diagonal_toLin' {n : Type u_1} [] [] {R : Type v} [] (w : nR) :
Matrix.toLin' () = LinearMap.pi fun (i : n) => w i
theorem Matrix.ker_diagonal_toLin' {m : Type u_1} [] {K : Type u} [] [] (w : mK) :
LinearMap.ker (Matrix.toLin' ()) = i{i : m | w i = 0}, LinearMap.range (LinearMap.stdBasis K (fun (x : m) => K) i)
theorem Matrix.range_diagonal {m : Type u_1} [] {K : Type u} [] [] (w : mK) :
LinearMap.range (Matrix.toLin' ()) = i{i : m | w i 0}, LinearMap.range (LinearMap.stdBasis K (fun (x : m) => K) i)
theorem LinearMap.rank_diagonal {m : Type u_1} [] {K : Type u} [] [] [] (w : mK) :
(Matrix.toLin' ()).rank = (Fintype.card { i : m // w i 0 })