Documentation

Mathlib.Data.Matrix.Basis

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.

def Matrix.single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
Matrix m n α

single i j a is the matrix with a in the i-th row, j-th column, and zeroes elsewhere.

Equations
Instances For
    @[deprecated Matrix.single (since := "2025-05-05")]
    def Matrix.stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
    Matrix m n α

    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
      theorem Matrix.single_eq_of_single_single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
      single i j a = of (Pi.single i (Pi.single j a))

      See also single_eq_updateRow_zero and single_eq_updateCol_zero.

      @[deprecated Matrix.single_eq_of_single_single (since := "2025-05-05")]
      theorem Matrix.stdBasisMatrix_eq_of_single_single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
      single i j a = of (Pi.single i (Pi.single j a))

      Alias of Matrix.single_eq_of_single_single.


      See also single_eq_updateRow_zero and single_eq_updateCol_zero.

      @[simp]
      theorem Matrix.of_symm_single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
      of.symm (single i j a) = Pi.single i (Pi.single j a)
      @[deprecated Matrix.of_symm_single (since := "2025-05-05")]
      theorem Matrix.of_symm_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
      of.symm (single i j a) = Pi.single i (Pi.single j a)

      Alias of Matrix.of_symm_single.

      @[simp]
      theorem Matrix.smul_single {m : Type u_2} {n : Type u_3} {R : Type u_5} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] [SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α) :
      r single i j a = single i j (r a)
      @[deprecated Matrix.smul_single (since := "2025-05-05")]
      theorem Matrix.smul_stdBasisMatrix {m : Type u_2} {n : Type u_3} {R : Type u_5} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] [SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α) :
      r single i j a = single i j (r a)

      Alias of Matrix.smul_single.

      @[simp]
      theorem Matrix.single_zero {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) :
      single i j 0 = 0
      @[deprecated Matrix.single_zero (since := "2025-05-05")]
      theorem Matrix.stdBasisMatrix_zero {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) :
      single i j 0 = 0

      Alias of Matrix.single_zero.

      @[simp]
      theorem Matrix.transpose_single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
      (single i j a).transpose = single j i a
      @[deprecated Matrix.transpose_single (since := "2025-05-05")]
      theorem Matrix.transpose_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
      (single i j a).transpose = single j i a

      Alias of Matrix.transpose_single.

      @[simp]
      theorem Matrix.map_single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) {β : Type u_10} [Zero β] {F : Type u_11} [FunLike F α β] [ZeroHomClass F α β] (f : F) :
      (single i j a).map f = single i j (f a)
      @[deprecated Matrix.map_single (since := "2025-05-05")]
      theorem Matrix.map_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) {β : Type u_10} [Zero β] {F : Type u_11} [FunLike F α β] [ZeroHomClass F α β] (f : F) :
      (single i j a).map f = single i j (f a)

      Alias of Matrix.map_single.

      theorem Matrix.single_add {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [AddZeroClass α] (i : m) (j : n) (a b : α) :
      single i j (a + b) = single i j a + single i j b
      @[deprecated Matrix.single_add (since := "2025-05-05")]
      theorem Matrix.stdBasisMatrix_add {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [AddZeroClass α] (i : m) (j : n) (a b : α) :
      single i j (a + b) = single i j a + single i j b

      Alias of Matrix.single_add.

      theorem Matrix.single_mulVec {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [NonUnitalNonAssocSemiring α] [Fintype m] (i : n) (j : m) (c : α) (x : mα) :
      (single i j c).mulVec x = Function.update 0 i (c * x j)
      @[deprecated Matrix.single_mulVec (since := "2025-05-05")]
      theorem Matrix.mulVec_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [NonUnitalNonAssocSemiring α] [Fintype m] (i : n) (j : m) (c : α) (x : mα) :
      (single i j c).mulVec x = Function.update 0 i (c * x j)

      Alias of Matrix.single_mulVec.

      theorem Matrix.matrix_eq_sum_single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] [Fintype m] [Fintype n] (x : Matrix m n α) :
      x = i : m, j : n, single i j (x i j)
      @[deprecated Matrix.matrix_eq_sum_single (since := "2025-05-05")]
      theorem Matrix.matrix_eq_sum_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] [Fintype m] [Fintype n] (x : Matrix m n α) :
      x = i : m, j : n, single i j (x i j)

      Alias of Matrix.matrix_eq_sum_single.

      theorem Matrix.single_eq_single_vecMulVec_single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [MulZeroOneClass α] (i : m) (j : n) :
      @[deprecated Matrix.single_eq_single_vecMulVec_single (since := "2025-05-05")]
      theorem Matrix.stdBasisMatrix_eq_single_vecMulVec_single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [MulZeroOneClass α] (i : m) (j : n) :

      Alias of Matrix.single_eq_single_vecMulVec_single.

      theorem Matrix.induction_on' {m : Type u_2} {n : Type u_3} {α : Type u_7} [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 pP qP (p + q)) (h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)) :
      P M
      theorem Matrix.induction_on {m : Type u_2} {n : Type u_3} {α : Type u_7} [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 pP qP (p + q)) (h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)) :
      P M
      def Matrix.singleAddMonoidHom {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] (i : m) (j : n) :
      α →+ Matrix m n α

      Matrix.single as a bundled additive map.

      Equations
      Instances For
        @[simp]
        theorem Matrix.singleAddMonoidHom_apply {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] (i : m) (j : n) (a : α) :
        @[deprecated Matrix.singleAddMonoidHom (since := "2025-05-05")]
        def Matrix.stdBasisMatrixAddMonoidHom {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] (i : m) (j : n) :
        α →+ Matrix m n α

        Alias of Matrix.singleAddMonoidHom.


        Matrix.single as a bundled additive map.

        Equations
        Instances For
          def Matrix.singleLinearMap {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_7} [DecidableEq m] [DecidableEq n] [Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) :
          α →ₗ[R] Matrix m n α

          Matrix.single as a bundled linear map.

          Equations
          Instances For
            @[simp]
            theorem Matrix.singleLinearMap_apply {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_7} [DecidableEq m] [DecidableEq n] [Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) (a✝ : α) :
            (singleLinearMap R i j) a✝ = single i j a✝
            @[deprecated Matrix.singleLinearMap (since := "2025-05-05")]
            def Matrix.stdBasisMatrixLinearMap {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_7} [DecidableEq m] [DecidableEq n] [Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) :
            α →ₗ[R] Matrix m n α

            Alias of Matrix.singleLinearMap.


            Matrix.single as a bundled linear map.

            Equations
            Instances For
              theorem Matrix.ext_addMonoidHom {m : Type u_2} {n : Type u_3} {α : Type u_7} {β : Type u_8} [DecidableEq m] [DecidableEq n] [Finite m] [Finite n] [AddCommMonoid α] [AddCommMonoid β] f g : Matrix m n α →+ β (h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)) :
              f = g

              Additive maps from finite matrices are equal if they agree on the standard basis.

              See note [partially-applied ext lemmas].

              theorem Matrix.ext_addMonoidHom_iff {m : Type u_2} {n : Type u_3} {α : Type u_7} {β : Type u_8} [DecidableEq m] [DecidableEq n] [Finite m] [Finite n] [AddCommMonoid α] [AddCommMonoid β] {f g : Matrix m n α →+ β} :
              f = g ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
              theorem Matrix.ext_linearMap {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_7} {β : Type u_8} [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 ∘ₗ singleLinearMap R i j = g ∘ₗ singleLinearMap R i j) :
              f = g

              Linear maps from finite matrices are equal if they agree on the standard basis.

              See note [partially-applied ext lemmas].

              theorem Matrix.ext_linearMap_iff {m : Type u_2} {n : Type u_3} {R : Type u_5} {α : Type u_7} {β : Type u_8} [DecidableEq m] [DecidableEq n] [Finite m] [Finite n] [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] {f g : Matrix m n α →ₗ[R] β} :
              f = g ∀ (i : m) (j : n), f ∘ₗ singleLinearMap R i j = g ∘ₗ singleLinearMap R i j
              def Matrix.liftLinear {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} {β : Type u_8} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] [Semiring R] [Semiring S] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Module S β] [SMulCommClass R S β] :
              (mnα →ₗ[R] β) ≃ₗ[S] Matrix m n α →ₗ[R] β

              Families of linear maps acting on each element are equivalent to linear maps from a matrix.

              This can be thought of as the matrix version of LinearMap.lsum.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem Matrix.liftLinear_piSingle {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} {β : Type u_8} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] [Semiring R] [Semiring S] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Module S β] [SMulCommClass R S β] (f : mnα →ₗ[R] β) (i : m) (j : n) (a : α) :
                ((liftLinear S) f) (single i j a) = (f i j) a
                @[simp]
                theorem Matrix.liftLinear_comp_singleLinearMap {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} {β : Type u_8} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] [Semiring R] [Semiring S] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Module S β] [SMulCommClass R S β] (f : mnα →ₗ[R] β) (i : m) (j : n) :
                @[simp]
                theorem Matrix.liftLinear_singleLinearMap {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] [Semiring R] [Semiring S] [AddCommMonoid α] [Module R α] [Module S α] [SMulCommClass R S α] :
                @[simp]
                theorem Matrix.single_apply_same {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (c : α) :
                single i j c i j = c
                @[deprecated Matrix.single_apply_same (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.apply_same {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (c : α) :
                single i j c i j = c

                Alias of Matrix.single_apply_same.

                @[simp]
                theorem Matrix.single_apply_of_ne {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (c : α) (i' : m) (j' : n) (h : ¬(i = i' j = j')) :
                single i j c i' j' = 0
                @[deprecated Matrix.single_apply_of_ne (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.apply_of_ne {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (c : α) (i' : m) (j' : n) (h : ¬(i = i' j = j')) :
                single i j c i' j' = 0

                Alias of Matrix.single_apply_of_ne.

                theorem Matrix.single_apply_of_row_ne {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] {i i' : m} (hi : i i') (j j' : n) (a : α) :
                single i j a i' j' = 0
                @[deprecated Matrix.single_apply_of_row_ne (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.apply_of_row_ne {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] {i i' : m} (hi : i i') (j j' : n) (a : α) :
                single i j a i' j' = 0

                Alias of Matrix.single_apply_of_row_ne.

                theorem Matrix.single_apply_of_col_ne {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i i' : m) {j j' : n} (hj : j j') (a : α) :
                single i j a i' j' = 0
                @[deprecated Matrix.single_apply_of_col_ne (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.apply_of_col_ne {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] (i i' : m) {j j' : n} (hj : j j') (a : α) :
                single i j a i' j' = 0

                Alias of Matrix.single_apply_of_col_ne.

                @[simp]
                theorem Matrix.diag_single_of_ne {n : Type u_3} {α : Type u_7} [DecidableEq n] [Zero α] (i j : n) (c : α) (h : i j) :
                (single i j c).diag = 0
                @[deprecated Matrix.diag_single_of_ne (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.diag_zero {n : Type u_3} {α : Type u_7} [DecidableEq n] [Zero α] (i j : n) (c : α) (h : i j) :
                (single i j c).diag = 0

                Alias of Matrix.diag_single_of_ne.

                @[simp]
                theorem Matrix.diag_single_same {n : Type u_3} {α : Type u_7} [DecidableEq n] [Zero α] (i : n) (c : α) :
                (single i i c).diag = Pi.single i c
                @[deprecated Matrix.diag_single_same (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.diag_same {n : Type u_3} {α : Type u_7} [DecidableEq n] [Zero α] (i : n) (c : α) :
                (single i i c).diag = Pi.single i c

                Alias of Matrix.diag_single_same.

                @[simp]
                theorem Matrix.single_mul_apply_same {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq l] [DecidableEq m] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (b : n) (M : Matrix m n α) :
                (single i j c * M) i b = c * M j b
                @[deprecated Matrix.single_mul_apply_same (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.mul_left_apply_same {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq l] [DecidableEq m] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (b : n) (M : Matrix m n α) :
                (single i j c * M) i b = c * M j b

                Alias of Matrix.single_mul_apply_same.

                @[simp]
                theorem Matrix.mul_single_apply_same {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : m) (j : n) (a : l) (M : Matrix l m α) :
                (M * single i j c) a j = M a i * c
                @[deprecated Matrix.mul_single_apply_same (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.mul_right_apply_same {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : m) (j : n) (a : l) (M : Matrix l m α) :
                (M * single i j c) a j = M a i * c

                Alias of Matrix.mul_single_apply_same.

                @[simp]
                theorem Matrix.single_mul_apply_of_ne {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq l] [DecidableEq m] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (a : l) (b : n) (h : a i) (M : Matrix m n α) :
                (single i j c * M) a b = 0
                @[deprecated Matrix.single_mul_apply_of_ne (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.mul_left_apply_of_ne {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq l] [DecidableEq m] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (a : l) (b : n) (h : a i) (M : Matrix m n α) :
                (single i j c * M) a b = 0

                Alias of Matrix.single_mul_apply_of_ne.

                @[simp]
                theorem Matrix.mul_single_apply_of_ne {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : m) (j : n) (a : l) (b : n) (hbj : b j) (M : Matrix l m α) :
                (M * single i j c) a b = 0
                @[deprecated Matrix.mul_single_apply_of_ne (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.mul_right_apply_of_ne {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : m) (j : n) (a : l) (b : n) (hbj : b j) (M : Matrix l m α) :
                (M * single i j c) a b = 0

                Alias of Matrix.mul_single_apply_of_ne.

                @[simp]
                theorem Matrix.single_mul_single_same {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq l] [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (k : n) (d : α) :
                single i j c * single j k d = single i k (c * d)
                @[deprecated Matrix.single_mul_single_same (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.mul_same {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq l] [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (k : n) (d : α) :
                single i j c * single j k d = single i k (c * d)

                Alias of Matrix.single_mul_single_same.

                @[simp]
                theorem Matrix.single_mul_mul_single {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_7} [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq o] [Fintype m] [NonUnitalNonAssocSemiring α] [Fintype n] (i : l) (i' : m) (j' : n) (j : o) (a : α) (x : Matrix m n α) (b : α) :
                single i i' a * x * single j' j b = single i j (a * x i' j' * b)
                @[deprecated Matrix.single_mul_mul_single (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.stdBasisMatrix_mul_mul_stdBasisMatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_7} [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq o] [Fintype m] [NonUnitalNonAssocSemiring α] [Fintype n] (i : l) (i' : m) (j' : n) (j : o) (a : α) (x : Matrix m n α) (b : α) :
                single i i' a * x * single j' j b = single i j (a * x i' j' * b)

                Alias of Matrix.single_mul_mul_single.

                @[simp]
                theorem Matrix.single_mul_single_of_ne {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq l] [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j k : m) {l✝ : n} (h : j k) (d : α) :
                single i j c * single k l✝ d = 0
                @[deprecated Matrix.single_mul_single_of_ne (since := "2025-05-05")]
                theorem Matrix.StdBasisMatrix.mul_of_ne {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq l] [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j k : m) {l✝ : n} (h : j k) (d : α) :
                single i j c * single k l✝ d = 0

                Alias of Matrix.single_mul_single_of_ne.

                theorem Matrix.row_eq_zero_of_commute_single {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {i j k : n} {M : Matrix n n α} (hM : Commute (single i j 1) M) (hkj : k j) :
                M j k = 0
                @[deprecated Matrix.row_eq_zero_of_commute_single (since := "2025-05-05")]
                theorem Matrix.row_eq_zero_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {i j k : n} {M : Matrix n n α} (hM : Commute (single i j 1) M) (hkj : k j) :
                M j k = 0

                Alias of Matrix.row_eq_zero_of_commute_single.

                theorem Matrix.col_eq_zero_of_commute_single {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {i j k : n} {M : Matrix n n α} (hM : Commute (single i j 1) M) (hki : k i) :
                M k i = 0
                @[deprecated Matrix.col_eq_zero_of_commute_single (since := "2025-05-05")]
                theorem Matrix.col_eq_zero_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {i j k : n} {M : Matrix n n α} (hM : Commute (single i j 1) M) (hki : k i) :
                M k i = 0

                Alias of Matrix.col_eq_zero_of_commute_single.

                theorem Matrix.diag_eq_of_commute_single {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {i j : n} {M : Matrix n n α} (hM : Commute (single i j 1) M) :
                M i i = M j j
                @[deprecated Matrix.diag_eq_of_commute_single (since := "2025-05-05")]
                theorem Matrix.diag_eq_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {i j : n} {M : Matrix n n α} (hM : Commute (single i j 1) M) :
                M i i = M j j

                Alias of Matrix.diag_eq_of_commute_single.

                theorem Matrix.mem_range_scalar_of_commute_single {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} (hM : Pairwise fun (i j : n) => Commute (single i j 1) M) :

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

                @[deprecated Matrix.mem_range_scalar_of_commute_single (since := "2025-05-05")]
                theorem Matrix.mem_range_scalar_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} (hM : Pairwise fun (i j : n) => Commute (single i j 1) M) :

                Alias of Matrix.mem_range_scalar_of_commute_single.


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

                theorem Matrix.mem_range_scalar_iff_commute_single {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} :
                M Set.range (scalar n) ∀ (i j : n), i jCommute (single i j 1) M
                @[deprecated Matrix.mem_range_scalar_iff_commute_single (since := "2025-05-05")]
                theorem Matrix.mem_range_scalar_iff_commute_stdBasisMatrix {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} :
                M Set.range (scalar n) ∀ (i j : n), i jCommute (single i j 1) M

                Alias of Matrix.mem_range_scalar_iff_commute_single.

                theorem Matrix.mem_range_scalar_iff_commute_single' {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} :
                M Set.range (scalar n) ∀ (i j : n), Commute (single i j 1) M

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

                @[deprecated Matrix.mem_range_scalar_iff_commute_single' (since := "2025-05-05")]
                theorem Matrix.mem_range_scalar_iff_commute_stdBasisMatrix' {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} :
                M Set.range (scalar n) ∀ (i j : n), Commute (single i j 1) M

                Alias of Matrix.mem_range_scalar_iff_commute_single'.


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