# mathlibdocumentation

data.matrix.basis

# Matrices with a single non-zero element. #

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

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

Equations
• = λ (i' : m) (j' : n), ite (i = i' j = j') a 0
@[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 : α) :
b = (b a)
@[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) :
= 0
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 : α) :
(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 : n α) :
x = finset.univ.sum (λ (i : m), finset.univ.sum (λ (j : n), (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.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 : n α → Prop} (M : n α) (h_zero : P 0) (h_add : ∀ (p q : n α), P pP qP (p + q)) (h_std_basis : ∀ (i : m) (j : n) (x : α), P 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 : n α → Prop} (M : n α) (h_add : ∀ (p q : n α), P pP qP (p + q)) (h_std_basis : ∀ (i : m) (j : n) (x : α), P 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 : α) :
i j = 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')) :
i' j' = 0
@[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 : α) :
i' j' = 0
@[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 : α) :
i' j' = 0
@[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) :
c).diag = 0
@[simp]
theorem matrix.std_basis_matrix.diag_same {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i : n) (c : α) :
c).diag = 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) :
c).trace = 0
@[simp]
theorem matrix.std_basis_matrix.trace_eq {n : Type u_3} {α : Type u_5} [decidable_eq n] [semiring α] (i : n) (c : α) [fintype n] :
c).trace = c
@[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 : n α) :
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 : n α) :
M.mul 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 : n α) :
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 : n α) :
M.mul 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 : α) :
c).mul d) = (c * 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 : α) :
c).mul d) = 0