Diagonal matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
[decidable_eq n]
{R : Type v}
[comm_ring R]
(i : n)
(w : n → R) :
(linear_map.proj i).comp (⇑matrix.to_lin' (matrix.diagonal w)) = w i • linear_map.proj i
theorem
matrix.diagonal_comp_std_basis
{n : Type u_1}
[fintype n]
[decidable_eq n]
{R : Type v}
[comm_ring R]
(w : n → R)
(i : n) :
(⇑matrix.to_lin' (matrix.diagonal w)).comp (linear_map.std_basis R (λ (_x : n), R) i) = w i • linear_map.std_basis R (λ (_x : n), R) i
theorem
matrix.diagonal_to_lin'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{R : Type v}
[comm_ring R]
(w : n → R) :
⇑matrix.to_lin' (matrix.diagonal w) = linear_map.pi (λ (i : n), w i • linear_map.proj i)
theorem
matrix.ker_diagonal_to_lin'
{m : Type u_1}
[fintype m]
{K : Type u}
[field K]
[decidable_eq m]
(w : m → K) :
linear_map.ker (⇑matrix.to_lin' (matrix.diagonal w)) = ⨆ (i : m) (H : i ∈ {i : m | w i = 0}), linear_map.range (linear_map.std_basis K (λ (i : m), K) i)
theorem
matrix.range_diagonal
{m : Type u_1}
[fintype m]
{K : Type u}
[field K]
[decidable_eq m]
(w : m → K) :
linear_map.range (⇑matrix.to_lin' (matrix.diagonal w)) = ⨆ (i : m) (H : i ∈ {i : m | w i ≠ 0}), linear_map.range (linear_map.std_basis K (λ (i : m), K) i)
theorem
matrix.rank_diagonal
{m : Type u_1}
[fintype m]
{K : Type u}
[field K]
[decidable_eq m]
[decidable_eq K]
(w : m → K) :
(⇑matrix.to_lin' (matrix.diagonal w)).rank = ↑(fintype.card {i // w i ≠ 0})