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} [Fintype n] [DecidableEq n] {R : Type v} [CommSemiring R] (i : n) (w : nR) :
LinearMap.proj i ∘ₗ Matrix.toLin' (Matrix.diagonal w) = w i LinearMap.proj i
theorem Matrix.diagonal_comp_single {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type v} [CommSemiring R] (w : nR) (i : n) :
Matrix.toLin' (Matrix.diagonal w) ∘ₗ LinearMap.single R (fun (x : n) => R) i = w i LinearMap.single R (fun (x : n) => R) i
@[deprecated Matrix.diagonal_comp_single]
theorem Matrix.diagonal_comp_stdBasis {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type v} [CommSemiring R] (w : nR) (i : n) :
Matrix.toLin' (Matrix.diagonal w) ∘ₗ 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} [Fintype n] [DecidableEq n] {R : Type v} [CommSemiring R] (w : nR) :
Matrix.toLin' (Matrix.diagonal w) = LinearMap.pi fun (i : n) => w i LinearMap.proj i
theorem Matrix.ker_diagonal_toLin' {m : Type u_1} [Fintype m] {K : Type u} [Semifield K] [DecidableEq m] (w : mK) :
LinearMap.ker (Matrix.toLin' (Matrix.diagonal w)) = i{i : m | w i = 0}, LinearMap.range (LinearMap.single K (fun (x : m) => K) i)
theorem Matrix.range_diagonal {m : Type u_1} [Fintype m] {K : Type u} [Semifield K] [DecidableEq m] (w : mK) :
LinearMap.range (Matrix.toLin' (Matrix.diagonal w)) = i{i : m | w i 0}, LinearMap.range (LinearMap.single K (fun (x : m) => K) i)
theorem LinearMap.rank_diagonal {m : Type u_1} [Fintype m] {K : Type u} [Field K] [DecidableEq m] [DecidableEq K] (w : mK) :
(Matrix.toLin' (Matrix.diagonal w)).rank = (Fintype.card { i : m // w i 0 })