HepLean Documentation

Mathlib.Data.Matrix.Defs

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 → α)

Instances For

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.

Porting note: In Lean 3, it is also safe to use pattern matching in a definition as | i j := _, which can only be unfolded when fully-applied. https://github.com/leanprover/lean4/issues/2042 means this does not (currently) work in Lean 4.

Equations

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

Instances For

@[simp]

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

Matrix.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) :

Matrix.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)

Instances For

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

Instances For

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

Instances For

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 α)

Equations

⋯ = ⋯

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

Nontrivial (Matrix m n α)

Equations

⋯ = ⋯

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 α)

Equations

⋯ = ⋯

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 α)

Equations

⋯ = ⋯

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 α)

Equations

⋯ = ⋯

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

simp-normal form pulls of to the outside.

@[simp]

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

Matrix.of 0 = 0

@[simp]

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

Matrix.of f + Matrix.of g = Matrix.of (f + g)

@[simp]

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

Matrix.of f - Matrix.of g = Matrix.of (f - g)

@[simp]

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

-Matrix.of f = Matrix.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 • Matrix.of f = Matrix.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) :

Matrix.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 α)

Equations

⋯ = ⋯

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

Subsingleton (Matrix m n α)

Equations

⋯ = ⋯

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' := ⋯ }

Instances For

@[simp]

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

⇑Matrix.ofAddEquiv = ⇑Matrix.of

@[simp]

theorem Matrix.coe_ofAddEquiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [Add α] :

⇑Matrix.ofAddEquiv.symm = ⇑Matrix.of.symm

@[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 Matrix.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 α] :

Matrix.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)

Instances For

@[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 α] :

Matrix.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 := ⋯ }

Instances For

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

(Matrix.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 α) :

(Matrix.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) :

(Matrix.reindex eₘ eₙ).symm = Matrix.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₂) :

(Matrix.reindex eₘ eₙ).trans (Matrix.reindex eₘ₂ eₙ₂) = Matrix.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 α) :

((Matrix.reindex eₘ eₙ) M).transpose = (Matrix.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)

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For