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
Instances For
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 : α)
:
@[simp]
theorem
Matrix.of_symm_stdBasisMatrix
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Zero α]
(i : m)
(j : n)
(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 : α)
:
@[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)
:
@[simp]
theorem
Matrix.transpose_stdBasisMatrix
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Zero α]
(i : m)
(j : n)
(a : α)
:
@[simp]
theorem
Matrix.map_stdBasisMatrix
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Zero α]
(i : m)
(j : n)
(a : α)
{β : Type u_7}
[Zero β]
{F : Type u_8}
[FunLike F α β]
[ZeroHomClass F α β]
(f : F)
:
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 : α)
:
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 → α)
:
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 α)
:
@[deprecated Matrix.matrix_eq_sum_stdBasisMatrix (since := "2024-08-11")]
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 α)
:
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)
:
@[deprecated Matrix.stdBasisMatrix_eq_single_vecMulVec_single (since := "2024-08-11")]
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)
:
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 (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 (stdBasisMatrix i j x))
:
P M
def
Matrix.stdBasisMatrixAddMonoidHom
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[AddCommMonoid α]
(i : m)
(j : n)
:
Matrix.stdBasisMatrix
as a bundled additive map.
Equations
- Matrix.stdBasisMatrixAddMonoidHom i j = { toFun := Matrix.stdBasisMatrix i j, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
Matrix.stdBasisMatrixAddMonoidHom_apply
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[AddCommMonoid α]
(i : m)
(j : n)
(a : α)
:
def
Matrix.stdBasisMatrixLinearMap
{m : Type u_2}
{n : Type u_3}
(R : Type u_4)
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring R]
[AddCommMonoid α]
[Module R α]
(i : m)
(j : n)
:
Matrix.stdBasisMatrix
as a bundled linear map.
Equations
- Matrix.stdBasisMatrixLinearMap R i j = { toFun := (↑(Matrix.stdBasisMatrixAddMonoidHom i j)).toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
Matrix.stdBasisMatrixLinearMap_apply
{m : Type u_2}
{n : Type u_3}
(R : Type u_4)
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring R]
[AddCommMonoid α]
[Module R α]
(i : m)
(j : n)
(a✝ : α)
:
theorem
Matrix.ext_addMonoidHom
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
{β : Type u_6}
[DecidableEq m]
[DecidableEq n]
[Finite m]
[Finite n]
[AddCommMonoid α]
[AddCommMonoid β]
⦃f g : Matrix m n α →+ β⦄
(h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j))
:
Additive maps from finite matrices are equal if they agree on the standard basis.
See note [partially-applied ext lemmas].
theorem
Matrix.ext_linearMap
{m : Type u_2}
{n : Type u_3}
(R : Type u_4)
{α : Type u_5}
{β : Type u_6}
[DecidableEq m]
[DecidableEq n]
[Finite m]
[Finite n]
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
⦃f g : Matrix m n α →ₗ[R] β⦄
(h : ∀ (i : m) (j : n), f ∘ₗ stdBasisMatrixLinearMap R i j = g ∘ₗ stdBasisMatrixLinearMap R i j)
:
Linear maps from finite matrices are equal if they agree on the standard basis.
See note [partially-applied ext lemmas].
@[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 : α)
:
@[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'))
:
@[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 : α)
:
@[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 : α)
:
@[simp]
theorem
Matrix.StdBasisMatrix.diag_zero
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Zero α]
(i j : n)
(c : α)
(h : j ≠ i)
:
@[simp]
theorem
Matrix.StdBasisMatrix.diag_same
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Zero α]
(i : n)
(c : α)
:
@[simp]
theorem
Matrix.StdBasisMatrix.mul_left_apply_same
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq l]
[DecidableEq m]
[Fintype m]
[NonUnitalNonAssocSemiring α]
(c : α)
(i : l)
(j : m)
(b : n)
(M : Matrix m n α)
:
@[simp]
theorem
Matrix.StdBasisMatrix.mul_right_apply_same
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Fintype m]
[NonUnitalNonAssocSemiring α]
(c : α)
(i : m)
(j : n)
(a : l)
(M : Matrix l m α)
:
@[simp]
theorem
Matrix.StdBasisMatrix.mul_left_apply_of_ne
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq l]
[DecidableEq m]
[Fintype m]
[NonUnitalNonAssocSemiring α]
(c : α)
(i : l)
(j : m)
(a : l)
(b : n)
(h : a ≠ i)
(M : Matrix m n α)
:
@[simp]
theorem
Matrix.StdBasisMatrix.mul_right_apply_of_ne
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Fintype m]
[NonUnitalNonAssocSemiring α]
(c : α)
(i : m)
(j : n)
(a : l)
(b : n)
(hbj : b ≠ j)
(M : Matrix l m α)
:
@[simp]
theorem
Matrix.StdBasisMatrix.mul_same
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq l]
[DecidableEq m]
[DecidableEq n]
[Fintype m]
[NonUnitalNonAssocSemiring α]
(c : α)
(i : l)
(j : m)
(k : n)
(d : α)
:
@[simp]
theorem
Matrix.StdBasisMatrix.mul_of_ne
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq l]
[DecidableEq m]
[DecidableEq n]
[Fintype m]
[NonUnitalNonAssocSemiring α]
(c : α)
(i : l)
(j k : m)
{l✝ : n}
(h : j ≠ k)
(d : α)
:
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 (stdBasisMatrix i j 1) M)
(hkj : k ≠ j)
:
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 (stdBasisMatrix i j 1) M)
(hki : k ≠ i)
:
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 (stdBasisMatrix i j 1) M)
:
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 (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]
[Fintype n]
[Semiring α]
{M : Matrix n n α}
:
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
is a scalar matrix if and only if it commutes with every stdBasisMatrix
.