Matrices with a single non-zero element. #
This file provides matrix.stdBasisMatrix. The matrix matrix.stdBasisMatrix i j c has c
at position (i, j), and zeroes elsewhere.
def
Matrix.stdBasisMatrix
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
(a : α)
:
Matrix m n α
stdBasisMatrix i j a is the matrix with a in the i-th row, j-th column,
and zeroes elsewhere.
Equations
- Matrix.stdBasisMatrix i j a i' j' = if i = i' ∧ j = j' then a else 0
Instances For
@[simp]
theorem
Matrix.smul_stdBasisMatrix
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
(a : α)
(b : α)
:
b • Matrix.stdBasisMatrix i j a = Matrix.stdBasisMatrix i j (b • a)
@[simp]
theorem
Matrix.stdBasisMatrix_zero
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
:
Matrix.stdBasisMatrix i j 0 = 0
theorem
Matrix.stdBasisMatrix_add
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
(a : α)
(b : α)
:
Matrix.stdBasisMatrix i j (a + b) = Matrix.stdBasisMatrix i j a + Matrix.stdBasisMatrix i j b
theorem
Matrix.matrix_eq_sum_std_basis
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
[Fintype m]
[Fintype n]
(x : Matrix m n α)
:
x = Finset.sum Finset.univ fun i => Finset.sum Finset.univ fun j => Matrix.stdBasisMatrix i j (x i j)
theorem
Matrix.std_basis_eq_basis_mul_basis
{m : Type u_2}
{n : Type u_3}
[DecidableEq m]
[DecidableEq n]
(i : m)
(j : n)
:
Matrix.stdBasisMatrix i j 1 = Matrix.vecMulVec (fun i' => if i = i' then 1 else 0) fun j' => if j = j' then 1 else 0
theorem
Matrix.induction_on'
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq 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.stdBasisMatrix i j x))
:
P M
theorem
Matrix.induction_on
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq 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.stdBasisMatrix i j x))
:
P M
@[simp]
theorem
Matrix.StdBasisMatrix.apply_same
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
(c : α)
:
Matrix.stdBasisMatrix i j c i j = c
@[simp]
theorem
Matrix.StdBasisMatrix.apply_of_ne
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
(c : α)
(i' : m)
(j' : n)
(h : ¬(i = i' ∧ j = j'))
:
Matrix.stdBasisMatrix i j c i' j' = 0
@[simp]
theorem
Matrix.StdBasisMatrix.apply_of_row_ne
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
{i : m}
{i' : m}
(hi : i ≠ i')
(j : n)
(j' : n)
(a : α)
:
Matrix.stdBasisMatrix i j a i' j' = 0
@[simp]
theorem
Matrix.StdBasisMatrix.apply_of_col_ne
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(i' : m)
{j : n}
{j' : n}
(hj : j ≠ j')
(a : α)
:
Matrix.stdBasisMatrix i j a i' j' = 0
@[simp]
theorem
Matrix.StdBasisMatrix.diag_zero
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
(h : j ≠ i)
:
Matrix.diag (Matrix.stdBasisMatrix i j c) = 0
@[simp]
theorem
Matrix.StdBasisMatrix.diag_same
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(c : α)
:
Matrix.diag (Matrix.stdBasisMatrix i i c) = Pi.single i c
@[simp]
theorem
Matrix.StdBasisMatrix.trace_zero
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(h : j ≠ i)
:
Matrix.trace (Matrix.stdBasisMatrix i j c) = 0
@[simp]
theorem
Matrix.StdBasisMatrix.trace_eq
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(c : α)
[Fintype n]
:
Matrix.trace (Matrix.stdBasisMatrix i i c) = c
@[simp]
theorem
Matrix.StdBasisMatrix.mul_left_apply_same
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(b : n)
(M : Matrix n n α)
:
(Matrix n n α * Matrix n n α) (Matrix n n α) Matrix.instHMulMatrixMatrixMatrix (Matrix.stdBasisMatrix i j c) M i b = c * M j b
@[simp]
theorem
Matrix.StdBasisMatrix.mul_right_apply_same
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(a : n)
(M : Matrix n n α)
:
(Matrix n n α * Matrix n n α) (Matrix n n α) Matrix.instHMulMatrixMatrixMatrix M (Matrix.stdBasisMatrix i j c) a j = M a i * c
@[simp]
theorem
Matrix.StdBasisMatrix.mul_left_apply_of_ne
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(a : n)
(b : n)
(h : a ≠ i)
(M : Matrix n n α)
:
(Matrix n n α * Matrix n n α) (Matrix n n α) Matrix.instHMulMatrixMatrixMatrix (Matrix.stdBasisMatrix i j c) M a b = 0
@[simp]
theorem
Matrix.StdBasisMatrix.mul_right_apply_of_ne
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(a : n)
(b : n)
(hbj : b ≠ j)
(M : Matrix n n α)
:
(Matrix n n α * Matrix n n α) (Matrix n n α) Matrix.instHMulMatrixMatrixMatrix M (Matrix.stdBasisMatrix i j c) a b = 0
@[simp]
theorem
Matrix.StdBasisMatrix.mul_same
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(k : n)
(d : α)
:
Matrix.stdBasisMatrix i j c * Matrix.stdBasisMatrix j k d = Matrix.stdBasisMatrix i k (c * d)
@[simp]
theorem
Matrix.StdBasisMatrix.mul_of_ne
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
{k : n}
{l : n}
(h : j ≠ k)
(d : α)
:
Matrix.stdBasisMatrix i j c * Matrix.stdBasisMatrix k l d = 0