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.

@[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

@[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

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

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

theorem Matrix.single_apply {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) : single i j c i' j' = if i = i' ∧ j = j' then c else 0

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.

@[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)

@[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)

@[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

@[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

@[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)

theorem Matrix.single_mem_matrix {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [Zero α] {S : Set α} (hS : 0 ∈ S) {i : m} {j : n} {a : α} : single i j a ∈ S.matrix ↔ a ∈ S

theorem Matrix.diagonal_single {m : Type u_2} {α : Type u_7} [DecidableEq m] [Zero α] (i : m) (r : α) : diagonal (Pi.single i r) = single i i r

@[simp]

theorem Matrix.submatrix_single_equiv {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] [Zero α] (f : l ≃ n) (g : m ≃ o) (i : n) (j : o) (r : α) : (single i j r).submatrix ⇑f ⇑g = single (f.symm i) (g.symm j) r

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

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)

theorem Matrix.sum_single_eq_diagonal {m : Type u_2} {α : Type u_7} [DecidableEq m] [AddCommMonoid α] [Fintype m] (f : m → α) : ∑ i : m, single i i (f i) = diagonal f

theorem Matrix.sum_single_one {m : Type u_2} {α : Type u_7} [DecidableEq m] [AddCommMonoid α] [One α] [Fintype m] : ∑ i : m, single i i 1 = 1

theorem Matrix.sum_single_natCast {m : Type u_2} {α : Type u_7} [DecidableEq m] [AddCommMonoidWithOne α] [Fintype m] (n : ℕ) : ∑ i : m, single i i ↑n = ↑n

theorem Matrix.sum_single_ofNat {m : Type u_2} {α : Type u_7} [DecidableEq m] [AddCommMonoidWithOne α] [Fintype m] (n : ℕ) [n.AtLeastTwo] : ∑ i : m, single i i (OfNat.ofNat n) = OfNat.ofNat n

theorem Matrix.sum_single_intCast {m : Type u_2} {α : Type u_7} [DecidableEq m] [AddCommGroupWithOne α] [Fintype m] (z : ℤ) : ∑ i : m, single i i ↑z = ↑z

theorem Matrix.sum_sum_single {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] [Fintype m] [Fintype n] (x : m → n → α) : ∑ i : m, ∑ j : n, single i j (x i j) = of x

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)

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) : single i j 1 = vecMulVec (Pi.single i 1) (Pi.single j 1)

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 p → P q → P (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 p → P q → P (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.

@[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 : α) : (singleAddMonoidHom i j) a = single i j a

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.

@[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✝

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 β] : (m → n → α →ₗ[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.

theorem Matrix.liftLinear_apply {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 : m → n → α →ₗ[R] β) (M : Matrix m n α) : ((liftLinear S) f) M = ∑ i : m, ∑ j : n, (f i j) (M i j)

@[simp]

theorem Matrix.liftLinear_single {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 : m → n → α →ₗ[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 : m → n → α →ₗ[R] β) (i : m) (j : n) : (liftLinear S) f ∘ₗ singleLinearMap R i j = f i j

@[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 α] : (liftLinear S) (singleLinearMap R) = LinearMap.id

@[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

@[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

@[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

@[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

@[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

@[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

@[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)

@[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)

@[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

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

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

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

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 ∈ Set.range ⇑(scalar n)

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 ≠ j → Commute (single i j 1) M

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.

theorem Matrix.center_eq_scalar_image {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] : Set.center (Matrix n n α) = ⇑(scalar n) '' Set.center α

The center of Matrix n n α is equal to the image of the center of α under scalar n.

theorem Matrix.submonoidCenter_eq_scalar_map {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] : Submonoid.center (Matrix n n α) = Submonoid.map (scalar n) (Submonoid.center α)

theorem Matrix.subsemigroupCenter_eq_scalar_map {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] : Subsemigroup.center (Matrix n n α) = Subsemigroup.map (↑↑(scalar n)) (Subsemigroup.center α)

theorem Matrix.subsemiringCenter_eq_scalar_map {n : Type u_3} {α : Type u_7} [DecidableEq n] [Fintype n] [Semiring α] : Subsemiring.center (Matrix n n α) = Subsemiring.map (scalar n) (Subsemiring.center α)

theorem Matrix.subringCenter_eq_scalar_map {n : Type u_3} (R : Type u_5) [DecidableEq n] [Fintype n] [Ring R] : Subring.center (Matrix n n R) = Subring.map (scalar n) (Subring.center R)

@[simp]

theorem Matrix.center_eq_range {n : Type u_3} (R : Type u_5) [DecidableEq n] [Fintype n] [CommSemiring R] : Set.center (Matrix n n R) = Set.range ⇑(scalar n)

For a commutative semiring R, the center of Matrix n n R is the range of scalar n (i.e., the span of {1}).