mathlib3 documentation

data.matrix.basis

Matrices with a single non-zero element. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides matrix.std_basis_matrix. The matrix matrix.std_basis_matrix i j c has c at position (i, j), and zeroes elsewhere.

def matrix.std_basis_matrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] (i : m) (j : n) (a : α) :
matrix m n α

std_basis_matrix i j a is the matrix with a in the i-th row, j-th column, and zeroes elsewhere.

Equations
@[simp]
theorem matrix.smul_std_basis_matrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] (i : m) (j : n) (a b : α) :
@[simp]
theorem matrix.std_basis_matrix_zero {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] (i : m) (j : n) :
theorem matrix.std_basis_matrix_add {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] (i : m) (j : n) (a b : α) :
theorem matrix.matrix_eq_sum_std_basis {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] [fintype m] [fintype n] (x : matrix m n α) :
x = finset.univ.sum (λ (i : m), finset.univ.sum (λ (j : n), matrix.std_basis_matrix i j (x i j)))
theorem matrix.std_basis_eq_basis_mul_basis {m : Type u_2} {n : Type u_3} [decidable_eq m] [decidable_eq n] (i : m) (j : n) :
matrix.std_basis_matrix i j 1 = matrix.vec_mul_vec (λ (i' : m), ite (i = i') 1 0) (λ (j' : n), ite (j = j') 1 0)
@[protected]
theorem matrix.induction_on' {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] [fintype m] [fintype n] {P : matrix m n α Prop} (M : matrix m n α) (h_zero : P 0) (h_add : (p q : matrix m n α), P p P q P (p + q)) (h_std_basis : (i : m) (j : n) (x : α), P (matrix.std_basis_matrix i j x)) :
P M
@[protected]
theorem matrix.induction_on {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] [fintype m] [fintype n] [nonempty m] [nonempty n] {P : matrix m n α Prop} (M : matrix m n α) (h_add : (p q : matrix m n α), P p P q P (p + q)) (h_std_basis : (i : m) (j : n) (x : α), P (matrix.std_basis_matrix i j x)) :
P M
@[simp]
theorem matrix.std_basis_matrix.apply_same {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] (i : m) (j : n) (c : α) :
@[simp]
theorem matrix.std_basis_matrix.apply_of_ne {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] (i : m) (j : n) (c : α) (i' : m) (j' : n) (h : ¬(i = i' j = j')) :
@[simp]
theorem matrix.std_basis_matrix.apply_of_row_ne {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] {i i' : m} (hi : i i') (j j' : n) (a : α) :
@[simp]
theorem matrix.std_basis_matrix.apply_of_col_ne {m : Type u_2} {n : Type u_3} {α : Type u_5} [decidable_eq m] [decidable_eq n] [semiring α] (i i' : m) {j j' : n} (hj : j j') (a : α) :
@[simp]
theorem matrix.std_basis_matrix.diag_zero {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i j : n) (c : α) (h : j i) :
@[simp]
theorem matrix.std_basis_matrix.diag_same {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i : n) (c : α) :
@[simp]
theorem matrix.std_basis_matrix.trace_zero {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i j : n) (c : α) [fintype n] (h : j i) :
@[simp]
theorem matrix.std_basis_matrix.trace_eq {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i : n) (c : α) [fintype n] :
@[simp]
theorem matrix.std_basis_matrix.mul_left_apply_same {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i j : n) (c : α) [fintype n] (b : n) (M : matrix n n α) :
(matrix.std_basis_matrix i j c).mul M i b = c * M j b
@[simp]
theorem matrix.std_basis_matrix.mul_right_apply_same {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i j : n) (c : α) [fintype n] (a : n) (M : matrix n n α) :
M.mul (matrix.std_basis_matrix i j c) a j = M a i * c
@[simp]
theorem matrix.std_basis_matrix.mul_left_apply_of_ne {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i j : n) (c : α) [fintype n] (a b : n) (h : a i) (M : matrix n n α) :
(matrix.std_basis_matrix i j c).mul M a b = 0
@[simp]
theorem matrix.std_basis_matrix.mul_right_apply_of_ne {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i j : n) (c : α) [fintype n] (a b : n) (hbj : b j) (M : matrix n n α) :
M.mul (matrix.std_basis_matrix i j c) a b = 0
@[simp]
theorem matrix.std_basis_matrix.mul_same {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i j : n) (c : α) [fintype n] (k : n) (d : α) :
@[simp]
theorem matrix.std_basis_matrix.mul_of_ne {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i j : n) (c : α) [fintype n] {k l : n} (h : j k) (d : α) :