mathlib3 documentation

linear_algebra.matrix.diagonal

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) :
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) :
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) :