Matrices

This file contains basic results on matrices including bundled versions of matrix operators.

Implementation notes

For convenience, Matrix m n α is defined as m → n → α, as this allows elements of the matrix to be accessed with A i j. However, it is not advisable to construct matrices using terms of the form fun i j ↦ _ or even (fun i j ↦ _ : Matrix m n α), as these are not recognized by Lean as having the right type. Instead, Matrix.of should be used.

TODO

Under various conditions, multiplication of infinite matrices makes sense. These have not yet been implemented.

instance Matrix.decidableEq {m : Type u_2} {n : Type u_3} {α : Type u_11} [DecidableEq α] [Fintype m] [Fintype n] : DecidableEq (Matrix m n α)

Equations

• Matrix.decidableEq = Fintype.decidablePiFintype

instance Matrix.instFintypeOfDecidableEq {n : Type u_14} {m : Type u_15} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (α : Type u_16) [Fintype α] : Fintype (Matrix m n α)

Equations

• Matrix.instFintypeOfDecidableEq α = inferInstanceAs (Fintype (m → n → α))

instance Matrix.instFinite {n : Type u_14} {m : Type u_15} [Finite m] [Finite n] (α : Type u_16) [Finite α] : Finite (Matrix m n α)

def Matrix.ofLinearEquiv {m : Type u_2} {n : Type u_3} (R : Type u_7) {α : Type u_11} [Semiring R] [AddCommMonoid α] [Module R α] : (m → n → α) ≃ₗ[R] Matrix m n α

This is Matrix.of bundled as a linear equivalence.

Equations

• Matrix.ofLinearEquiv R = { toFun := Matrix.ofAddEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := Matrix.ofAddEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Matrix.coe_ofLinearEquiv {m : Type u_2} {n : Type u_3} (R : Type u_7) {α : Type u_11} [Semiring R] [AddCommMonoid α] [Module R α] : ⇑(ofLinearEquiv R) = ⇑of

@[simp]

theorem Matrix.coe_ofLinearEquiv_symm {m : Type u_2} {n : Type u_3} (R : Type u_7) {α : Type u_11} [Semiring R] [AddCommMonoid α] [Module R α] : ⇑(ofLinearEquiv R).symm = ⇑of.symm

theorem Matrix.sum_apply {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [AddCommMonoid α] (i : m) (j : n) (s : Finset β) (g : β → Matrix m n α) : (∑ c ∈ s, g c) i j = ∑ c ∈ s, g c i j

def Matrix.diagonalAddMonoidHom (n : Type u_3) (α : Type u_11) [DecidableEq n] [AddZeroClass α] : (n → α) →+ Matrix n n α

Matrix.diagonal as an AddMonoidHom.

Equations

• Matrix.diagonalAddMonoidHom n α = { toFun := Matrix.diagonal, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.diagonalAddMonoidHom_apply (n : Type u_3) (α : Type u_11) [DecidableEq n] [AddZeroClass α] (d : n → α) : (diagonalAddMonoidHom n α) d = diagonal d

def Matrix.diagonalLinearMap (n : Type u_3) (R : Type u_7) (α : Type u_11) [DecidableEq n] [Semiring R] [AddCommMonoid α] [Module R α] : (n → α) →ₗ[R] Matrix n n α

Matrix.diagonal as a LinearMap.

Equations

• Matrix.diagonalLinearMap n R α = { toFun := (↑(Matrix.diagonalAddMonoidHom n α)).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Matrix.diagonalLinearMap_apply (n : Type u_3) (R : Type u_7) (α : Type u_11) [DecidableEq n] [Semiring R] [AddCommMonoid α] [Module R α] (a✝ : n → α) : (diagonalLinearMap n R α) a✝ = (↑(diagonalAddMonoidHom n α)).toFun a✝

theorem Matrix.zero_le_one_elem {n : Type u_3} {α : Type u_11} [DecidableEq n] [Zero α] [One α] [Preorder α] [ZeroLEOneClass α] (i j : n) : 0 ≤ 1 i j

theorem Matrix.zero_le_one_row {n : Type u_3} {α : Type u_11} [DecidableEq n] [Zero α] [One α] [Preorder α] [ZeroLEOneClass α] (i : n) : 0 ≤ 1 i

def Matrix.diagAddMonoidHom (n : Type u_3) (α : Type u_11) [AddZeroClass α] : Matrix n n α →+ n → α

Matrix.diag as an AddMonoidHom.

Equations

• Matrix.diagAddMonoidHom n α = { toFun := Matrix.diag, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.diagAddMonoidHom_apply (n : Type u_3) (α : Type u_11) [AddZeroClass α] (A : Matrix n n α) (i : n) : (diagAddMonoidHom n α) A i = A.diag i

def Matrix.diagLinearMap (n : Type u_3) (R : Type u_7) (α : Type u_11) [Semiring R] [AddCommMonoid α] [Module R α] : Matrix n n α →ₗ[R] n → α

Matrix.diag as a LinearMap.

Equations

• Matrix.diagLinearMap n R α = { toFun := (↑(Matrix.diagAddMonoidHom n α)).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Matrix.diagLinearMap_apply (n : Type u_3) (R : Type u_7) (α : Type u_11) [Semiring R] [AddCommMonoid α] [Module R α] (a✝ : Matrix n n α) (a✝¹ : n) : (diagLinearMap n R α) a✝ a✝¹ = (↑(diagAddMonoidHom n α)).toFun a✝ a✝¹

@[simp]

theorem Matrix.diag_list_sum {n : Type u_3} {α : Type u_11} [AddMonoid α] (l : List (Matrix n n α)) : l.sum.diag = (List.map diag l).sum

@[simp]

theorem Matrix.diag_multiset_sum {n : Type u_3} {α : Type u_11} [AddCommMonoid α] (s : Multiset (Matrix n n α)) : s.sum.diag = (Multiset.map diag s).sum

@[simp]

theorem Matrix.diag_sum {n : Type u_3} {α : Type u_11} {ι : Type u_14} [AddCommMonoid α] (s : Finset ι) (f : ι → Matrix n n α) : (∑ i ∈ s, f i).diag = ∑ i ∈ s, (f i).diag

def Matrix.diagonalRingHom (n : Type u_3) (α : Type u_11) [NonAssocSemiring α] [Fintype n] [DecidableEq n] : (n → α) →+* Matrix n n α

Matrix.diagonal as a RingHom.

Equations

• Matrix.diagonalRingHom n α = { toFun := Matrix.diagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.diagonalRingHom_apply (n : Type u_3) (α : Type u_11) [NonAssocSemiring α] [Fintype n] [DecidableEq n] (d : n → α) : (diagonalRingHom n α) d = diagonal d

theorem Matrix.diagonal_pow {n : Type u_3} {α : Type u_11} [Semiring α] [Fintype n] [DecidableEq n] (v : n → α) (k : ℕ) : diagonal v ^ k = diagonal (v ^ k)

def Matrix.scalar {α : Type u_11} [Semiring α] (n : Type u) [DecidableEq n] [Fintype n] : α →+* Matrix n n α

The ring homomorphism α →+* Matrix n n α sending a to the diagonal matrix with a on the diagonal.

Equations

• Matrix.scalar n = (Matrix.diagonalRingHom n α).comp (Pi.constRingHom n α)

@[simp]

theorem Matrix.scalar_apply {n : Type u_3} {α : Type u_11} [Semiring α] [DecidableEq n] [Fintype n] (a : α) : (scalar n) a = diagonal fun (x : n) => a

theorem Matrix.scalar_inj {n : Type u_3} {α : Type u_11} [Semiring α] [DecidableEq n] [Fintype n] [Nonempty n] {r s : α} : (scalar n) r = (scalar n) s ↔ r = s

theorem Matrix.scalar_comm_iff {m : Type u_2} {n : Type u_3} {α : Type u_11} [Semiring α] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] {r : α} {M : Matrix m n α} : (scalar m) r * M = M * (scalar n) r ↔ r • M = MulOpposite.op r • M

A version of Matrix.scalar_commute_iff for rectangular matrices.

theorem Matrix.scalar_commute_iff {n : Type u_3} {α : Type u_11} [Semiring α] [DecidableEq n] [Fintype n] {r : α} {M : Matrix n n α} : Commute ((scalar n) r) M ↔ r • M = MulOpposite.op r • M

theorem Matrix.scalar_comm {m : Type u_2} {n : Type u_3} {α : Type u_11} [Semiring α] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (r : α) (hr : ∀ (r' : α), Commute r r') (M : Matrix m n α) : (scalar m) r * M = M * (scalar n) r

A version of Matrix.scalar_commute for rectangular matrices.

theorem Matrix.scalar_commute {n : Type u_3} {α : Type u_11} [Semiring α] [DecidableEq n] [Fintype n] (r : α) (hr : ∀ (r' : α), Commute r r') (M : Matrix n n α) : Commute ((scalar n) r) M

instance Matrix.instAlgebra {n : Type u_3} {R : Type u_7} {α : Type u_11} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] : Algebra R (Matrix n n α)

Equations

• Matrix.instAlgebra = { toSMul := Matrix.smul, algebraMap := (Matrix.scalar n).comp (algebraMap R α), commutes' := ⋯, smul_def' := ⋯ }

theorem Matrix.algebraMap_matrix_apply {n : Type u_3} {R : Type u_7} {α : Type u_11} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] {r : R} {i j : n} : (algebraMap R (Matrix n n α)) r i j = if i = j then (algebraMap R α) r else 0

theorem Matrix.algebraMap_eq_diagonal {n : Type u_3} {R : Type u_7} {α : Type u_11} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] (r : R) : (algebraMap R (Matrix n n α)) r = diagonal ((algebraMap R (n → α)) r)

theorem Matrix.algebraMap_eq_diagonalRingHom {n : Type u_3} {R : Type u_7} {α : Type u_11} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] : algebraMap R (Matrix n n α) = (diagonalRingHom n α).comp (algebraMap R (n → α))

@[simp]

theorem Matrix.map_algebraMap {n : Type u_3} {R : Type u_7} {α : Type u_11} {β : Type u_12} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (r : R) (f : α → β) (hf : f 0 = 0) (hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r) : ((algebraMap R (Matrix n n α)) r).map f = (algebraMap R (Matrix n n β)) r

def Matrix.diagonalAlgHom {n : Type u_3} (R : Type u_7) {α : Type u_11} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] : (n → α) →ₐ[R] Matrix n n α

Matrix.diagonal as an AlgHom.

Equations

• Matrix.diagonalAlgHom R = { toFun := Matrix.diagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Matrix.diagonalAlgHom_apply {n : Type u_3} (R : Type u_7) {α : Type u_11} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] (d : n → α) : (diagonalAlgHom R) d = diagonal d

def Matrix.scalarAlgHom (n : Type u_3) (R : Type u_7) {α : Type u_11} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] : α →ₐ[R] Matrix n n α

Matrix.scalar as an AlgHom.

Equations

• Matrix.scalarAlgHom n R = { toRingHom := Matrix.scalar n, commutes' := ⋯ }

@[simp]

theorem Matrix.scalarAlgHom_apply (n : Type u_3) (R : Type u_7) {α : Type u_11} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] (a : α) : (scalarAlgHom n R) a = (scalar n) a

def Matrix.entryAddHom {m : Type u_2} {n : Type u_3} (α : Type u_11) [Add α] (i : m) (j : n) : Matrix m n α →ₙ+ α

Extracting entries from a matrix as an additive homomorphism.

Equations

• Matrix.entryAddHom α i j = { toFun := fun (M : Matrix m n α) => M i j, map_add' := ⋯ }

@[simp]

theorem Matrix.entryAddHom_apply {m : Type u_2} {n : Type u_3} (α : Type u_11) [Add α] (i : m) (j : n) (M : Matrix m n α) : (entryAddHom α i j) M = M i j

theorem Matrix.entryAddHom_eq_comp {m : Type u_2} {n : Type u_3} {α : Type u_11} [Add α] {i : m} {j : n} : entryAddHom α i j = ((Pi.evalAddHom (fun (x : n) => α) j).comp (Pi.evalAddHom (fun (i : m) => n → α) i)).comp ↑ofAddEquiv.symm

def Matrix.entryAddMonoidHom {m : Type u_2} {n : Type u_3} (α : Type u_11) [AddZeroClass α] (i : m) (j : n) : Matrix m n α →+ α

Extracting entries from a matrix as an additive monoid homomorphism. Note this cannot be upgraded to a ring homomorphism, as it does not respect multiplication.

Equations

• Matrix.entryAddMonoidHom α i j = { toFun := fun (M : Matrix m n α) => M i j, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.entryAddMonoidHom_apply {m : Type u_2} {n : Type u_3} (α : Type u_11) [AddZeroClass α] (i : m) (j : n) (M : Matrix m n α) : (entryAddMonoidHom α i j) M = M i j

theorem Matrix.entryAddMonoidHom_eq_comp {m : Type u_2} {n : Type u_3} {α : Type u_11} [AddZeroClass α] {i : m} {j : n} : entryAddMonoidHom α i j = ((Pi.evalAddMonoidHom (fun (x : n) => α) j).comp (Pi.evalAddMonoidHom (fun (i : m) => n → α) i)).comp ↑ofAddEquiv.symm

@[simp]

theorem Matrix.evalAddMonoidHom_comp_diagAddMonoidHom {m : Type u_2} {α : Type u_11} [AddZeroClass α] (i : m) : (Pi.evalAddMonoidHom (fun (i : m) => α) i).comp (diagAddMonoidHom m α) = entryAddMonoidHom α i i

@[simp]

theorem Matrix.entryAddMonoidHom_toAddHom {m : Type u_2} {n : Type u_3} {α : Type u_11} [AddZeroClass α] {i : m} {j : n} : ↑(entryAddMonoidHom α i j) = entryAddHom α i j

def Matrix.entryLinearMap {m : Type u_2} {n : Type u_3} (R : Type u_7) (α : Type u_11) [Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) : Matrix m n α →ₗ[R] α

Extracting entries from a matrix as a linear map. Note this cannot be upgraded to an algebra homomorphism, as it does not respect multiplication.

Equations

• Matrix.entryLinearMap R α i j = { toFun := fun (M : Matrix m n α) => M i j, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Matrix.entryLinearMap_apply {m : Type u_2} {n : Type u_3} (R : Type u_7) (α : Type u_11) [Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) (M : Matrix m n α) : (entryLinearMap R α i j) M = M i j

theorem Matrix.entryLinearMap_eq_comp {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [Semiring R] [AddCommMonoid α] [Module R α] {i : m} {j : n} : entryLinearMap R α i j = LinearMap.proj j ∘ₗ LinearMap.proj i ∘ₗ ↑(ofLinearEquiv R).symm

@[simp]

theorem Matrix.proj_comp_diagLinearMap {m : Type u_2} {R : Type u_7} {α : Type u_11} [Semiring R] [AddCommMonoid α] [Module R α] (i : m) : LinearMap.proj i ∘ₗ diagLinearMap m R α = entryLinearMap R α i i

@[simp]

theorem Matrix.entryLinearMap_toAddMonoidHom {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [Semiring R] [AddCommMonoid α] [Module R α] {i : m} {j : n} : ↑(entryLinearMap R α i j) = entryAddMonoidHom α i j

@[simp]

theorem Matrix.entryLinearMap_toAddHom {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [Semiring R] [AddCommMonoid α] [Module R α] {i : m} {j : n} : ↑(entryLinearMap R α i j) = entryAddHom α i j

Bundled versions of Matrix.map

def Equiv.mapMatrix {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} (f : α ≃ β) : Matrix m n α ≃ Matrix m n β

The Equiv between spaces of matrices induced by an Equiv between their coefficients. This is Matrix.map as an Equiv.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m n α) => M.map ⇑f, invFun := fun (M : Matrix m n β) => M.map ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.mapMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} (f : α ≃ β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

@[simp]

theorem Equiv.mapMatrix_refl {m : Type u_2} {n : Type u_3} {α : Type u_11} : (Equiv.refl α).mapMatrix = Equiv.refl (Matrix m n α)

@[simp]

theorem Equiv.mapMatrix_symm {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} (f : α ≃ β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem Equiv.mapMatrix_trans {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} {γ : Type u_13} (f : α ≃ β) (g : β ≃ γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

def AddMonoidHom.mapMatrix {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) : Matrix m n α →+ Matrix m n β

The AddMonoidHom between spaces of matrices induced by an AddMonoidHom between their coefficients. This is Matrix.map as an AddMonoidHom.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m n α) => M.map ⇑f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.mapMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

@[simp]

theorem AddMonoidHom.mapMatrix_id {m : Type u_2} {n : Type u_3} {α : Type u_11} [AddZeroClass α] : (id α).mapMatrix = id (Matrix m n α)

@[simp]

theorem AddMonoidHom.mapMatrix_comp {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+ γ) (g : α →+ β) : f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix

@[simp]

theorem AddMonoidHom.entryAddMonoidHom_comp_mapMatrix {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (i : m) (j : n) : (Matrix.entryAddMonoidHom β i j).comp f.mapMatrix = f.comp (Matrix.entryAddMonoidHom α i j)

@[simp]

theorem AddMonoidHom.mapMatrix_zero {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [AddZeroClass α] [AddZeroClass β] : mapMatrix 0 = 0

@[simp]

theorem AddMonoidHom.mapMatrix_add {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [AddZeroClass α] [AddCommMonoid β] (f g : α →+ β) : (f + g).mapMatrix = f.mapMatrix + g.mapMatrix

@[simp]

theorem AddMonoidHom.mapMatrix_sub {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [AddZeroClass α] [AddCommGroup β] (f g : α →+ β) : (f - g).mapMatrix = f.mapMatrix - g.mapMatrix

@[simp]

theorem AddMonoidHom.mapMatrix_neg {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [AddZeroClass α] [AddCommGroup β] (f : α →+ β) : (-f).mapMatrix = -f.mapMatrix

@[simp]

theorem AddMonoidHom.mapMatrix_smul {m : Type u_2} {n : Type u_3} {A : Type u_10} {α : Type u_11} {β : Type u_12} [Monoid A] [AddZeroClass α] [AddMonoid β] [DistribMulAction A β] (a : A) (f : α →+ β) : (a • f).mapMatrix = a • f.mapMatrix

def AddEquiv.mapMatrix {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [Add α] [Add β] (f : α ≃+ β) : Matrix m n α ≃+ Matrix m n β

The AddEquiv between spaces of matrices induced by an AddEquiv between their coefficients. This is Matrix.map as an AddEquiv.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m n α) => M.map ⇑f, invFun := fun (M : Matrix m n β) => M.map ⇑f.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem AddEquiv.mapMatrix_apply {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [Add α] [Add β] (f : α ≃+ β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

@[simp]

theorem AddEquiv.mapMatrix_refl {m : Type u_2} {n : Type u_3} {α : Type u_11} [Add α] : (refl α).mapMatrix = refl (Matrix m n α)

@[simp]

theorem AddEquiv.mapMatrix_symm {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [Add α] [Add β] (f : α ≃+ β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem AddEquiv.mapMatrix_trans {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [Add α] [Add β] [Add γ] (f : α ≃+ β) (g : β ≃+ γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

@[simp]

theorem AddEquiv.entryAddHom_comp_mapMatrix {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [Add α] [Add β] (f : α ≃+ β) (i : m) (j : n) : (Matrix.entryAddHom β i j).comp ↑f.mapMatrix = (↑f).comp (Matrix.entryAddHom α i j)

def LinearMap.mapMatrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] (f : α →ₛₗ[σᵣₛ] β) : Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β

The LinearMap between spaces of matrices induced by a LinearMap between their coefficients. This is Matrix.map as a LinearMap.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m n α) => M.map ⇑f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.mapMatrix_apply {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] (f : α →ₛₗ[σᵣₛ] β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

@[simp]

theorem LinearMap.mapMatrix_id {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [Semiring R] [AddCommMonoid α] [Module R α] : id.mapMatrix = id

@[simp]

theorem LinearMap.mapMatrix_comp {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {T : Type u_9} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [Semiring R] [Semiring S] [Semiring T] {σᵣₛ : R →+* S} {σₛₜ : S →+* T} {σᵣₜ : R →+* T} [RingHomCompTriple σᵣₛ σₛₜ σᵣₜ] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module S β] [Module T γ] (f : β →ₛₗ[σₛₜ] γ) (g : α →ₛₗ[σᵣₛ] β) : f.mapMatrix ∘ₛₗ g.mapMatrix = (f ∘ₛₗ g).mapMatrix

@[simp]

theorem LinearMap.entryLinearMap_comp_mapMatrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] (f : α →ₛₗ[σᵣₛ] β) (i : m) (j : n) : Matrix.entryLinearMap S β i j ∘ₛₗ f.mapMatrix = f ∘ₛₗ Matrix.entryLinearMap R α i j

@[simp]

theorem LinearMap.mapMatrix_zero {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] : mapMatrix 0 = 0

@[simp]

theorem LinearMap.mapMatrix_add {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] (f g : α →ₛₗ[σᵣₛ] β) : (f + g).mapMatrix = f.mapMatrix + g.mapMatrix

@[simp]

theorem LinearMap.mapMatrix_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {A : Type u_10} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] [Monoid A] [DistribMulAction A β] [SMulCommClass S A β] (a : A) (f : α →ₛₗ[σᵣₛ] β) : (a • f).mapMatrix = a • f.mapMatrix

def LinearMap.mapMatrixLinear {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} (A : Type u_10) {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] [Semiring A] [Module A β] [SMulCommClass S A β] : (α →ₛₗ[σᵣₛ] β) →ₗ[A] Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β

LinearMap.mapMatrix is itself linear in the map being applied.

Alternative, this is Matrix.map as a bilinear map.

Equations

• LinearMap.mapMatrixLinear A = { toFun := LinearMap.mapMatrix, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.mapMatrixLinear_apply {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} (A : Type u_10) {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] [Semiring A] [Module A β] [SMulCommClass S A β] (f : α →ₛₗ[σᵣₛ] β) : (mapMatrixLinear A) f = f.mapMatrix

@[simp]

theorem LinearMap.mapMatrix_sub {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommGroup β] [Module R α] [Module S β] (f g : α →ₛₗ[σᵣₛ] β) : (f - g).mapMatrix = f.mapMatrix - g.mapMatrix

@[simp]

theorem LinearMap.mapMatrix_neg {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] {σᵣₛ : R →+* S} [AddCommMonoid α] [AddCommGroup β] [Module R α] [Module S β] (f : α →ₛₗ[σᵣₛ] β) : (-f).mapMatrix = -f.mapMatrix

def LinearEquiv.mapMatrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] {σᵣₛ : R →+* S} {σₛᵣ : S →+* R} [RingHomInvPair σᵣₛ σₛᵣ] [RingHomInvPair σₛᵣ σᵣₛ] (f : α ≃ₛₗ[σᵣₛ] β) : Matrix m n α ≃ₛₗ[σᵣₛ] Matrix m n β

The LinearEquiv between spaces of matrices induced by a LinearEquiv between their coefficients. This is Matrix.map as a LinearEquiv.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m n α) => M.map ⇑f, map_add' := ⋯, map_smul' := ⋯, invFun := fun (M : Matrix m n β) => M.map ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearEquiv.mapMatrix_apply {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] {σᵣₛ : R →+* S} {σₛᵣ : S →+* R} [RingHomInvPair σᵣₛ σₛᵣ] [RingHomInvPair σₛᵣ σᵣₛ] (f : α ≃ₛₗ[σᵣₛ] β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f

@[simp]

theorem LinearEquiv.mapMatrix_refl {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [Semiring R] [AddCommMonoid α] [Module R α] : (refl R α).mapMatrix = refl R (Matrix m n α)

@[simp]

theorem LinearEquiv.mapMatrix_symm {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] {σᵣₛ : R →+* S} {σₛᵣ : S →+* R} [RingHomInvPair σᵣₛ σₛᵣ] [RingHomInvPair σₛᵣ σᵣₛ] (f : α ≃ₛₗ[σᵣₛ] β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem LinearEquiv.mapMatrix_trans {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {T : Type u_9} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [Semiring R] [Semiring S] [Semiring T] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module S β] [Module T γ] {σᵣₛ : R →+* S} {σₛₜ : S →+* T} {σᵣₜ : R →+* T} [RingHomCompTriple σᵣₛ σₛₜ σᵣₜ] {σₛᵣ : S →+* R} {σₜₛ : T →+* S} {σₜᵣ : T →+* R} [RingHomCompTriple σₜₛ σₛᵣ σₜᵣ] [RingHomInvPair σᵣₛ σₛᵣ] [RingHomInvPair σₛᵣ σᵣₛ] [RingHomInvPair σₛₜ σₜₛ] [RingHomInvPair σₜₛ σₛₜ] [RingHomInvPair σᵣₜ σₜᵣ] [RingHomInvPair σₜᵣ σᵣₜ] (f : α ≃ₛₗ[σᵣₛ] β) (g : β ≃ₛₗ[σₛₜ] γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

@[simp]

theorem LinearEquiv.mapMatrix_toLinearMap {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] {σᵣₛ : R →+* S} {σₛᵣ : S →+* R} [RingHomInvPair σᵣₛ σₛᵣ] [RingHomInvPair σₛᵣ σᵣₛ] (f : α ≃ₛₗ[σᵣₛ] β) : ↑f.mapMatrix = (↑f).mapMatrix

theorem LinearEquiv.entryLinearMap_comp_mapMatrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module S β] {σᵣₛ : R →+* S} {σₛᵣ : S →+* R} [RingHomInvPair σᵣₛ σₛᵣ] [RingHomInvPair σₛᵣ σᵣₛ] (f : α ≃ₛₗ[σᵣₛ] β) (i : m) (j : n) : Matrix.entryLinearMap S β i j ∘ₛₗ ↑f.mapMatrix = ↑f ∘ₛₗ Matrix.entryLinearMap R α i j

def RingHom.mapMatrix {m : Type u_2} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) : Matrix m m α →+* Matrix m m β

The RingHom between spaces of square matrices induced by a RingHom between their coefficients. This is Matrix.map as a RingHom.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m m α) => M.map ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.mapMatrix_apply {m : Type u_2} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f

@[simp]

theorem RingHom.mapMatrix_id {m : Type u_2} {α : Type u_11} [Fintype m] [DecidableEq m] [NonAssocSemiring α] : (id α).mapMatrix = id (Matrix m m α)

@[simp]

theorem RingHom.mapMatrix_comp {m : Type u_2} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] [NonAssocSemiring γ] (f : β →+* γ) (g : α →+* β) : f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix

def RingEquiv.mapMatrix {m : Type u_2} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α ≃+* β) : Matrix m m α ≃+* Matrix m m β

The RingEquiv between spaces of square matrices induced by a RingEquiv between their coefficients. This is Matrix.map as a RingEquiv.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m m α) => M.map ⇑f, invFun := fun (M : Matrix m m β) => M.map ⇑f.symm, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingEquiv.mapMatrix_apply {m : Type u_2} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α ≃+* β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f

@[simp]

theorem RingEquiv.mapMatrix_refl {m : Type u_2} {α : Type u_11} [Fintype m] [DecidableEq m] [NonAssocSemiring α] : (refl α).mapMatrix = refl (Matrix m m α)

@[simp]

theorem RingEquiv.mapMatrix_symm {m : Type u_2} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α ≃+* β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem RingEquiv.mapMatrix_trans {m : Type u_2} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] [NonAssocSemiring γ] (f : α ≃+* β) (g : β ≃+* γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

def RingEquiv.mopMatrix {m : Type u_2} {α : Type u_11} [Fintype m] [NonAssocSemiring α] : Matrix m m αᵐᵒᵖ ≃+* (Matrix m m α)ᵐᵒᵖ

For any ring R, we have ring isomorphism Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RingEquiv.mopMatrix_symm_apply {m : Type u_2} {α : Type u_11} [Fintype m] [NonAssocSemiring α] (M : (Matrix m m α)ᵐᵒᵖ) : mopMatrix.symm M = (MulOpposite.unop M).transpose.map MulOpposite.op

@[simp]

theorem RingEquiv.mopMatrix_apply {m : Type u_2} {α : Type u_11} [Fintype m] [NonAssocSemiring α] (M : Matrix m m αᵐᵒᵖ) : mopMatrix M = MulOpposite.op (M.transpose.map MulOpposite.unop)

def AlgHom.mapMatrix {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) : Matrix m m α →ₐ[R] Matrix m m β

The AlgHom between spaces of square matrices induced by an AlgHom between their coefficients. This is Matrix.map as an AlgHom.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m m α) => M.map ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgHom.mapMatrix_apply {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f

@[simp]

theorem AlgHom.mapMatrix_id {m : Type u_2} {R : Type u_7} {α : Type u_11} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] : (AlgHom.id R α).mapMatrix = AlgHom.id R (Matrix m m α)

@[simp]

theorem AlgHom.mapMatrix_comp {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Semiring γ] [Algebra R α] [Algebra R β] [Algebra R γ] (f : β →ₐ[R] γ) (g : α →ₐ[R] β) : f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix

def AlgEquiv.mapMatrix {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α ≃ₐ[R] β) : Matrix m m α ≃ₐ[R] Matrix m m β

The AlgEquiv between spaces of square matrices induced by an AlgEquiv between their coefficients. This is Matrix.map as an AlgEquiv.

Equations

• f.mapMatrix = { toFun := fun (M : Matrix m m α) => M.map ⇑f, invFun := fun (M : Matrix m m β) => M.map ⇑f.symm, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgEquiv.mapMatrix_apply {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α ≃ₐ[R] β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f

@[simp]

theorem AlgEquiv.mapMatrix_refl {m : Type u_2} {R : Type u_7} {α : Type u_11} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] : refl.mapMatrix = refl

@[simp]

theorem AlgEquiv.mapMatrix_symm {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α ≃ₐ[R] β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem AlgEquiv.mapMatrix_trans {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Semiring γ] [Algebra R α] [Algebra R β] [Algebra R γ] (f : α ≃ₐ[R] β) (g : β ≃ₐ[R] γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

def AlgEquiv.mopMatrix {m : Type u_2} {R : Type u_7} {α : Type u_11} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] : Matrix m m αᵐᵒᵖ ≃ₐ[R] (Matrix m m α)ᵐᵒᵖ

For any algebra α over a ring R, we have an R-algebra isomorphism Matₙₓₙ(αᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose. If α is commutative, we can get rid of the ᵒᵖ in the left-hand side, see Matrix.transposeAlgEquiv.

Equations

• AlgEquiv.mopMatrix = { toEquiv := RingEquiv.mopMatrix.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgEquiv.mopMatrix_symm_apply {m : Type u_2} {R : Type u_7} {α : Type u_11} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] (M : (Matrix m m α)ᵐᵒᵖ) : mopMatrix.symm M = (MulOpposite.unop M).transpose.map MulOpposite.op

@[simp]

theorem AlgEquiv.mopMatrix_apply {m : Type u_2} {R : Type u_7} {α : Type u_11} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] (M : Matrix m m αᵐᵒᵖ) : mopMatrix M = MulOpposite.op (M.transpose.map MulOpposite.unop)

def AddSubmonoid.matrix {m : Type u_2} {n : Type u_3} {A : Type u_14} [AddMonoid A] (S : AddSubmonoid A) : AddSubmonoid (Matrix m n A)

A version of Set.matrix for AddSubmonoids. Given an AddSubmonoid S, S.matrix is the AddSubmonoid of matrices m all of whose entries m i j belong to S.

Equations

• S.matrix = { carrier := (↑S).matrix, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem AddSubmonoid.coe_matrix {m : Type u_2} {n : Type u_3} {A : Type u_14} [AddMonoid A] (S : AddSubmonoid A) : ↑S.matrix = (↑S).matrix

def AddSubgroup.matrix {m : Type u_2} {n : Type u_3} {A : Type u_14} [AddGroup A] (S : AddSubgroup A) : AddSubgroup (Matrix m n A)

A version of Set.matrix for AddSubgroups. Given an AddSubgroup S, S.matrix is the AddSubgroup of matrices m all of whose entries m i j belong to S.

Equations

• S.matrix = { toAddSubmonoid := S.matrix, neg_mem' := ⋯ }

@[simp]

theorem AddSubgroup.coe_matrix {m : Type u_2} {n : Type u_3} {A : Type u_14} [AddGroup A] (S : AddSubgroup A) : ↑S.matrix = (↑S).matrix

def Subsemiring.matrix {n : Type u_3} {R : Type u_14} [NonAssocSemiring R] [Fintype n] [DecidableEq n] (S : Subsemiring R) : Subsemiring (Matrix n n R)

A version of Set.matrix for Subsemirings. Given a Subsemiring S, S.matrix is the Subsemiring of square matrices m all of whose entries m i j belong to S.

Equations

• S.matrix = { carrier := S.toAddSubmonoid.matrix.carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Subsemiring.coe_matrix {n : Type u_3} {R : Type u_14} [NonAssocSemiring R] [Fintype n] [DecidableEq n] (S : Subsemiring R) : ↑S.matrix = S.toAddSubmonoid.matrix.carrier

def Subring.matrix {n : Type u_3} {R : Type u_14} [Ring R] [Fintype n] [DecidableEq n] (S : Subring R) : Subring (Matrix n n R)

A version of Set.matrix for Subrings. Given a Subring S, S.matrix is the Subring of square matrices m all of whose entries m i j belong to S.

Equations

• S.matrix = { toSubsemiring := S.matrix, neg_mem' := ⋯ }

@[simp]

theorem Subring.coe_matrix {n : Type u_3} {R : Type u_14} [Ring R] [Fintype n] [DecidableEq n] (S : Subring R) : ↑S.matrix = S.toAddSubmonoid.matrix.carrier

def Submodule.matrix {m : Type u_2} {n : Type u_3} {R : Type u_14} {M : Type u_15} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) : Submodule R (Matrix m n M)

A version of Set.matrix for Submodules. Given a Submodule S, S.matrix is the Submodule of matrices m all of whose entries m i j belong to S.

Equations

• S.matrix = { toAddSubmonoid := S.matrix, smul_mem' := ⋯ }

@[simp]

theorem Submodule.coe_matrix {m : Type u_2} {n : Type u_3} {R : Type u_14} {M : Type u_15} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) : ↑S.matrix = (↑S).matrix

def Matrix.transposeAddEquiv (m : Type u_2) (n : Type u_3) (α : Type u_11) [Add α] : Matrix m n α ≃+ Matrix n m α

Matrix.transpose as an AddEquiv

Equations

• Matrix.transposeAddEquiv m n α = { toFun := Matrix.transpose, invFun := Matrix.transpose, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.transposeAddEquiv_apply (m : Type u_2) (n : Type u_3) (α : Type u_11) [Add α] (M : Matrix m n α) : (transposeAddEquiv m n α) M = M.transpose

@[simp]

theorem Matrix.transposeAddEquiv_symm (m : Type u_2) (n : Type u_3) (α : Type u_11) [Add α] : (transposeAddEquiv m n α).symm = transposeAddEquiv n m α

theorem Matrix.transpose_list_sum {m : Type u_2} {n : Type u_3} {α : Type u_11} [AddMonoid α] (l : List (Matrix m n α)) : l.sum.transpose = (List.map transpose l).sum

theorem Matrix.transpose_multiset_sum {m : Type u_2} {n : Type u_3} {α : Type u_11} [AddCommMonoid α] (s : Multiset (Matrix m n α)) : s.sum.transpose = (Multiset.map transpose s).sum

theorem Matrix.transpose_sum {m : Type u_2} {n : Type u_3} {α : Type u_11} [AddCommMonoid α] {ι : Type u_14} (s : Finset ι) (M : ι → Matrix m n α) : (∑ i ∈ s, M i).transpose = ∑ i ∈ s, (M i).transpose

def Matrix.transposeLinearEquiv (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type u_11) [Semiring R] [AddCommMonoid α] [Module R α] : Matrix m n α ≃ₗ[R] Matrix n m α

Matrix.transpose as a LinearMap

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.transposeLinearEquiv_apply (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type u_11) [Semiring R] [AddCommMonoid α] [Module R α] (a✝ : Matrix m n α) : (transposeLinearEquiv m n R α) a✝ = (transposeAddEquiv m n α).toFun a✝

@[simp]

theorem Matrix.transposeLinearEquiv_symm (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type u_11) [Semiring R] [AddCommMonoid α] [Module R α] : (transposeLinearEquiv m n R α).symm = transposeLinearEquiv n m R α

def Matrix.transposeRingEquiv (m : Type u_2) (α : Type u_11) [AddCommMonoid α] [CommSemigroup α] [Fintype m] : Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ

Matrix.transpose as a RingEquiv to the opposite ring

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.transposeRingEquiv_symm_apply (m : Type u_2) (α : Type u_11) [AddCommMonoid α] [CommSemigroup α] [Fintype m] (M : (Matrix m m α)ᵐᵒᵖ) : (transposeRingEquiv m α).symm M = (MulOpposite.unop M).transpose

@[simp]

theorem Matrix.transposeRingEquiv_apply (m : Type u_2) (α : Type u_11) [AddCommMonoid α] [CommSemigroup α] [Fintype m] (M : Matrix m m α) : (transposeRingEquiv m α) M = MulOpposite.op M.transpose

@[simp]

theorem Matrix.transpose_pow {m : Type u_2} {α : Type u_11} [CommSemiring α] [Fintype m] [DecidableEq m] (M : Matrix m m α) (k : ℕ) : (M ^ k).transpose = M.transpose ^ k

theorem Matrix.transpose_list_prod {m : Type u_2} {α : Type u_11} [CommSemiring α] [Fintype m] [DecidableEq m] (l : List (Matrix m m α)) : l.prod.transpose = (List.map transpose l).reverse.prod

def Matrix.transposeAlgEquiv (m : Type u_2) (R : Type u_7) (α : Type u_11) [CommSemiring R] [CommSemiring α] [Fintype m] [DecidableEq m] [Algebra R α] : Matrix m m α ≃ₐ[R] (Matrix m m α)ᵐᵒᵖ

Matrix.transpose as an AlgEquiv to the opposite ring

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.transposeAlgEquiv_apply (m : Type u_2) (R : Type u_7) (α : Type u_11) [CommSemiring R] [CommSemiring α] [Fintype m] [DecidableEq m] [Algebra R α] (M : Matrix m m α) : (transposeAlgEquiv m R α) M = MulOpposite.op M.transpose

@[simp]

theorem Matrix.transposeAlgEquiv_symm_apply (m : Type u_2) (R : Type u_7) (α : Type u_11) [CommSemiring R] [CommSemiring α] [Fintype m] [DecidableEq m] [Algebra R α] (a✝ : (Matrix m m α)ᵐᵒᵖ) : (transposeAlgEquiv m R α).symm a✝ = ((transposeAddEquiv m m α).trans MulOpposite.opAddEquiv).invFun a✝

theorem Matrix.sum_mulVec {m : Type u_2} {n : Type u_3} {α : Type u_11} {ι : Type u_14} [NonUnitalNonAssocSemiring α] [Fintype n] (s : Finset ι) (x : ι → Matrix m n α) (y : n → α) : (∑ i ∈ s, x i).mulVec y = ∑ i ∈ s, (x i).mulVec y

theorem Matrix.mulVec_sum {m : Type u_2} {n : Type u_3} {α : Type u_11} {ι : Type u_14} [NonUnitalNonAssocSemiring α] [Fintype n] (x : Matrix m n α) (s : Finset ι) (y : ι → n → α) : x.mulVec (∑ i ∈ s, y i) = ∑ i ∈ s, x.mulVec (y i)

theorem Matrix.sum_vecMul {m : Type u_2} {n : Type u_3} {α : Type u_11} {ι : Type u_14} [NonUnitalNonAssocSemiring α] [Fintype n] (s : Finset ι) (x : ι → n → α) (y : Matrix n m α) : vecMul (∑ i ∈ s, x i) y = ∑ i ∈ s, vecMul (x i) y

theorem Matrix.vecMul_sum {m : Type u_2} {n : Type u_3} {α : Type u_11} {ι : Type u_14} [NonUnitalNonAssocSemiring α] [Fintype n] (x : n → α) (s : Finset ι) (y : ι → Matrix n m α) : vecMul x (∑ i ∈ s, y i) = ∑ i ∈ s, vecMul x (y i)