# Documentation

Mathlib.LinearAlgebra.Matrix.Diagonal

# 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) :
LinearMap.comp () (Matrix.toLin' ()) = w i
theorem Matrix.diagonal_comp_stdBasis {n : Type u_1} [] [] {R : Type v} [] (w : nR) (i : n) :
LinearMap.comp (Matrix.toLin' ()) (LinearMap.stdBasis R (fun x => R) i) = w i LinearMap.stdBasis R (fun x => R) i
theorem Matrix.diagonal_toLin' {n : Type u_1} [] [] {R : Type v} [] (w : nR) :
Matrix.toLin' () = LinearMap.pi fun i => w i
theorem Matrix.ker_diagonal_toLin' {m : Type u_1} [] {K : Type u} [] [] (w : mK) :
LinearMap.ker (Matrix.toLin' ()) = ⨆ (i : m) (_ : i {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
theorem Matrix.range_diagonal {m : Type u_1} [] {K : Type u} [] [] (w : mK) :
LinearMap.range (Matrix.toLin' ()) = ⨆ (i : m) (_ : i {i | w i 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
theorem LinearMap.rank_diagonal {m : Type u_1} [] {K : Type u} [] [] [] (w : mK) :
LinearMap.rank (Matrix.toLin' ()) = ↑(Fintype.card { i // w i 0 })