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 v} [DecidableEq α] [Fintype m] [Fintype n] : DecidableEq (Matrix m n α)

Equations

• Matrix.decidableEq = Fintype.decidablePiFintype

instance Matrix.instFintypeOfDecidableEq {n : Type u_10} {m : Type u_11} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (α : Type u_12) [Fintype α] : Fintype (Matrix m n α)

Equations

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

instance Matrix.instFinite {n : Type u_10} {m : Type u_11} [Finite m] [Finite n] (α : Type u_12) [Finite α] : Finite (Matrix m n α)

def Matrix.ofLinearEquiv {m : Type u_2} {n : Type u_3} (R : Type u_7) {α : Type v} [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 v} [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 v} [Semiring R] [AddCommMonoid α] [Module R α] : ⇑(ofLinearEquiv R).symm = ⇑of.symm

theorem Matrix.sum_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [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 v) [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 v) [DecidableEq n] [AddZeroClass α] (d : n → α) : (diagonalAddMonoidHom n α) d = diagonal d

def Matrix.diagonalLinearMap (n : Type u_3) (R : Type u_7) (α : Type v) [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 v) [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 v} [DecidableEq n] [Zero α] [One α] [Preorder α] [ZeroLEOneClass α] (i j : n) : 0 ≤ 1 i j

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

def Matrix.diagAddMonoidHom (n : Type u_3) (α : Type v) [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 v) [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 v) [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 v) [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 v} [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 v} [AddCommMonoid α] (s : Multiset (Matrix n n α)) : s.sum.diag = (Multiset.map diag s).sum

@[simp]

theorem Matrix.diag_sum {n : Type u_3} {α : Type v} {ι : Type u_10} [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 v) [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 v) [NonAssocSemiring α] [Fintype n] [DecidableEq n] (d : n → α) : (diagonalRingHom n α) d = diagonal d

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

def Matrix.scalar {α : Type v} [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 v} [Semiring α] [DecidableEq n] [Fintype n] (a : α) : (scalar n) a = diagonal fun (x : n) => a

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

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

theorem Matrix.scalar_commute {n : Type u_3} {α : Type v} [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 v} [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 v} [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 v} [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 v} [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 v} {β : Type w} [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 v} [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 v} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Algebra R α] (d : n → α) : (diagonalAlgHom R) d = diagonal d

def Matrix.entryAddHom {m : Type u_2} {n : Type u_3} (α : Type v) [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 v) [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 v} [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 v) [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 v) [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 v} [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 v} [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 v} [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 v) [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 v) [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 v} [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 v} [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 v} [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 v} [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 v} {β : Type w} (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 v} {β : Type w} (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 v} : (Equiv.refl α).mapMatrix = Equiv.refl (Matrix m n α)

@[simp]

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

@[simp]

theorem Equiv.mapMatrix_trans {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} (f : α ≃ β) (g : β ≃ γ) : f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix

def AddMonoidHom.mapMatrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [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 v} {β : Type w} [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 v} [AddZeroClass α] : (id α).mapMatrix = id (Matrix m n α)

@[simp]

theorem AddMonoidHom.mapMatrix_comp {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} [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 v} {β : Type w} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (i : m) (j : n) : (Matrix.entryAddMonoidHom β i j).comp f.mapMatrix = f.comp (Matrix.entryAddMonoidHom α i j)

def AddEquiv.mapMatrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [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 v} {β : Type w} [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 v} [Add α] : (refl α).mapMatrix = refl (Matrix m n α)

@[simp]

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

@[simp]

theorem AddEquiv.mapMatrix_trans {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} [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 v} {β : Type w} [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} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α →ₗ[R] β) : Matrix m n α →ₗ[R] 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} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α →ₗ[R] β) (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 v} [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} {α : Type v} {β : Type w} {γ : Type u_9} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (f : β →ₗ[R] γ) (g : α →ₗ[R] β) : 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} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α →ₗ[R] β) (i : m) (j : n) : Matrix.entryLinearMap R β i j ∘ₗ f.mapMatrix = f ∘ₗ Matrix.entryLinearMap R α i j

def LinearEquiv.mapMatrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α ≃ₗ[R] β) : Matrix m n α ≃ₗ[R] 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} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α ≃ₗ[R] β) (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 v} [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} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α ≃ₗ[R] β) : f.mapMatrix.symm = f.symm.mapMatrix

@[simp]

theorem LinearEquiv.mapMatrix_trans {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} {γ : Type u_9} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (f : α ≃ₗ[R] β) (g : β ≃ₗ[R] γ) : f.mapMatrix ≪≫ₗ g.mapMatrix = (f ≪≫ₗ g).mapMatrix

@[simp]

theorem LinearEquiv.mapMatrix_toLinearMap {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α ≃ₗ[R] β) : ↑f.mapMatrix = (↑f).mapMatrix

@[simp]

theorem LinearEquiv.entryLinearMap_comp_mapMatrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α ≃ₗ[R] β) (i : m) (j : n) : Matrix.entryLinearMap R β i j ∘ₗ ↑f.mapMatrix = ↑f ∘ₗ Matrix.entryLinearMap R α i j

def RingHom.mapMatrix {m : Type u_2} {α : Type v} {β : Type w} [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 v} {β : Type w} [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 v} [Fintype m] [DecidableEq m] [NonAssocSemiring α] : (id α).mapMatrix = id (Matrix m m α)

@[simp]

theorem RingHom.mapMatrix_comp {m : Type u_2} {α : Type v} {β : Type w} {γ : Type u_9} [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 v} {β : Type w} [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 v} {β : Type w} [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 v} [Fintype m] [DecidableEq m] [NonAssocSemiring α] : (refl α).mapMatrix = refl (Matrix m m α)

@[simp]

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

@[simp]

theorem RingEquiv.mapMatrix_trans {m : Type u_2} {α : Type v} {β : Type w} {γ : Type u_9} [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 v} [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_apply {m : Type u_2} {α : Type v} [Fintype m] [NonAssocSemiring α] (M : Matrix m m αᵐᵒᵖ) : mopMatrix M = MulOpposite.op (M.transpose.map MulOpposite.unop)

@[simp]

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

def AlgHom.mapMatrix {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [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 v} {β : Type w} [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 v} [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 v} {β : Type w} {γ : Type u_9} [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 v} {β : Type w} [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 v} {β : Type w} [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 v} [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 v} {β : Type w} [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 v} {β : Type w} {γ : Type u_9} [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 v} [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_apply {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] (M : Matrix m m αᵐᵒᵖ) : mopMatrix M = MulOpposite.op (M.transpose.map MulOpposite.unop)

@[simp]

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

def Matrix.transposeAddEquiv (m : Type u_2) (n : Type u_3) (α : Type v) [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 v) [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 v) [Add α] : (transposeAddEquiv m n α).symm = transposeAddEquiv n m α

theorem Matrix.transpose_list_sum {m : Type u_2} {n : Type u_3} {α : Type v} [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 v} [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 v} [AddCommMonoid α] {ι : Type u_10} (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 v) [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 v) [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 v) [Semiring R] [AddCommMonoid α] [Module R α] : (transposeLinearEquiv m n R α).symm = transposeLinearEquiv n m R α

def Matrix.transposeRingEquiv (m : Type u_2) (α : Type v) [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 v) [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 v) [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 v} [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 v} [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 v) [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_symm_apply (m : Type u_2) (R : Type u_7) (α : Type v) [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✝

@[simp]

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