Matrices with a single non-zero element. #
This file provides Matrix.single
. The matrix Matrix.single i j c
has c
at position (i, j)
, and zeroes elsewhere.
single i j a
is the matrix with a
in the i
-th row, j
-th column,
and zeroes elsewhere.
Instances For
Alias of Matrix.single
.
single i j a
is the matrix with a
in the i
-th row, j
-th column,
and zeroes elsewhere.
Equations
Instances For
Alias of Matrix.single_eq_of_single_single
.
Alias of Matrix.of_symm_single
.
Alias of Matrix.smul_single
.
Alias of Matrix.single_zero
.
Alias of Matrix.transpose_single
.
Alias of Matrix.map_single
.
Alias of Matrix.single_add
.
Alias of Matrix.single_mulVec
.
Alias of Matrix.matrix_eq_sum_single
.
Alias of Matrix.single_eq_single_vecMulVec_single
.
Matrix.single
as a bundled additive map.
Equations
- Matrix.singleAddMonoidHom i j = { toFun := Matrix.single i j, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Alias of Matrix.singleAddMonoidHom
.
Matrix.single
as a bundled additive map.
Instances For
Matrix.single
as a bundled linear map.
Equations
- Matrix.singleLinearMap R i j = { toFun := (↑(Matrix.singleAddMonoidHom i j)).toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Alias of Matrix.singleLinearMap
.
Matrix.single
as a bundled linear map.
Instances For
Additive maps from finite matrices are equal if they agree on the standard basis.
See note [partially-applied ext lemmas].
Linear maps from finite matrices are equal if they agree on the standard basis.
See note [partially-applied ext lemmas].
Alias of Matrix.single_apply_same
.
Alias of Matrix.single_apply_of_ne
.
Alias of Matrix.single_apply_of_row_ne
.
Alias of Matrix.single_apply_of_col_ne
.
Alias of Matrix.diag_single_of_ne
.
Alias of Matrix.diag_single_same
.
Alias of Matrix.single_mul_apply_same
.
Alias of Matrix.mul_single_apply_same
.
Alias of Matrix.single_mul_apply_of_ne
.
Alias of Matrix.mul_single_apply_of_ne
.
Alias of Matrix.single_mul_single_same
.
Alias of Matrix.single_mul_mul_single
.
Alias of Matrix.single_mul_single_of_ne
.
Alias of Matrix.row_eq_zero_of_commute_single
.
Alias of Matrix.col_eq_zero_of_commute_single
.
Alias of Matrix.diag_eq_of_commute_single
.
Alias of Matrix.mem_range_scalar_of_commute_single
.
M
is a scalar matrix if it commutes with every non-diagonal single
.
Alias of Matrix.mem_range_scalar_iff_commute_single'
.
M
is a scalar matrix if and only if it commutes with every single
.