Documentation

Mathlib.Data.Matrix.Basic

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

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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