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] [Zero α] (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 = Matrix.of fun (i' : m) (j' : n) => if i = i' ∧ j = j' then a else 0

theorem Matrix.stdBasisMatrix_eq_of_single_single {m : Type u_2} {n : Type u_3} {α : Type u_5} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) : Matrix.stdBasisMatrix i j a = Matrix.of (Pi.single i (Pi.single j a))

@[simp]

theorem Matrix.smul_stdBasisMatrix {m : Type u_2} {n : Type u_3} {R : Type u_4} {α : Type u_5} [DecidableEq m] [DecidableEq n] [Zero α] [SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α) : r • Matrix.stdBasisMatrix i j a = Matrix.stdBasisMatrix i j (r • a)

@[simp]

theorem Matrix.stdBasisMatrix_zero {m : Type u_2} {n : Type u_3} {α : Type u_5} [DecidableEq m] [DecidableEq n] [Zero α] (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] [AddZeroClass α] (i : m) (j : n) (a b : α) : Matrix.stdBasisMatrix i j (a + b) = Matrix.stdBasisMatrix i j a + Matrix.stdBasisMatrix i j b

theorem Matrix.mulVec_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [DecidableEq m] [DecidableEq n] [NonUnitalNonAssocSemiring α] [Fintype m] (i : n) (j : m) (c : α) (x : m → α) : (Matrix.stdBasisMatrix i j c).mulVec x = Function.update 0 i (c * x j)

theorem Matrix.matrix_eq_sum_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] [Fintype m] [Fintype n] (x : Matrix m n α) : x = ∑ i : m, ∑ j : n, Matrix.stdBasisMatrix i j (x i j)

@[deprecated Matrix.matrix_eq_sum_stdBasisMatrix]

theorem Matrix.matrix_eq_sum_std_basis {m : Type u_2} {n : Type u_3} {α : Type u_5} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] [Fintype m] [Fintype n] (x : Matrix m n α) : x = ∑ i : m, ∑ j : n, Matrix.stdBasisMatrix i j (x i j)

Alias of Matrix.matrix_eq_sum_stdBasisMatrix.

theorem Matrix.stdBasisMatrix_eq_single_vecMulVec_single {m : Type u_2} {n : Type u_3} {α : Type u_5} [DecidableEq m] [DecidableEq n] [MulZeroOneClass α] (i : m) (j : n) : Matrix.stdBasisMatrix i j 1 = Matrix.vecMulVec (Pi.single i 1) (Pi.single j 1)

@[deprecated Matrix.stdBasisMatrix_eq_single_vecMulVec_single]

theorem Matrix.std_basis_eq_basis_mul_basis {m : Type u_2} {n : Type u_3} {α : Type u_5} [DecidableEq m] [DecidableEq n] [MulZeroOneClass α] (i : m) (j : n) : Matrix.stdBasisMatrix i j 1 = Matrix.vecMulVec (fun (i' : m) => if i = i' then 1 else 0) fun (j' : n) => 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] [AddCommMonoid α] [Finite m] [Finite 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] [AddCommMonoid α] [Finite m] [Finite 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] [Zero α] (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] [Zero α] (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] [Zero α] {i i' : m} (hi : i ≠ i') (j 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] [Zero α] (i i' : m) {j 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] [Zero α] (i j : n) (c : α) (h : j ≠ i) : (Matrix.stdBasisMatrix i j c).diag = 0

@[simp]

theorem Matrix.StdBasisMatrix.diag_same {n : Type u_3} {α : Type u_5} [DecidableEq n] [Zero α] (i : n) (c : α) : (Matrix.stdBasisMatrix i i c).diag = Pi.single i c

@[simp]

theorem Matrix.StdBasisMatrix.mul_left_apply_same {n : Type u_3} {α : Type u_5} [DecidableEq n] [Fintype n] [NonUnitalNonAssocSemiring α] (i j : n) (c : α) (b : n) (M : Matrix n n α) : (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] [Fintype n] [NonUnitalNonAssocSemiring α] (i j : n) (c : α) (a : n) (M : Matrix n n α) : (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] [Fintype n] [NonUnitalNonAssocSemiring α] (i j : n) (c : α) (a b : n) (h : a ≠ i) (M : Matrix n n α) : (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] [Fintype n] [NonUnitalNonAssocSemiring α] (i j : n) (c : α) (a b : n) (hbj : b ≠ j) (M : Matrix n n α) : (M * Matrix.stdBasisMatrix i j c) a b = 0

@[simp]

theorem Matrix.StdBasisMatrix.mul_same {n : Type u_3} {α : Type u_5} [DecidableEq n] [Fintype n] [NonUnitalNonAssocSemiring α] (i j : n) (c : α) (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] [Fintype n] [NonUnitalNonAssocSemiring α] (i j : n) (c : α) {k l : n} (h : j ≠ k) (d : α) : Matrix.stdBasisMatrix i j c * Matrix.stdBasisMatrix k l d = 0

theorem Matrix.row_eq_zero_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_5} [DecidableEq n] [Fintype n] [Semiring α] {i j k : n} {M : Matrix n n α} (hM : Commute (Matrix.stdBasisMatrix i j 1) M) (hkj : k ≠ j) : M j k = 0

theorem Matrix.col_eq_zero_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_5} [DecidableEq n] [Fintype n] [Semiring α] {i j k : n} {M : Matrix n n α} (hM : Commute (Matrix.stdBasisMatrix i j 1) M) (hki : k ≠ i) : M k i = 0

theorem Matrix.diag_eq_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_5} [DecidableEq n] [Fintype n] [Semiring α] {i j : n} {M : Matrix n n α} (hM : Commute (Matrix.stdBasisMatrix i j 1) M) : M i i = M j j

theorem Matrix.mem_range_scalar_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_5} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} (hM : Pairwise fun (i j : n) => Commute (Matrix.stdBasisMatrix i j 1) M) : M ∈ Set.range ⇑(Matrix.scalar n)

M is a scalar matrix if it commutes with every non-diagonal stdBasisMatrix.

theorem Matrix.mem_range_scalar_iff_commute_stdBasisMatrix {n : Type u_3} {α : Type u_5} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} : M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (Matrix.stdBasisMatrix i j 1) M

theorem Matrix.mem_range_scalar_iff_commute_stdBasisMatrix' {n : Type u_3} {α : Type u_5} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} : M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (i j : n), Commute (Matrix.stdBasisMatrix i j 1) M

M is a scalar matrix if and only if it commutes with every stdBasisMatrix.