mathlib documentation

linear_algebra.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] [decidable_eq n] {R : Type v} [comm_ring R] (i : n) (w : n → R) :
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) ∘ₗ 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) :
theorem matrix.ker_diagonal_to_lin' {m : Type u_1} [fintype m] {K : Type u} [field K] [decidable_eq m] (w : m → K) :
(matrix.to_lin' (matrix.diagonal w)).ker = ⨆ (i : m) (H : i {i : m | w i = 0}), (linear_map.std_basis K (λ (i : m), K) i).range
theorem matrix.range_diagonal {m : Type u_1} [fintype m] {K : Type u} [field K] [decidable_eq m] (w : m → K) :
(matrix.to_lin' (matrix.diagonal w)).range = ⨆ (i : m) (H : i {i : m | w i 0}), (linear_map.std_basis K (λ (i : m), K) i).range
theorem matrix.rank_diagonal {m : Type u_1} [fintype m] {K : Type u} [field K] [decidable_eq m] [decidable_eq K] (w : m → K) :