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.
@[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 • matrix.std_basis_matrix i j a = matrix.std_basis_matrix i j (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) :
matrix.std_basis_matrix i j 0 = 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 : α) :
matrix.std_basis_matrix i j (a + b) = matrix.std_basis_matrix i j a + matrix.std_basis_matrix i j 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 : α) :
matrix.std_basis_matrix i j 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')) :
matrix.std_basis_matrix i j c 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 : α) :
matrix.std_basis_matrix i j 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 : α) :
matrix.std_basis_matrix i 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) :
(matrix.std_basis_matrix i j 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 : α) :
(matrix.std_basis_matrix i i c).diag = pi.single i 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) :
(matrix.std_basis_matrix i j 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] :
(matrix.std_basis_matrix i i 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 : 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 : α) :
(matrix.std_basis_matrix i j c).mul (matrix.std_basis_matrix j k d) = matrix.std_basis_matrix i k (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 : α) :
(matrix.std_basis_matrix i j c).mul (matrix.std_basis_matrix k l d) = 0