Matrices

This file defines basic properties of matrices up to the module structure.

Matrices with rows indexed by m, columns indexed by n, and entries of type α are represented with Matrix m n α. For the typical approach of counting rows and columns, Matrix (Fin m) (Fin n) α can be used.

Main definitions

• Matrix.transpose: transpose of a matrix, turning rows into columns and vice versa
• Matrix.submatrix: take a submatrix by reindexing rows and columns
• Matrix.module: matrices are a module over the ring of entries

Notation

The locale Matrix gives the following notation:

• ᵀ for Matrix.transpose

See Mathlib/Data/Matrix/ConjTranspose.lean for

• ᴴ for Matrix.conjTranspose

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.

def Matrix (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)

Matrix m n R is the type of matrices with entries in R, whose rows are indexed by m and whose columns are indexed by n.

Equations

• Matrix m n α = (m → n → α)

theorem Matrix.ext_iff {m : Type u_2} {n : Type u_3} {α : Type v} {M N : Matrix m n α} : (∀ (i : m) (j : n), M i j = N i j) ↔ M = N

theorem Matrix.ext {m : Type u_2} {n : Type u_3} {α : Type v} {M N : Matrix m n α} : (∀ (i : m) (j : n), M i j = N i j) → M = N

def Matrix.of {m : Type u_2} {n : Type u_3} {α : Type v} : (m → n → α) ≃ Matrix m n α

Cast a function into a matrix.

The two sides of the equivalence are definitionally equal types. We want to use an explicit cast to distinguish the types because Matrix has different instances to pi types (such as Pi.mul, which performs elementwise multiplication, vs Matrix.mul).

If you are defining a matrix, in terms of its entries, use of (fun i j ↦ _). The purpose of this approach is to ensure that terms of the form (fun i j ↦ _) * (fun i j ↦ _) do not appear, as the type of * can be misleading.

Equations

• Matrix.of = Equiv.refl (m → n → α)

@[simp]

theorem Matrix.of_apply {m : Type u_2} {n : Type u_3} {α : Type v} (f : m → n → α) (i : m) (j : n) : of f i j = f i j

@[simp]

theorem Matrix.of_symm_apply {m : Type u_2} {n : Type u_3} {α : Type v} (f : Matrix m n α) (i : m) (j : n) : of.symm f i j = f i j

def Matrix.map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (M : Matrix m n α) (f : α → β) : Matrix m n β

M.map f is the matrix obtained by applying f to each entry of the matrix M.

This is available in bundled forms as:

• AddMonoidHom.mapMatrix
• LinearMap.mapMatrix
• RingHom.mapMatrix
• AlgHom.mapMatrix
• Equiv.mapMatrix
• AddEquiv.mapMatrix
• LinearEquiv.mapMatrix
• RingEquiv.mapMatrix
• AlgEquiv.mapMatrix

Equations

• M.map f = Matrix.of fun (i : m) (j : n) => f (M i j)

@[simp]

theorem Matrix.map_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {f : α → β} {i : m} {j : n} : M.map f i j = f (M i j)

@[simp]

theorem Matrix.map_id {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : M.map id = M

@[simp]

theorem Matrix.map_id' {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : (M.map fun (x : α) => x) = M

@[simp]

theorem Matrix.map_map {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {β : Type u_10} {γ : Type u_11} {f : α → β} {g : β → γ} : (M.map f).map g = M.map (g ∘ f)

theorem Matrix.map_injective {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} (hf : Function.Injective f) : Function.Injective fun (M : Matrix m n α) => M.map f

def Matrix.transpose {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : Matrix n m α

The transpose of a matrix.

Equations

• M.transpose = Matrix.of fun (x : n) (y : m) => M y x

@[simp]

theorem Matrix.transpose_apply {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) (i : n) (j : m) : M.transpose i j = M j i

def Matrix.«term_ᵀ» : Lean.TrailingParserDescr

The transpose of a matrix.

Equations

• Matrix.«term_ᵀ» = Lean.ParserDescr.trailingNode `Matrix.«term_ᵀ» 1024 1024 (Lean.ParserDescr.symbol "ᵀ")

instance Matrix.inhabited {m : Type u_2} {n : Type u_3} {α : Type v} [Inhabited α] : Inhabited (Matrix m n α)

Equations

• Matrix.inhabited = inferInstanceAs (Inhabited (m → n → α))

instance Matrix.add {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] : Add (Matrix m n α)

Equations

• Matrix.add = Pi.instAdd

instance Matrix.addSemigroup {m : Type u_2} {n : Type u_3} {α : Type v} [AddSemigroup α] : AddSemigroup (Matrix m n α)

Equations

• Matrix.addSemigroup = Pi.addSemigroup

instance Matrix.addCommSemigroup {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommSemigroup α] : AddCommSemigroup (Matrix m n α)

Equations

• Matrix.addCommSemigroup = Pi.addCommSemigroup

instance Matrix.zero {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] : Zero (Matrix m n α)

Equations

• Matrix.zero = Pi.instZero

instance Matrix.addZeroClass {m : Type u_2} {n : Type u_3} {α : Type v} [AddZeroClass α] : AddZeroClass (Matrix m n α)

Equations

• Matrix.addZeroClass = Pi.addZeroClass

instance Matrix.addMonoid {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] : AddMonoid (Matrix m n α)

Equations

• Matrix.addMonoid = Pi.addMonoid

instance Matrix.addCommMonoid {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] : AddCommMonoid (Matrix m n α)

Equations

• Matrix.addCommMonoid = Pi.addCommMonoid

instance Matrix.neg {m : Type u_2} {n : Type u_3} {α : Type v} [Neg α] : Neg (Matrix m n α)

Equations

• Matrix.neg = Pi.instNeg

instance Matrix.sub {m : Type u_2} {n : Type u_3} {α : Type v} [Sub α] : Sub (Matrix m n α)

Equations

• Matrix.sub = Pi.instSub

instance Matrix.addGroup {m : Type u_2} {n : Type u_3} {α : Type v} [AddGroup α] : AddGroup (Matrix m n α)

Equations

• Matrix.addGroup = Pi.addGroup

instance Matrix.addCommGroup {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommGroup α] : AddCommGroup (Matrix m n α)

Equations

• Matrix.addCommGroup = Pi.addCommGroup

instance Matrix.unique {m : Type u_2} {n : Type u_3} {α : Type v} [Unique α] : Unique (Matrix m n α)

Equations

• Matrix.unique = Pi.unique

instance Matrix.subsingleton {m : Type u_2} {n : Type u_3} {α : Type v} [Subsingleton α] : Subsingleton (Matrix m n α)

instance Matrix.nonempty {m : Type u_2} {n : Type u_3} {α : Type v} [Nonempty m] [Nonempty n] [Nontrivial α] : Nontrivial (Matrix m n α)

instance Matrix.smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [SMul R α] : SMul R (Matrix m n α)

Equations

• Matrix.smul = Pi.instSMul

instance Matrix.smulCommClass {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type v} [SMul R α] [SMul S α] [SMulCommClass R S α] : SMulCommClass R S (Matrix m n α)

instance Matrix.isScalarTower {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type v} [SMul R S] [SMul R α] [SMul S α] [IsScalarTower R S α] : IsScalarTower R S (Matrix m n α)

instance Matrix.isCentralScalar {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] : IsCentralScalar R (Matrix m n α)

instance Matrix.mulAction {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Monoid R] [MulAction R α] : MulAction R (Matrix m n α)

Equations

• Matrix.mulAction = Pi.mulAction R

instance Matrix.distribMulAction {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Monoid R] [AddMonoid α] [DistribMulAction R α] : DistribMulAction R (Matrix m n α)

Equations

• Matrix.distribMulAction = Pi.distribMulAction R

instance Matrix.module {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Semiring R] [AddCommMonoid α] [Module R α] : Module R (Matrix m n α)

Equations

• Matrix.module = Pi.module m (fun (a : m) => n → α) R

@[simp]

theorem Matrix.zero_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] (i : m) (j : n) : 0 i j = 0

@[simp]

theorem Matrix.add_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] (A B : Matrix m n α) (i : m) (j : n) : (A + B) i j = A i j + B i j

@[simp]

theorem Matrix.smul_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [SMul β α] (r : β) (A : Matrix m n α) (i : m) (j : n) : (r • A) i j = r • A i j

@[simp]

theorem Matrix.sub_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Sub α] (A B : Matrix m n α) (i : m) (j : n) : (A - B) i j = A i j - B i j

@[simp]

theorem Matrix.neg_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Neg α] (A : Matrix m n α) (i : m) (j : n) : (-A) i j = -A i j

theorem Matrix.dite_apply {m : Type u_2} {n : Type u_3} {α : Type v} (P : Prop) [Decidable P] (A : P → Matrix m n α) (B : ¬P → Matrix m n α) (i : m) (j : n) : dite P A B i j = if x : P then A x i j else B x i j

theorem Matrix.ite_apply {m : Type u_2} {n : Type u_3} {α : Type v} (P : Prop) [Decidable P] (A B : Matrix m n α) (i : m) (j : n) : (if P then A else B) i j = if P then A i j else B i j

simp-normal form pulls of to the outside.

@[simp]

theorem Matrix.of_zero {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] : of 0 = 0

@[simp]

theorem Matrix.of_add_of {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] (f g : m → n → α) : of f + of g = of (f + g)

@[simp]

theorem Matrix.of_sub_of {m : Type u_2} {n : Type u_3} {α : Type v} [Sub α] (f g : m → n → α) : of f - of g = of (f - g)

@[simp]

theorem Matrix.neg_of {m : Type u_2} {n : Type u_3} {α : Type v} [Neg α] (f : m → n → α) : -of f = of (-f)

@[simp]

theorem Matrix.smul_of {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [SMul R α] (r : R) (f : m → n → α) : r • of f = of (r • f)

@[simp]

theorem Matrix.map_zero {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Zero α] [Zero β] (f : α → β) (h : f 0 = 0) : map 0 f = 0

theorem Matrix.map_add {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Add α] [Add β] (f : α → β) (hf : ∀ (a₁ a₂ : α), f (a₁ + a₂) = f a₁ + f a₂) (M N : Matrix m n α) : (M + N).map f = M.map f + N.map f

theorem Matrix.map_sub {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Sub α] [Sub β] (f : α → β) (hf : ∀ (a₁ a₂ : α), f (a₁ - a₂) = f a₁ - f a₂) (M N : Matrix m n α) : (M - N).map f = M.map f - N.map f

theorem Matrix.map_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [SMul R α] [SMul R β] (f : α → β) (r : R) (hf : ∀ (a : α), f (r • a) = r • f a) (M : Matrix m n α) : (r • M).map f = r • M.map f

theorem Matrix.map_smul' {n : Type u_3} {α : Type v} {β : Type w} [Mul α] [Mul β] (f : α → β) (r : α) (A : Matrix n n α) (hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) : (r • A).map f = f r • A.map f

The scalar action via Mul.toSMul is transformed by the same map as the elements of the matrix, when f preserves multiplication.

theorem Matrix.map_op_smul' {n : Type u_3} {α : Type v} {β : Type w} [Mul α] [Mul β] (f : α → β) (r : α) (A : Matrix n n α) (hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) : (MulOpposite.op r • A).map f = MulOpposite.op (f r) • A.map f

The scalar action via mul.toOppositeSMul is transformed by the same map as the elements of the matrix, when f preserves multiplication.

theorem IsSMulRegular.matrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [SMul R S] {k : R} (hk : IsSMulRegular S k) : IsSMulRegular (Matrix m n S) k

theorem IsLeftRegular.matrix {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] {k : α} (hk : IsLeftRegular k) : IsSMulRegular (Matrix m n α) k

instance Matrix.subsingleton_of_empty_left {m : Type u_2} {n : Type u_3} {α : Type v} [IsEmpty m] : Subsingleton (Matrix m n α)

instance Matrix.subsingleton_of_empty_right {m : Type u_2} {n : Type u_3} {α : Type v} [IsEmpty n] : Subsingleton (Matrix m n α)

def Matrix.ofAddEquiv {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] : (m → n → α) ≃+ Matrix m n α

This is Matrix.of bundled as an additive equivalence.

Equations

• Matrix.ofAddEquiv = { toEquiv := Matrix.of, map_add' := ⋯ }

@[simp]

theorem Matrix.coe_ofAddEquiv {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] : ⇑ofAddEquiv = ⇑of

@[simp]

theorem Matrix.coe_ofAddEquiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] : ⇑ofAddEquiv.symm = ⇑of.symm

@[simp]

theorem Matrix.isAddUnit_iff {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] {A : Matrix m n α} : IsAddUnit A ↔ ∀ (i : m) (j : n), IsAddUnit (A i j)

@[simp]

theorem Matrix.transpose_transpose {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : M.transpose.transpose = M

theorem Matrix.transpose_injective {m : Type u_2} {n : Type u_3} {α : Type v} : Function.Injective transpose

@[simp]

theorem Matrix.transpose_inj {m : Type u_2} {n : Type u_3} {α : Type v} {A B : Matrix m n α} : A.transpose = B.transpose ↔ A = B

@[simp]

theorem Matrix.transpose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] : transpose 0 = 0

@[simp]

theorem Matrix.transpose_eq_zero {m : Type u_2} {n : Type u_3} {α : Type v} [Zero α] {M : Matrix m n α} : M.transpose = 0 ↔ M = 0

@[simp]

theorem Matrix.transpose_add {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] (M N : Matrix m n α) : (M + N).transpose = M.transpose + N.transpose

@[simp]

theorem Matrix.transpose_sub {m : Type u_2} {n : Type u_3} {α : Type v} [Sub α] (M N : Matrix m n α) : (M - N).transpose = M.transpose - N.transpose

@[simp]

theorem Matrix.transpose_smul {m : Type u_2} {n : Type u_3} {α : Type v} {R : Type u_10} [SMul R α] (c : R) (M : Matrix m n α) : (c • M).transpose = c • M.transpose

@[simp]

theorem Matrix.transpose_neg {m : Type u_2} {n : Type u_3} {α : Type v} [Neg α] (M : Matrix m n α) : (-M).transpose = -M.transpose

theorem Matrix.transpose_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {M : Matrix m n α} : M.transpose.map f = (M.map f).transpose

def Matrix.submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) : Matrix l o α

Given maps (r_reindex : l → m) and (c_reindex : o → n) reindexing the rows and columns of a matrix M : Matrix m n α, the matrix M.submatrix r_reindex c_reindex : Matrix l o α is defined by (M.submatrix r_reindex c_reindex) i j = M (r_reindex i) (c_reindex j) for (i,j) : l × o. Note that the total number of row and columns does not have to be preserved.

Equations

• A.submatrix r_reindex c_reindex = Matrix.of fun (i : l) (j : o) => A (r_reindex i) (c_reindex j)

@[simp]

theorem Matrix.submatrix_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) (i : l) (j : o) : A.submatrix r_reindex c_reindex i j = A (r_reindex i) (c_reindex j)

@[simp]

theorem Matrix.submatrix_id_id {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : A.submatrix id id = A

@[simp]

theorem Matrix.submatrix_submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {l₂ : Type u_10} {o₂ : Type u_11} (A : Matrix m n α) (r₁ : l → m) (c₁ : o → n) (r₂ : l₂ → l) (c₂ : o₂ → o) : (A.submatrix r₁ c₁).submatrix r₂ c₂ = A.submatrix (r₁ ∘ r₂) (c₁ ∘ c₂)

@[simp]

theorem Matrix.transpose_submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) : (A.submatrix r_reindex c_reindex).transpose = A.transpose.submatrix c_reindex r_reindex

theorem Matrix.submatrix_add {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Add α] (A B : Matrix m n α) : (A + B).submatrix = A.submatrix + B.submatrix

theorem Matrix.submatrix_neg {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Neg α] (A : Matrix m n α) : (-A).submatrix = -A.submatrix

theorem Matrix.submatrix_sub {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Sub α] (A B : Matrix m n α) : (A - B).submatrix = A.submatrix - B.submatrix

@[simp]

theorem Matrix.submatrix_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Zero α] : submatrix 0 = 0

theorem Matrix.submatrix_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {R : Type u_10} [SMul R α] (r : R) (A : Matrix m n α) : (r • A).submatrix = r • A.submatrix

theorem Matrix.submatrix_map {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} (f : α → β) (e₁ : l → m) (e₂ : o → n) (A : Matrix m n α) : (A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f

def Matrix.reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) : Matrix m n α ≃ Matrix l o α

The natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence.

Equations

• Matrix.reindex eₘ eₙ = { toFun := fun (M : Matrix m n α) => M.submatrix ⇑eₘ.symm ⇑eₙ.symm, invFun := fun (M : Matrix l o α) => M.submatrix ⇑eₘ ⇑eₙ, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Matrix.reindex_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) : (reindex eₘ eₙ) M = M.submatrix ⇑eₘ.symm ⇑eₙ.symm

theorem Matrix.reindex_refl_refl {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : (reindex (Equiv.refl m) (Equiv.refl n)) A = A

@[simp]

theorem Matrix.reindex_symm {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) : (reindex eₘ eₙ).symm = reindex eₘ.symm eₙ.symm

@[simp]

theorem Matrix.reindex_trans {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {l₂ : Type u_10} {o₂ : Type u_11} (eₘ : m ≃ l) (eₙ : n ≃ o) (eₘ₂ : l ≃ l₂) (eₙ₂ : o ≃ o₂) : (reindex eₘ eₙ).trans (reindex eₘ₂ eₙ₂) = reindex (eₘ.trans eₘ₂) (eₙ.trans eₙ₂)

theorem Matrix.transpose_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) : ((reindex eₘ eₙ) M).transpose = (reindex eₙ eₘ) M.transpose

@[reducible, inline]

abbrev Matrix.subLeft {α : Type v} {m l r : ℕ} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin l) α

The left n × l part of an n × (l+r) matrix.

Equations

• A.subLeft = A.submatrix id (Fin.castAdd r)

@[reducible, inline]

abbrev Matrix.subRight {α : Type v} {m l r : ℕ} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin r) α

The right n × r part of an n × (l+r) matrix.

Equations

• A.subRight = A.submatrix id (Fin.natAdd l)

@[reducible, inline]

abbrev Matrix.subUp {α : Type v} {d u n : ℕ} (A : Matrix (Fin (u + d)) (Fin n) α) : Matrix (Fin u) (Fin n) α

The top u × n part of a (u+d) × n matrix.

Equations

• A.subUp = A.submatrix (Fin.castAdd d) id

@[reducible, inline]

abbrev Matrix.subDown {α : Type v} {d u n : ℕ} (A : Matrix (Fin (u + d)) (Fin n) α) : Matrix (Fin d) (Fin n) α

The bottom d × n part of a (u+d) × n matrix.

Equations

• A.subDown = A.submatrix (Fin.natAdd u) id

@[reducible, inline]

abbrev Matrix.subUpRight {α : Type v} {d u l r : ℕ} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin u) (Fin r) α

The top-right u × r part of a (u+d) × (l+r) matrix.

Equations

• A.subUpRight = A.subRight.subUp

@[reducible, inline]

abbrev Matrix.subDownRight {α : Type v} {d u l r : ℕ} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin d) (Fin r) α

The bottom-right d × r part of a (u+d) × (l+r) matrix.

Equations

• A.subDownRight = A.subRight.subDown

@[reducible, inline]

abbrev Matrix.subUpLeft {α : Type v} {d u l r : ℕ} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin u) (Fin l) α

The top-left u × l part of a (u+d) × (l+r) matrix.

Equations

• A.subUpLeft = A.subLeft.subUp

@[reducible, inline]

abbrev Matrix.subDownLeft {α : Type v} {d u l r : ℕ} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin d) (Fin l) α

The bottom-left d × l part of a (u+d) × (l+r) matrix.

Equations

• A.subDownLeft = A.subLeft.subDown

def Matrix.row {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : m → n → α

For an m × n α-matrix A, A.row i is the ith row of A as a vector in n → α. A.row is defeq to A, but explicitly refers to the 'row functionofAwhile avoiding defeq abuse and noisy eta-expansions, such as in expressions likeSet.Injective A.rowandSet.range A.row. (Note 2025-04-07 : the identifier Matrix.rowused to refer to a matrix with all rows equal; this is now calledMatrix.replicateRow`)

Equations

• A.row = A

def Matrix.col {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : n → m → α

For an m × n α-matrix A, A.col j is the jth column of A as a vector in m → α. A.col is defeq to Aᵀ, but refers to the 'column function' of A while avoiding defeq abuse and noisy eta-expansions (and without the simplifier unfolding transposes) in expressions like Set.Injective A.col and Set.range A.col. (Note 2025-04-07 : the identifier Matrix.col used to refer to a matrix with all columns equal; this is now called Matrix.replicateCol)

Equations

• A.col = A.transpose

theorem Matrix.row_eq_self {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : A.row = of.symm A

theorem Matrix.col_eq_transpose {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : A.col = of.symm A.transpose

@[simp]

theorem Matrix.of_row {m : Type u_2} {n : Type u_3} {α : Type v} (f : m → n → α) : (of f).row = f

@[simp]

theorem Matrix.of_col {m : Type u_2} {n : Type u_3} {α : Type v} (f : m → n → α) : (of f).transpose.col = f

theorem Matrix.row_def {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : A.row = fun (i : m) => A i

theorem Matrix.col_def {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : A.col = fun (j : n) => A.transpose j

@[simp]

theorem Matrix.row_apply {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) (i : m) (j : n) : A.row i j = A i j

theorem Matrix.row_apply' {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) (i : m) : A.row i = A i

A partially applied version of Matrix.row_apply

@[simp]

theorem Matrix.col_apply {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) (i : n) (j : m) : A.col i j = A j i

theorem Matrix.col_apply' {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) (i : n) : A.col i = fun (j : m) => A j i

A partially applied version of Matrix.col_apply

theorem Matrix.row_submatrix {m : Type u_2} {n : Type u_3} {α : Type v} {m₀ : Type u_10} {n₀ : Type u_11} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (i : m₀) : (A.submatrix r c).row i = (A.submatrix id c).row (r i)

theorem Matrix.row_submatrix_eq_comp {m : Type u_2} {n : Type u_3} {α : Type v} {m₀ : Type u_10} {n₀ : Type u_11} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (i : m₀) : (A.submatrix r c).row i = A.row (r i) ∘ c

theorem Matrix.col_submatrix {m : Type u_2} {n : Type u_3} {α : Type v} {m₀ : Type u_10} {n₀ : Type u_11} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (j : n₀) : (A.submatrix r c).col j = (A.submatrix r id).col (c j)

theorem Matrix.col_submatrix_eq_comp {m : Type u_2} {n : Type u_3} {α : Type v} {m₀ : Type u_10} {n₀ : Type u_11} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (j : n₀) : (A.submatrix r c).col j = A.col (c j) ∘ r

theorem Matrix.row_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (A : Matrix m n α) (f : α → β) (i : m) : (A.map f).row i = f ∘ A.row i

theorem Matrix.col_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (A : Matrix m n α) (f : α → β) (j : n) : (A.map f).col j = f ∘ A.col j

@[simp]

theorem Matrix.row_transpose {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : A.transpose.row = A.col

@[simp]

theorem Matrix.col_transpose {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : A.transpose.col = A.row