Documentation

Mathlib.Data.Matrix.Basis

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
Instances For
    @[simp]
    theorem Matrix.smul_stdBasisMatrix {m : Type u_2} {n : Type u_3} {R : Type u_4} {α : Type u_5} [DecidableEq m] [DecidableEq n] [Semiring α] [SMulZeroClass R α] (r : R) (i : m) (j : n) (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) :
    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 : α) :
    theorem Matrix.mulVec_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_5} [DecidableEq m] [DecidableEq n] [Semiring α] [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_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 = i : m, j : n, Matrix.stdBasisMatrix i j (x i j)
    theorem Matrix.std_basis_eq_basis_mul_basis {m : Type u_2} {n : Type u_3} {α : Type u_5} [DecidableEq m] [DecidableEq n] [Semiring α] (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] [Semiring α] [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 pP qP (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 α] [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 pP qP (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 : α) :
    @[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.stdBasisMatrix i j c).diag = 0
    @[simp]
    theorem Matrix.StdBasisMatrix.diag_same {n : Type u_3} {α : Type u_5} [DecidableEq n] [Semiring α] (i : n) (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.stdBasisMatrix i j c).trace = 0
    @[simp]
    theorem Matrix.StdBasisMatrix.trace_eq {n : Type u_3} {α : Type u_5} [DecidableEq n] [Semiring α] (i : n) (c : α) [Fintype n] :
    (Matrix.stdBasisMatrix i i c).trace = 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.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 α) :
    (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.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 α) :
    (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 : α) :
    @[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 : α) :
    theorem Matrix.row_eq_zero_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_5} [DecidableEq n] [Semiring α] [Fintype n] {i : n} {j : n} {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] [Semiring α] [Fintype n] {i : n} {j : n} {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] [Semiring α] [Fintype n] {i : n} {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] [Semiring α] [Fintype n] {M : Matrix n n α} (hM : Pairwise fun (i j : n) => Commute (Matrix.stdBasisMatrix i j 1) M) :

    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] [Semiring α] [Fintype n] {M : Matrix n n α} :
    M Set.range (Matrix.scalar n) ∀ (i j : n), i jCommute (Matrix.stdBasisMatrix i j 1) M
    theorem Matrix.mem_range_scalar_iff_commute_stdBasisMatrix' {n : Type u_3} {α : Type u_5} [DecidableEq n] [Semiring α] [Fintype n] {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.​