Matrix.StdBasisMatrix.mul_right_apply_same
theorem Matrix.StdBasisMatrix.mul_right_apply_same :
∀ {n : Type u_3} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Semiring α] (i j : n) (c : α) [inst_2 : Fintype n]
(a : n) (M : Matrix n n α), (M * Matrix.stdBasisMatrix i j c) a j = M a i * c
The theorem `Matrix.StdBasisMatrix.mul_right_apply_same` states that for any type `n` with decidable equality and any semiring `α`, given indices `i`, `j` of type `n`, a scalar `c` of type `α`, a matrix `M` of type `Matrix n n α`, and an index `a` of type `n`, the result of multiplying matrix `M` with the standard basis matrix at indices `i`, `j` with value `c` and then applying the resulting matrix at indices `a`, `j` is equal to the product of the element at indices `a`, `i` of the matrix `M` and scalar `c`. This theorem essentially describes a property of matrix multiplication with respect to standard basis matrices.
More concisely: For any semiring α and type n with decidable equality, the product of matrix M with the standard basis matrix at indices i, j multiplied by scalar c, and then applying the resulting matrix at indices a, j, equals the product of the element at indices a, i of matrix M and scalar c.
|
Matrix.StdBasisMatrix.apply_of_ne
theorem Matrix.StdBasisMatrix.apply_of_ne :
∀ {m : Type u_2} {n : Type u_3} {α : Type u_5} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
(i : m) (j : n) (c : α) (i' : m) (j' : n), ¬(i = i' ∧ j = j') → Matrix.stdBasisMatrix i j c i' j' = 0
The theorem `Matrix.StdBasisMatrix.apply_of_ne` states that for any types `m`, `n`, and `α` with decidable equality (`DecidableEq`) and a semiring structure on `α`, and for any elements `i, i'` of type `m`, `j, j'` of type `n`, and `c` of type `α`, if `(i, j)` is not equal to `(i', j')`, then the entry of the standard basis matrix `stdBasisMatrix` at the position `(i', j')`, created with `i, j, c` as parameters, is zero.
In other words, the standard basis matrix created with `i, j, c` has `c` at the `i-th` row and `j-th` column, and zeroes elsewhere. The theorem specifically asserts that if we're looking at a position `(i', j')` that is not the same as `(i, j)`, then the value at that position in the matrix will be zero.
More concisely: For any types `m`, `n`, and `α` with decidable equality and a semiring structure, the standard basis matrix `stdBasisMatrix` has entry `0` at position `(i', j')` whenever `(i, j)` is not equal to `(i', j')`.
|
Matrix.StdBasisMatrix.mul_left_apply_same
theorem Matrix.StdBasisMatrix.mul_left_apply_same :
∀ {n : Type u_3} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Semiring α] (i j : n) (c : α) [inst_2 : Fintype n]
(b : n) (M : Matrix n n α), (Matrix.stdBasisMatrix i j c * M) i b = c * M j b
The theorem `Matrix.StdBasisMatrix.mul_left_apply_same` states that for any given semiring `α`, indices `i`, `j` and `b`, a scalar `c` of `α`, and a square matrix `M` indexed by `n` with elements in `α`, if we left multiply the standard basis matrix (where the `i`-th row and `j`-th column is `c` and zeroes elsewhere) with `M`, the `i`-th row and `b`-th column of the resulting matrix is equal to `c` times the `j`-th row and `b`-th column of `M`. This theorem assumes that equality in the index set `n` is decidable and that `n` is finite.
More concisely: For any square matrix M indexed by a finite and decidably equated set, the product of the standard basis matrix with row i and column j, and M, equals the product of the scalar c and the product of row i and column j of M.
|