Mathlib.Data.Matrix.Defs

Matrix definition

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

Full source

/-- `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`. -/
def Matrix (m : Type u) (n : Type u') (α : Type v) : Type max u u' v :=
  m → n → α

Matrix

Informal description

The type of matrices with rows indexed by a type `m`, columns indexed by a type `n`, and entries of type `α`. A matrix is represented as a function `m → n → α`, where `A i j` denotes the entry in the `i`-th row and `j`-th column.

Matrix.ext_iff theorem

: (∀ i j, M i j = N i j) ↔ M = N

Full source

theorem ext_iff : (∀ i j, M i j = N i j) ↔ M = N :=
  ⟨fun h => funext fun i => funext <| h i, fun h => by simp [h]⟩

Matrix Equality via Entrywise Equality

Informal description

Two matrices $M$ and $N$ of type $\text{Matrix}\, m\, n\, \alpha$ are equal if and only if their corresponding entries are equal, i.e., $M_{ij} = N_{ij}$ for all row indices $i \in m$ and column indices $j \in n$.

Matrix.ext theorem

: (∀ i j, M i j = N i j) → M = N

Full source

@[ext]
theorem ext : (∀ i j, M i j = N i j) → M = N :=
  ext_iff.mp

Matrix Equality via Entrywise Equality

Informal description

Two matrices $M$ and $N$ of type $\text{Matrix}\, m\, n\, \alpha$ are equal if their corresponding entries are equal, i.e., if $M_{ij} = N_{ij}$ for all row indices $i \in m$ and column indices $j \in n$.

Matrix.of definition

: (m → n → α) ≃ Matrix m n α

Full source

/-- 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.
-/
def of : (m → n → α) ≃ Matrix m n α :=
  Equiv.refl _

Matrix construction from a function

Informal description

The function `Matrix.of` casts a function $f : m \to n \to \alpha$ into a matrix of type $\text{Matrix}\, m\, n\, \alpha$, where $m$ and $n$ are the row and column index types respectively, and $\alpha$ is the type of the entries. The equivalence ensures that the matrix representation is definitionally equal to the original function, but distinguishes the types to avoid confusion with other instances (such as elementwise multiplication in function types versus matrix multiplication).

Matrix.of_apply theorem

(f : m → n → α) (i j) : of f i j = f i j

Full source

@[simp]
theorem of_apply (f : m → n → α) (i j) : of f i j = f i j :=
  rfl

Matrix Construction Preserves Entries: $(\text{of}\, f)_{ij} = f(i,j)$

Informal description

For any function $f : m \to n \to \alpha$ and any indices $i \in m$, $j \in n$, the $(i,j)$-th entry of the matrix constructed via `Matrix.of f` equals $f(i,j)$, i.e., $(\text{Matrix.of}\, f)_{ij} = f(i,j)$.

Matrix.of_symm_apply theorem

(f : Matrix m n α) (i j) : of.symm f i j = f i j

Full source

@[simp]
theorem of_symm_apply (f : Matrix m n α) (i j) : of.symm f i j = f i j :=
  rfl

Inverse Matrix Construction Preserves Entries: $(\text{of}^{-1}\, f)(i,j) = f_{i,j}$

Informal description

For any matrix $f \in \text{Matrix}\, m\, n\, \alpha$ and indices $i \in m$, $j \in n$, the $(i,j)$-th entry of the function obtained by applying the inverse of the `Matrix.of` equivalence to $f$ equals the $(i,j)$-th entry of $f$, i.e., $(\text{Matrix.of}^{-1}\, f)(i,j) = f_{i,j}$.

Matrix.map definition

(M : Matrix m n α) (f : α → β) : Matrix m n β

Full source

/-- `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`
-/
def map (M : Matrix m n α) (f : α → β) : Matrix m n β :=
  of fun i j => f (M i j)

Matrix entry-wise map

Informal description

Given a matrix $M$ of type $\text{Matrix}\, m\, n\, \alpha$ and a function $f : \alpha \to \beta$, the matrix $\text{map}\, M\, f$ is obtained by applying $f$ to each entry of $M$. Specifically, the $(i,j)$-th entry of the resulting matrix is $f(M_{ij})$.

Matrix.map_apply theorem

{M : Matrix m n α} {f : α → β} {i : m} {j : n} : M.map f i j = f (M i j)

Full source

@[simp]
theorem map_apply {M : Matrix m n α} {f : α → β} {i : m} {j : n} : M.map f i j = f (M i j) :=
  rfl

Matrix Mapping Preserves Entry-wise Application: $(M.map\, f)_{i,j} = f(M_{i,j})$

Informal description

For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$, function $f : \alpha \to \beta$, and indices $i \in m$, $j \in n$, the $(i,j)$-th entry of the mapped matrix $M.map\, f$ is equal to $f$ applied to the $(i,j)$-th entry of $M$, i.e., $(M.map\, f)_{i,j} = f(M_{i,j})$.

Matrix.map_id theorem

(M : Matrix m n α) : M.map id = M

Full source

@[simp]
theorem map_id (M : Matrix m n α) : M.map id = M := by
  ext
  rfl

Identity Map Preserves Matrix

Informal description

For any matrix $M$ of type $\text{Matrix}\, m\, n\, \alpha$, the entry-wise application of the identity function to $M$ yields $M$ itself, i.e., $\text{map}\, M\, \text{id} = M$.

Matrix.map_id' theorem

(M : Matrix m n α) : M.map (·) = M

Full source

@[simp]
theorem map_id' (M : Matrix m n α) : M.map (·) = M := map_id M

Identity Map Preserves Matrix (Lambda Notation Version)

Informal description

For any matrix $M$ of type $\text{Matrix}\, m\, n\, \alpha$, the entry-wise application of the identity function (written as `(·)`) to $M$ yields $M$ itself, i.e., $M.map\, (·) = M$.

Matrix.map_map theorem

{M : Matrix m n α} {β γ : Type*} {f : α → β} {g : β → γ} : (M.map f).map g = M.map (g ∘ f)

Full source

@[simp]
theorem map_map {M : Matrix m n α} {β γ : Type*} {f : α → β} {g : β → γ} :
    (M.map f).map g = M.map (g ∘ f) := by
  ext
  rfl

Composition of Matrix Entry-wise Maps: $(M.map\, f).map\, g = M.map\, (g \circ f)$

Informal description

For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$ and functions $f : \alpha \to \beta$ and $g : \beta \to \gamma$, the composition of entry-wise mappings satisfies $(M.map\, f).map\, g = M.map\, (g \circ f)$. In other words, mapping $f$ followed by $g$ is equivalent to mapping the composition $g \circ f$ directly.

Matrix.map_injective theorem

{f : α → β} (hf : Function.Injective f) : Function.Injective fun M : Matrix m n α => M.map f

Full source

theorem map_injective {f : α → β} (hf : Function.Injective f) :
    Function.Injective fun M : Matrix m n α => M.map f := fun _ _ h =>
  ext fun i j => hf <| ext_iff.mpr h i j

Injectivity of Matrix Entry-wise Map under Injective Function

Informal description

Let $f : \alpha \to \beta$ be an injective function. Then the entry-wise matrix map operation $M \mapsto M.map\, f$ is also injective. That is, for any two matrices $M, N \in \text{Matrix}\, m\, n\, \alpha$, if $M.map\, f = N.map\, f$, then $M = N$.

Matrix.transpose definition

(M : Matrix m n α) : Matrix n m α

Full source

/-- The transpose of a matrix. -/
def transpose (M : Matrix m n α) : Matrix n m α :=
  of fun x y => M y x

Matrix transpose

Informal description

The transpose of a matrix $M \in \text{Matrix}\, m\, n\, \alpha$ is the matrix $M^\top \in \text{Matrix}\, n\, m\, \alpha$ obtained by swapping rows and columns, defined by $(M^\top)_{i,j} = M_{j,i}$ for all $i \in n$ and $j \in m$.

Matrix.transpose_apply theorem

(M : Matrix m n α) (i j) : transpose M i j = M j i

Full source

@[simp]
theorem transpose_apply (M : Matrix m n α) (i j) : transpose M i j = M j i :=
  rfl

Transpose Entry Formula: $(M^\top)_{i,j} = M_{j,i}$

Informal description

For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$ and indices $i \in n$, $j \in m$, the $(i,j)$-th entry of the transpose matrix $M^\top$ is equal to the $(j,i)$-th entry of $M$, i.e., $(M^\top)_{i,j} = M_{j,i}$.

Matrix.term_ᵀ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
scoped postfix:1024 "ᵀ" => Matrix.transpose

Matrix transpose notation

Informal description

The notation `Aᵀ` denotes the transpose of a matrix `A`, which swaps its rows and columns. For any matrix `A : Matrix m n α`, the transpose `Aᵀ` is a matrix of type `Matrix n m α` where the entry at position `(i,j)` is equal to `A j i`.

Matrix.inhabited instance

[Inhabited α] : Inhabited (Matrix m n α)

Full source

instance inhabited [Inhabited α] : Inhabited (Matrix m n α) :=
  inferInstanceAs <| Inhabited <| m → n → α

Inhabited Matrices from Inhabited Entries

Informal description

For any type $\alpha$ with a distinguished element, the type of matrices $\text{Matrix}\, m\, n\, \alpha$ also has a distinguished element, where each entry of the matrix is the distinguished element of $\alpha$.

Matrix.add instance

[Add α] : Add (Matrix m n α)

Full source

instance add [Add α] : Add (Matrix m n α) :=
  Pi.instAdd

Componentwise Addition of Matrices

Informal description

For any type $α$ equipped with an addition operation, the type of matrices $\mathrm{Matrix}\, m\, n\, α$ is also equipped with an addition operation defined componentwise. That is, for two matrices $A$ and $B$ in $\mathrm{Matrix}\, m\, n\, α$, the sum $A + B$ is the matrix whose $(i,j)$-th entry is $A_{i,j} + B_{i,j}$ for all $i \in m$ and $j \in n$.

Matrix.addSemigroup instance

[AddSemigroup α] : AddSemigroup (Matrix m n α)

Full source

instance addSemigroup [AddSemigroup α] : AddSemigroup (Matrix m n α) :=
  Pi.addSemigroup

Matrix Addition Forms a Semigroup

Informal description

For any type `α` with an add-semigroup structure, the type of matrices `Matrix m n α` inherits an add-semigroup structure where matrix addition is defined entrywise.

Matrix.addCommSemigroup instance

[AddCommSemigroup α] : AddCommSemigroup (Matrix m n α)

Full source

instance addCommSemigroup [AddCommSemigroup α] : AddCommSemigroup (Matrix m n α) :=
  Pi.addCommSemigroup

Commutative Additive Semigroup Structure on Matrices

Informal description

For any type $\alpha$ with a commutative add-semigroup structure, the type of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ inherits a commutative add-semigroup structure where matrix addition is defined entrywise and is commutative.

Matrix.zero instance

[Zero α] : Zero (Matrix m n α)

Full source

instance zero [Zero α] : Zero (Matrix m n α) :=
  Pi.instZero

Zero Matrix

Informal description

For any type $α$ with a zero element, the type of matrices $\mathrm{Matrix}\, m\, n\, α$ has a zero element given by the matrix with all entries equal to zero.

Matrix.addZeroClass instance

[AddZeroClass α] : AddZeroClass (Matrix m n α)

Full source

instance addZeroClass [AddZeroClass α] : AddZeroClass (Matrix m n α) :=
  Pi.addZeroClass

Entrywise Additive Zero Class Structure on Matrices

Informal description

For any type `α` with an additive zero class structure (i.e., an addition operation with a zero element satisfying the additive identity properties), the type of matrices `Matrix m n α` inherits an additive zero class structure where addition and zero are defined entrywise.

Matrix.addMonoid instance

[AddMonoid α] : AddMonoid (Matrix m n α)

Full source

instance addMonoid [AddMonoid α] : AddMonoid (Matrix m n α) :=
  Pi.addMonoid

Entrywise Additive Monoid Structure on Matrices

Informal description

For any type $\alpha$ with an additive monoid structure, the type of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ inherits an additive monoid structure where addition and zero are defined entrywise.

Matrix.addCommMonoid instance

[AddCommMonoid α] : AddCommMonoid (Matrix m n α)

Full source

instance addCommMonoid [AddCommMonoid α] : AddCommMonoid (Matrix m n α) :=
  Pi.addCommMonoid

Entrywise Additive Commutative Monoid Structure on Matrices

Informal description

For any type $\alpha$ with an additive commutative monoid structure, the type of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ inherits an additive commutative monoid structure where addition and zero are defined entrywise.

Matrix.neg instance

[Neg α] : Neg (Matrix m n α)

Full source

instance neg [Neg α] : Neg (Matrix m n α) :=
  Pi.instNeg

Entrywise Negation of Matrices

Informal description

For any type `α` equipped with a negation operation and any types `m`, `n` indexing rows and columns, the space of matrices `Matrix m n α` inherits a negation operation defined entrywise.

Matrix.sub instance

[Sub α] : Sub (Matrix m n α)

Full source

instance sub [Sub α] : Sub (Matrix m n α) :=
  Pi.instSub

Componentwise Subtraction of Matrices

Informal description

For any type $m$ of rows, type $n$ of columns, and type $\alpha$ with a subtraction operation, the type of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ inherits a subtraction operation defined componentwise.

Matrix.addGroup instance

[AddGroup α] : AddGroup (Matrix m n α)

Full source

instance addGroup [AddGroup α] : AddGroup (Matrix m n α) :=
  Pi.addGroup

Additive Group Structure on Matrices

Informal description

For any additive group $\alpha$ and any types $m$, $n$ indexing rows and columns, the space of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ forms an additive group under entrywise addition.

Matrix.addCommGroup instance

[AddCommGroup α] : AddCommGroup (Matrix m n α)

Full source

instance addCommGroup [AddCommGroup α] : AddCommGroup (Matrix m n α) :=
  Pi.addCommGroup

Commutative Additive Group Structure on Matrices

Informal description

For any commutative additive group $\alpha$ and any types $m$, $n$ indexing rows and columns, the space of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ forms a commutative additive group under entrywise addition.

Matrix.unique instance

[Unique α] : Unique (Matrix m n α)

Full source

instance unique [Unique α] : Unique (Matrix m n α) :=
  Pi.unique

Uniqueness of Matrices over a Unique Type

Informal description

For any types $m$ and $n$ indexing rows and columns, and a type $\alpha$ with exactly one element, the space of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ has exactly one element (the constant matrix with all entries equal to the unique element of $\alpha$).

Matrix.subsingleton instance

[Subsingleton α] : Subsingleton (Matrix m n α)

Full source

instance subsingleton [Subsingleton α] : Subsingleton (Matrix m n α) :=
  inferInstanceAs <| Subsingleton <| m → n → α

Subsingleton Matrices over Subsingleton Types

Informal description

For any types $m$ and $n$ and a subsingleton type $\alpha$ (i.e., a type with at most one element), the type of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ is also a subsingleton.

Matrix.nonempty instance

[Nonempty m] [Nonempty n] [Nontrivial α] : Nontrivial (Matrix m n α)

Full source

instance nonempty [Nonempty m] [Nonempty n] [Nontrivial α] : Nontrivial (Matrix m n α) :=
  Function.nontrivial

Nontriviality of Matrix Spaces over Nontrivial Entries

Informal description

For any nonempty types $m$ and $n$ indexing rows and columns, and a nontrivial type $\alpha$ of entries, the space of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ is also nontrivial.

Matrix.smul instance

[SMul R α] : SMul R (Matrix m n α)

Full source

instance smul [SMul R α] : SMul R (Matrix m n α) :=
  Pi.instSMul

Scalar Multiplication on Matrices

Informal description

For any type $R$ with a scalar multiplication operation on a type $\alpha$, the space of matrices with entries in $\alpha$ inherits a scalar multiplication operation from $\alpha$, where $(c \cdot A)_{ij} = c \cdot A_{ij}$ for any $c \in R$, matrix $A \in \text{Matrix}\, m\, n\, \alpha$, and indices $i \in m$, $j \in n$.

Matrix.smulCommClass instance

[SMul R α] [SMul S α] [SMulCommClass R S α] : SMulCommClass R S (Matrix m n α)

Full source

instance smulCommClass [SMul R α] [SMul S α] [SMulCommClass R S α] :
    SMulCommClass R S (Matrix m n α) :=
  Pi.smulCommClass

Commutativity of Scalar Multiplication on Matrices

Informal description

For any types $R$ and $S$ with scalar multiplication operations on a type $\alpha$, if the scalar multiplications of $R$ and $S$ on $\alpha$ commute (i.e., $r \cdot (s \cdot a) = s \cdot (r \cdot a)$ for all $r \in R$, $s \in S$, $a \in \alpha$), then the scalar multiplications of $R$ and $S$ on the space of matrices $\text{Matrix}\, m\, n\, \alpha$ also commute.

Matrix.isScalarTower instance

[SMul R S] [SMul R α] [SMul S α] [IsScalarTower R S α] : IsScalarTower R S (Matrix m n α)

Full source

instance isScalarTower [SMul R S] [SMul R α] [SMul S α] [IsScalarTower R S α] :
    IsScalarTower R S (Matrix m n α) :=
  Pi.isScalarTower

Scalar Tower Condition for Matrix Scalar Multiplication

Informal description

For any types $R$ and $S$ with scalar multiplication operations on a type $\alpha$, if the scalar multiplications satisfy the tower condition (i.e., $r \cdot (s \cdot a) = (r \cdot s) \cdot a$ for all $r \in R$, $s \in S$, $a \in \alpha$), then the induced scalar multiplications on the space of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ also satisfy the tower condition.

Matrix.isCentralScalar instance

[SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] : IsCentralScalar R (Matrix m n α)

Full source

instance isCentralScalar [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] :
    IsCentralScalar R (Matrix m n α) :=
  Pi.isCentralScalar

Central Scalar Multiplication on Matrices

Informal description

For any type $R$ with scalar multiplication operations on a type $\alpha$ and its multiplicative opposite $R^\text{op}$, if the scalar multiplication by $R$ on $\alpha$ is central (i.e., $r \cdot a = a \cdot r$ for all $r \in R$ and $a \in \alpha$), then the induced scalar multiplication by $R$ on the space of matrices $\text{Matrix}\, m\, n\, \alpha$ is also central.

Matrix.mulAction instance

[Monoid R] [MulAction R α] : MulAction R (Matrix m n α)

Full source

instance mulAction [Monoid R] [MulAction R α] : MulAction R (Matrix m n α) :=
  Pi.mulAction _

Pointwise Multiplicative Action on Matrices

Informal description

For any monoid $R$ and type $\alpha$ equipped with a multiplicative action of $R$, the type of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ inherits a pointwise multiplicative action structure from $R$, where the action is defined by $(r \cdot A)_{ij} = r \cdot (A_{ij})$ for each entry $A_{ij}$ of the matrix $A$.

Matrix.distribMulAction instance

[Monoid R] [AddMonoid α] [DistribMulAction R α] : DistribMulAction R (Matrix m n α)

Full source

instance distribMulAction [Monoid R] [AddMonoid α] [DistribMulAction R α] :
    DistribMulAction R (Matrix m n α) :=
  Pi.distribMulAction _

Distributive Multiplicative Action on Matrices

Informal description

For any monoid $R$ and any additive monoid $\alpha$ equipped with a distributive multiplicative action of $R$, the space of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ inherits a distributive multiplicative action structure from $R$, where the action is defined entrywise as $(r \cdot A)_{ij} = r \cdot (A_{ij})$ for each entry $A_{ij}$ of the matrix $A$.

Matrix.module instance

[Semiring R] [AddCommMonoid α] [Module R α] : Module R (Matrix m n α)

Full source

instance module [Semiring R] [AddCommMonoid α] [Module R α] : Module R (Matrix m n α) :=
  Pi.module _ _ _

Module Structure on Matrices with Entrywise Scalar Multiplication

Informal description

For any semiring $R$ and any additive commutative monoid $\alpha$ equipped with a module structure over $R$, the space of matrices $\mathrm{Matrix}\, m\, n\, \alpha$ inherits a module structure over $R$, where the scalar multiplication is defined entrywise as $(r \cdot A)_{ij} = r \cdot (A_{ij})$ for each entry $A_{ij}$ of the matrix $A$.

Matrix.zero_apply theorem

[Zero α] (i : m) (j : n) : (0 : Matrix m n α) i j = 0

Full source

@[simp]
theorem zero_apply [Zero α] (i : m) (j : n) : (0 : Matrix m n α) i j = 0 := rfl

Zero Matrix Entry Property: $0_{i,j} = 0$

Informal description

For any type $\alpha$ with a zero element, and for any indices $i \in m$ and $j \in n$, the $(i,j)$-th entry of the zero matrix in $\mathrm{Matrix}\,m\,n\,\alpha$ is equal to zero, i.e., $0_{i,j} = 0$.

Matrix.add_apply theorem

[Add α] (A B : Matrix m n α) (i : m) (j : n) : (A + B) i j = (A i j) + (B i j)

Full source

@[simp]
theorem add_apply [Add α] (A B : Matrix m n α) (i : m) (j : n) :
    (A + B) i j = (A i j) + (B i j) := rfl

Entrywise Addition of Matrices: $(A + B)_{i,j} = A_{i,j} + B_{i,j}$

Informal description

For any type $\alpha$ equipped with an addition operation, and for any two matrices $A, B \in \mathrm{Matrix}\,m\,n\,\alpha$, the $(i,j)$-th entry of the sum $A + B$ is equal to the sum of the corresponding entries $A_{i,j} + B_{i,j}$ for all $i \in m$ and $j \in n$.

Matrix.smul_apply theorem

[SMul β α] (r : β) (A : Matrix m n α) (i : m) (j : n) : (r • A) i j = r • (A i j)

Full source

@[simp]
theorem smul_apply [SMul β α] (r : β) (A : Matrix m n α) (i : m) (j : n) :
    (r • A) i j = r • (A i j) := rfl

Scalar Multiplication Acts Entrywise on Matrices

Informal description

For any scalar $r$ in a type $\beta$ with a scalar multiplication operation on a type $\alpha$, and for any matrix $A \in \text{Matrix}\,m\,n\,\alpha$, the $(i,j)$-th entry of the scalar multiple $r \cdot A$ is equal to the scalar multiple $r \cdot A_{i,j}$ for any indices $i \in m$ and $j \in n$.

Matrix.sub_apply theorem

[Sub α] (A B : Matrix m n α) (i : m) (j : n) : (A - B) i j = (A i j) - (B i j)

Full source

@[simp]
theorem sub_apply [Sub α] (A B : Matrix m n α) (i : m) (j : n) :
    (A - B) i j = (A i j) - (B i j) := rfl

Matrix Subtraction Acts Entrywise: $(A - B)_{i,j} = A_{i,j} - B_{i,j}$

Informal description

For any two matrices $A$ and $B$ of type $\mathrm{Matrix}\, m\, n\, \alpha$ where $\alpha$ has a subtraction operation, and for any row index $i \in m$ and column index $j \in n$, the $(i,j)$-th entry of the matrix difference $A - B$ is equal to the difference of the corresponding entries $A_{i,j} - B_{i,j}$.

Matrix.neg_apply theorem

[Neg α] (A : Matrix m n α) (i : m) (j : n) : (-A) i j = -(A i j)

Full source

@[simp]
theorem neg_apply [Neg α] (A : Matrix m n α) (i : m) (j : n) :
    (-A) i j = -(A i j) := rfl

Entrywise Negation of Matrix Elements

Informal description

For any matrix $A \in \text{Matrix}\,m\,n\,\alpha$ where $\alpha$ has a negation operation, and for any indices $i \in m$ and $j \in n$, the $(i,j)$-th entry of the negated matrix $-A$ is equal to the negation of the $(i,j)$-th entry of $A$, i.e., $(-A)_{i,j} = -A_{i,j}$.

Matrix.dite_apply theorem

 (P : Prop) [Decidable P] (A : P → Matrix m n α) (B : ¬P → Matrix m n α) (i : m) (j : n) :
  dite P A B i j = dite P (A · i j) (B · i j)

Full source

protected theorem dite_apply (P : Prop) [Decidable P]
    (A : P → Matrix m n α) (B : ¬P → Matrix m n α) (i : m) (j : n) :
    dite P A B i j = dite P (A · i j) (B · i j) := by
  rw [dite_apply, dite_apply]

Entrywise Dependent If-Then-Else for Matrices

Informal description

For any proposition $P$ with a decidability instance, and for any matrix-valued functions $A : P \to \text{Matrix}\,m\,n\,\alpha$ and $B : \neg P \to \text{Matrix}\,m\,n\,\alpha$, the $(i,j)$-th entry of the dependent if-then-else matrix $\text{dite}(P, A, B)$ is equal to $\text{dite}(P, A(\cdot)_{i,j}, B(\cdot)_{i,j})$. In other words, the $(i,j)$-th entry of a matrix constructed via dependent if-then-else is obtained by applying dependent if-then-else to the $(i,j)$-th entries of the potential matrices.

Matrix.ite_apply theorem

 (P : Prop) [Decidable P] (A : Matrix m n α) (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

Full source

protected theorem ite_apply (P : Prop) [Decidable P]
    (A : Matrix m n α) (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 :=
  Matrix.dite_apply _ _ _ _ _

Entrywise If-Then-Else for Matrix Elements

Informal description

For any proposition $P$ with a decidability instance, any two matrices $A, B \in \text{Matrix}\,m\,n\,\alpha$, and any indices $i \in m$ and $j \in n$, the $(i,j)$-th entry of the matrix $\text{if } P \text{ then } A \text{ else } B$ is equal to $\text{if } P \text{ then } A_{i,j} \text{ else } B_{i,j}$.

Matrix.of_zero theorem

[Zero α] : of (0 : m → n → α) = 0

Full source

@[simp]
theorem of_zero [Zero α] : of (0 : m → n → α) = 0 :=
  rfl

Zero Matrix Construction via Zero Function

Informal description

For any type $\alpha$ with a zero element, the matrix constructed from the zero function (which maps all indices to $0$) is equal to the zero matrix in $\text{Matrix}\, m\, n\, \alpha$. That is, $\text{of}(0) = 0$.

Matrix.of_add_of theorem

[Add α] (f g : m → n → α) : of f + of g = of (f + g)

Full source

@[simp]
theorem of_add_of [Add α] (f g : m → n → α) : of f + of g = of (f + g) :=
  rfl

Matrix Construction Preserves Addition: $\text{of}(f) + \text{of}(g) = \text{of}(f + g)$

Informal description

For any type $\alpha$ equipped with an addition operation, and for any functions $f, g : m \to n \to \alpha$, the sum of the matrices constructed from $f$ and $g$ via `Matrix.of` is equal to the matrix constructed from the pointwise sum $f + g$. In other words, $\text{of}(f) + \text{of}(g) = \text{of}(f + g)$.

Matrix.of_sub_of theorem

[Sub α] (f g : m → n → α) : of f - of g = of (f - g)

Full source

@[simp]
theorem of_sub_of [Sub α] (f g : m → n → α) : of f - of g = of (f - g) :=
  rfl

Matrix subtraction via pointwise subtraction of functions

Informal description

For any type $\alpha$ with a subtraction operation and any types $m$, $n$ indexing rows and columns, the subtraction of two matrices constructed from functions $f, g : m \to n \to \alpha$ via `Matrix.of` is equal to the matrix constructed from the pointwise subtraction of $f$ and $g$. That is, \[ \text{of}(f) - \text{of}(g) = \text{of}(f - g). \]

Matrix.neg_of theorem

[Neg α] (f : m → n → α) : -of f = of (-f)

Full source

@[simp]
theorem neg_of [Neg α] (f : m → n → α) : -of f = of (-f) :=
  rfl

Negation of Matrix Construction Equals Construction of Negated Function

Informal description

For any types $m$ and $n$ indexing rows and columns, and any type $\alpha$ equipped with a negation operation, the negation of a matrix constructed from a function $f : m \to n \to \alpha$ via `Matrix.of` is equal to the matrix constructed from the entrywise negation of $f$. That is, $-(\text{of}\, f) = \text{of}\, (-f)$.

Matrix.smul_of theorem

[SMul R α] (r : R) (f : m → n → α) : r • of f = of (r • f)

Full source

@[simp]
theorem smul_of [SMul R α] (r : R) (f : m → n → α) : r • of f = of (r • f) :=
  rfl

Scalar Multiplication Commutes with Matrix Construction: $r \cdot \text{of}(f) = \text{of}(r \cdot f)$

Informal description

For any scalar $r$ in a type $R$ with a scalar multiplication operation on a type $\alpha$, and any function $f : m \to n \to \alpha$, the scalar multiplication of $r$ with the matrix constructed from $f$ is equal to the matrix constructed from the scalar multiplication of $r$ with $f$. In other words, $r \cdot \text{of}(f) = \text{of}(r \cdot f)$, where $\text{of}$ is the matrix construction function.

Matrix.map_zero theorem

[Zero α] [Zero β] (f : α → β) (h : f 0 = 0) : (0 : Matrix m n α).map f = 0

Full source

@[simp]
protected theorem map_zero [Zero α] [Zero β] (f : α → β) (h : f 0 = 0) :
    (0 : Matrix m n α).map f = 0 := by
  ext
  simp [h]

Zero Matrix Preservation under Zero-Preserving Map

Informal description

Let $\alpha$ and $\beta$ be types with zero elements, and let $f : \alpha \to \beta$ be a function such that $f(0) = 0$. Then the entrywise application of $f$ to the zero matrix of type $\mathrm{Matrix}\, m\, n\, \alpha$ yields the zero matrix of type $\mathrm{Matrix}\, m\, n\, \beta$, i.e., $0.\mathrm{map}\, f = 0$.

Matrix.map_add theorem

 [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

Full source

protected theorem map_add [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 :=
  ext fun _ _ => hf _ _

Additivity of Matrix Map Under Addition-Preserving Functions

Informal description

Let $\alpha$ and $\beta$ be types equipped with addition operations, and let $f : \alpha \to \beta$ be a function that preserves addition (i.e., $f(a_1 + a_2) = f(a_1) + f(a_2)$ for all $a_1, a_2 \in \alpha$). Then for any two matrices $M, N \in \mathrm{Matrix}\, m\, n\, \alpha$, the entry-wise application of $f$ to the sum $M + N$ is equal to the sum of the entry-wise applications of $f$ to $M$ and $N$ individually. That is, $$(M + N).\mathrm{map}\, f = M.\mathrm{map}\, f + N.\mathrm{map}\, f.$$

Matrix.map_sub theorem

 [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

Full source

protected theorem map_sub [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 :=
  ext fun _ _ => hf _ _

Matrix Subtraction Preserved Under Entry-wise Map

Informal description

Let $\alpha$ and $\beta$ be types equipped with subtraction operations, and let $f : \alpha \to \beta$ be a function that preserves subtraction, i.e., $f(a_1 - a_2) = f(a_1) - f(a_2)$ for all $a_1, a_2 \in \alpha$. Then for any two matrices $M, N : \mathrm{Matrix}\, m\, n\, \alpha$, the entry-wise application of $f$ to the matrix difference $M - N$ equals the difference of the entry-wise applications of $f$ to $M$ and $N$: \[ (M - N).\mathrm{map}\, f = M.\mathrm{map}\, f - N.\mathrm{map}\, f. \]

Matrix.map_smul theorem

 [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

Full source

protected theorem map_smul [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 :=
  ext fun _ _ => hf _

Scalar Multiplication Commutes with Matrix Mapping under Linear Function

Informal description

Let $R$, $\alpha$, and $\beta$ be types equipped with scalar multiplication operations, and let $f : \alpha \to \beta$ be a function such that $f(r \cdot a) = r \cdot f(a)$ for all $r \in R$ and $a \in \alpha$. For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$ and scalar $r \in R$, the entry-wise application of $f$ to the scalar multiple $r \cdot M$ is equal to the scalar multiple $r \cdot f(M)$, where $f(M)$ denotes the matrix obtained by applying $f$ to each entry of $M$. In other words, $(r \cdot M).map\, f = r \cdot (M.map\, f)$.

Matrix.map_smul' theorem

 [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

Full source

/-- The scalar action via `Mul.toSMul` is transformed by the same map as the elements
of the matrix, when `f` preserves multiplication. -/
theorem map_smul' [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 :=
  ext fun _ _ => hf _ _

Scalar Multiplication Commutes with Matrix Mapping under Multiplicative Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplication operations, and let $f : \alpha \to \beta$ be a multiplicative homomorphism, i.e., $f(a_1 a_2) = f(a_1) f(a_2)$ for all $a_1, a_2 \in \alpha$. For any scalar $r \in \alpha$ and square matrix $A \in \text{Matrix}\, n\, n\, \alpha$, the entry-wise application of $f$ to the scalar multiple $r \cdot A$ equals the scalar multiple $f(r) \cdot f(A)$, where $f(A)$ denotes the matrix obtained by applying $f$ to each entry of $A$. In other words: \[ (r \cdot A).\text{map}\, f = f(r) \cdot (A.\text{map}\, f). \]

Matrix.map_op_smul' theorem

 [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

Full source

/-- The scalar action via `mul.toOppositeSMul` is transformed by the same map as the
elements of the matrix, when `f` preserves multiplication. -/
theorem map_op_smul' [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 :=
  ext fun _ _ => hf _ _

Matrix Mapping Commutes with Opposite Scalar Multiplication under Multiplicative Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types with multiplication operations, and let $f : \alpha \to \beta$ be a multiplicative homomorphism (i.e., $f(a_1 * a_2) = f(a_1) * f(a_2)$ for all $a_1, a_2 \in \alpha$). For any scalar $r \in \alpha$ and matrix $A \in \text{Matrix}\, n\, n\, \alpha$, the entry-wise application of $f$ to the matrix obtained by scalar multiplication with the opposite of $r$ (i.e., $\text{op}(r) \cdot A$) is equal to the matrix obtained by scalar multiplication with the opposite of $f(r)$ applied to the matrix $f(A)$. In other words, $$f(\text{op}(r) \cdot A) = \text{op}(f(r)) \cdot f(A)$$ where $f(A)$ denotes the matrix obtained by applying $f$ to each entry of $A$.

IsSMulRegular.matrix theorem

[SMul R S] {k : R} (hk : IsSMulRegular S k) : IsSMulRegular (Matrix m n S) k

Full source

theorem _root_.IsSMulRegular.matrix [SMul R S] {k : R} (hk : IsSMulRegular S k) :
    IsSMulRegular (Matrix m n S) k :=
  IsSMulRegular.pi fun _ => IsSMulRegular.pi fun _ => hk

Regularity of Scalar Multiplication on Matrices

Informal description

Let $R$ and $S$ be types with a scalar multiplication operation, and let $k \in R$. If $k$ is a regular scalar for $S$ (i.e., the map $x \mapsto k \cdot x$ is injective on $S$), then $k$ is also a regular scalar for the space of matrices $\text{Matrix}\, m\, n\, S$.

IsLeftRegular.matrix theorem

[Mul α] {k : α} (hk : IsLeftRegular k) : IsSMulRegular (Matrix m n α) k

Full source

theorem _root_.IsLeftRegular.matrix [Mul α] {k : α} (hk : IsLeftRegular k) :
    IsSMulRegular (Matrix m n α) k :=
  hk.isSMulRegular.matrix

Left Regular Element Induces Regular Scalar Multiplication on Matrices

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $k \in \alpha$ be left regular (i.e., the map $x \mapsto k \cdot x$ is injective on $\alpha$). Then $k$ is also a regular scalar for the space of matrices $\text{Matrix}\, m\, n\, \alpha$, meaning the map $A \mapsto k \cdot A$ is injective on $\text{Matrix}\, m\, n\, \alpha$.

Matrix.subsingleton_of_empty_left instance

[IsEmpty m] : Subsingleton (Matrix m n α)

Full source

instance subsingleton_of_empty_left [IsEmpty m] : Subsingleton (Matrix m n α) :=
  ⟨fun M N => by
    ext i
    exact isEmptyElim i⟩

Matrices with Empty Row Index Type are Subsingletons

Informal description

For any empty row index type $m$, column index type $n$, and entry type $\alpha$, the type of matrices $\text{Matrix}\, m\, n\, \alpha$ is a subsingleton (i.e., has at most one element).

Matrix.subsingleton_of_empty_right instance

[IsEmpty n] : Subsingleton (Matrix m n α)

Full source

instance subsingleton_of_empty_right [IsEmpty n] : Subsingleton (Matrix m n α) :=
  ⟨fun M N => by
    ext i j
    exact isEmptyElim j⟩

Subsingleton Property of Matrices with Empty Column Index Type

Informal description

For any type $m$ and any empty type $n$, the type of matrices $\text{Matrix}\, m\, n\, \alpha$ is a subsingleton (i.e., has at most one element).

Matrix.ofAddEquiv definition

[Add α] : (m → n → α) ≃+ Matrix m n α

Full source

/-- This is `Matrix.of` bundled as an additive equivalence. -/
def ofAddEquiv [Add α] : (m → n → α) ≃+ Matrix m n α where
  __ := of
  map_add' _ _ := rfl

Additive equivalence between functions and matrices

Informal description

The additive equivalence `Matrix.ofAddEquiv` between the type of functions `m → n → α` and the type of matrices `Matrix m n α`, which preserves addition. Specifically, for any two functions `f, g : m → n → α`, the equivalence satisfies `ofAddEquiv (f + g) = ofAddEquiv f + ofAddEquiv g`.

Matrix.coe_ofAddEquiv theorem

[Add α] : ⇑(ofAddEquiv : (m → n → α) ≃+ Matrix m n α) = of

Full source

@[simp] lemma coe_ofAddEquiv [Add α] :
    ⇑(ofAddEquiv : (m → n → α) ≃+ Matrix m n α) = of := rfl

Coercion of Matrix Additive Equivalence Equals Construction Function

Informal description

For any type $\alpha$ equipped with an addition operation, the underlying function of the additive equivalence `ofAddEquiv` from functions $m \to n \to \alpha$ to matrices $\text{Matrix}\, m\, n\, \alpha$ is equal to the matrix construction function `of`. That is, the coercion of `ofAddEquiv` coincides with `of`.

Matrix.coe_ofAddEquiv_symm theorem

[Add α] : ⇑(ofAddEquiv.symm : Matrix m n α ≃+ (m → n → α)) = of.symm

Full source

@[simp] lemma coe_ofAddEquiv_symm [Add α] :
    ⇑(ofAddEquiv.symm : MatrixMatrix m n α ≃+ (m → n → α)) = of.symm := rfl

Coercion of Inverse Matrix Additive Equivalence Equals Inverse Construction Function

Informal description

For any type $\alpha$ equipped with an addition operation, the underlying function of the inverse of the additive equivalence `ofAddEquiv` from matrices $\mathrm{Matrix}\, m\, n\, \alpha$ to functions $m \to n \to \alpha$ is equal to the inverse of the matrix construction function `of`. That is, the coercion of `ofAddEquiv.symm` coincides with `of.symm`.

Matrix.isAddUnit_iff theorem

[AddMonoid α] {A : Matrix m n α} : IsAddUnit A ↔ ∀ i j, IsAddUnit (A i j)

Full source

@[simp] lemma isAddUnit_iff [AddMonoid α] {A : Matrix m n α} :
    IsAddUnitIsAddUnit A ↔ ∀ i j, IsAddUnit (A i j) := by
  simp_rw [isAddUnit_iff_exists, Classical.skolem, forall_and,
    ← Matrix.ext_iff, add_apply, zero_apply]
  rfl

Matrix is Additive Unit if and only if All Entries Are Additive Units

Informal description

Let $\alpha$ be an additive monoid and $A$ be an $m \times n$ matrix with entries in $\alpha$. Then $A$ is an additive unit (i.e., has an additive inverse) if and only if every entry $A_{i,j}$ is an additive unit in $\alpha$.

Matrix.transpose_transpose theorem

(M : Matrix m n α) : Mᵀᵀ = M

Full source

@[simp]
theorem transpose_transpose (M : Matrix m n α) : MᵀMᵀᵀ = M := by
  ext
  rfl

Double Transpose Identity: $(M^\top)^\top = M$

Informal description

For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$, the transpose of the transpose of $M$ equals $M$ itself, i.e., $(M^\top)^\top = M$.

Matrix.transpose_injective theorem

: Function.Injective (transpose : Matrix m n α → Matrix n m α)

Full source

theorem transpose_injective : Function.Injective (transpose : Matrix m n α → Matrix n m α) :=
  fun _ _ h => ext fun i j => ext_iff.2 h j i

Injectivity of Matrix Transpose

Informal description

The transpose operation on matrices, which maps a matrix $A \in \text{Matrix}\, m\, n\, \alpha$ to its transpose $A^\top \in \text{Matrix}\, n\, m\, \alpha$, is an injective function. That is, for any two matrices $A$ and $B$ of the same size, if $A^\top = B^\top$, then $A = B$.

Matrix.transpose_inj theorem

{A B : Matrix m n α} : Aᵀ = Bᵀ ↔ A = B

Full source

@[simp] theorem transpose_inj {A B : Matrix m n α} : AᵀAᵀ = Bᵀ ↔ A = B := transpose_injective.eq_iff

Transpose Equality Criterion: $A^\top = B^\top \leftrightarrow A = B$

Informal description

For any two matrices $A$ and $B$ of type $\text{Matrix}\, m\, n\, \alpha$, the transpose of $A$ equals the transpose of $B$ if and only if $A$ equals $B$. In other words, $A^\top = B^\top \leftrightarrow A = B$.

Matrix.transpose_zero theorem

[Zero α] : (0 : Matrix m n α)ᵀ = 0

Full source

@[simp]
theorem transpose_zero [Zero α] : (0 : Matrix m n α)ᵀ = 0 := rfl

Transpose of Zero Matrix Equals Zero Matrix

Informal description

For any type $\alpha$ with a zero element, the transpose of the zero matrix in $\text{Matrix}\, m\, n\, \alpha$ is equal to the zero matrix in $\text{Matrix}\, n\, m\, \alpha$, i.e., $0^\top = 0$.

Matrix.transpose_eq_zero theorem

[Zero α] {M : Matrix m n α} : Mᵀ = 0 ↔ M = 0

Full source

@[simp]
theorem transpose_eq_zero [Zero α] {M : Matrix m n α} : MᵀMᵀ = 0 ↔ M = 0 := transpose_inj

Transpose Equals Zero Matrix Criterion: $M^\top = 0 \leftrightarrow M = 0$

Informal description

For any type $\alpha$ with a zero element and any matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, the transpose of $M$ equals the zero matrix if and only if $M$ itself equals the zero matrix, i.e., $M^\top = 0 \leftrightarrow M = 0$.

Matrix.transpose_add theorem

[Add α] (M : Matrix m n α) (N : Matrix m n α) : (M + N)ᵀ = Mᵀ + Nᵀ

Full source

@[simp]
theorem transpose_add [Add α] (M : Matrix m n α) (N : Matrix m n α) : (M + N)ᵀ = Mᵀ + Nᵀ := by
  ext
  simp

Transpose of Matrix Sum: $(M + N)^\top = M^\top + N^\top$

Informal description

For any two matrices $M$ and $N$ of type $\mathrm{Matrix}\, m\, n\, \alpha$ where $\alpha$ has an addition operation, the transpose of their sum equals the sum of their transposes, i.e., $(M + N)^\top = M^\top + N^\top$.

Matrix.transpose_sub theorem

[Sub α] (M : Matrix m n α) (N : Matrix m n α) : (M - N)ᵀ = Mᵀ - Nᵀ

Full source

@[simp]
theorem transpose_sub [Sub α] (M : Matrix m n α) (N : Matrix m n α) : (M - N)ᵀ = Mᵀ - Nᵀ := by
  ext
  simp

Transpose of Matrix Difference: $(M - N)^\top = M^\top - N^\top$

Informal description

Let $\alpha$ be a type equipped with a subtraction operation, and let $M$ and $N$ be matrices in $\mathrm{Matrix}\, m\, n\, \alpha$. Then the transpose of the difference of $M$ and $N$ is equal to the difference of their transposes, i.e., $$(M - N)^\top = M^\top - N^\top.$$

Matrix.transpose_smul theorem

{R : Type*} [SMul R α] (c : R) (M : Matrix m n α) : (c • M)ᵀ = c • Mᵀ

Full source

@[simp]
theorem transpose_smul {R : Type*} [SMul R α] (c : R) (M : Matrix m n α) : (c • M)ᵀ = c • Mᵀ := by
  ext
  rfl

Transpose Commutes with Scalar Multiplication: $(c \cdot M)^\top = c \cdot M^\top$

Informal description

For any scalar $c$ in a type $R$ with a scalar multiplication operation on a type $\alpha$, and any matrix $M \in \text{Matrix}\, m\, n\, \alpha$, the transpose of the scalar multiple $c \cdot M$ is equal to the scalar multiple of the transpose of $M$, i.e., $(c \cdot M)^\top = c \cdot M^\top$.

Matrix.transpose_neg theorem

[Neg α] (M : Matrix m n α) : (-M)ᵀ = -Mᵀ

Full source

@[simp]
theorem transpose_neg [Neg α] (M : Matrix m n α) : (-M)ᵀ = -Mᵀ := by
  ext
  rfl

Transpose of Negated Matrix Equals Negated Transpose

Informal description

For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$ where $\alpha$ has a negation operation, the transpose of the negation of $M$ equals the negation of the transpose of $M$, i.e., $(-M)^\top = -M^\top$.

Matrix.transpose_map theorem

{f : α → β} {M : Matrix m n α} : Mᵀ.map f = (M.map f)ᵀ

Full source

theorem transpose_map {f : α → β} {M : Matrix m n α} : Mᵀ.map f = (M.map f)ᵀ := by
  ext
  rfl

Transpose Commutes with Entry-wise Map: $(f(M))^\top = f(M^\top)$

Informal description

For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$ and any function $f : \alpha \to \beta$, the transpose of the entry-wise mapped matrix $(M \text{map} f)^\top$ is equal to the entry-wise mapped transpose $M^\top \text{map} f$. In other words, $(f(M_{i,j}))^\top = f(M^\top_{i,j})$ for all $i \in m$ and $j \in n$.

Matrix.submatrix definition

(A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) : Matrix l o α

Full source

/-- 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. -/
def submatrix (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) : Matrix l o α :=
  of fun i j => A (r_reindex i) (c_reindex j)

Submatrix via row and column reindexing

Informal description

Given a matrix $A$ of size $m \times n$ with entries in $\alpha$, and reindexing functions $r_{\text{reindex}} : l \to m$ for rows and $c_{\text{reindex}} : o \to n$ for columns, the submatrix $A.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}}$ is the $l \times o$ matrix defined by $(A.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}})_{i,j} = A_{r_{\text{reindex}}(i), c_{\text{reindex}}(j)}$ for each $(i,j) \in l \times o$. The total number of rows and columns may change based on the reindexing functions.

Matrix.submatrix_apply theorem

 (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) (i j) :
  A.submatrix r_reindex c_reindex i j = A (r_reindex i) (c_reindex j)

Full source

@[simp]
theorem submatrix_apply (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) (i j) :
    A.submatrix r_reindex c_reindex i j = A (r_reindex i) (c_reindex j) :=
  rfl

Submatrix Entry Formula: $(A.\text{submatrix}\, r\, c)_{i,j} = A_{r(i), c(j)}$

Informal description

For any matrix $A \in \text{Matrix}(m, n, \alpha)$, row reindexing function $r_{\text{reindex}} : l \to m$, column reindexing function $c_{\text{reindex}} : o \to n$, and indices $i \in l$, $j \in o$, the $(i,j)$-entry of the submatrix $A.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}}$ is equal to the $(r_{\text{reindex}}(i), c_{\text{reindex}}(j))$-entry of $A$, i.e., $$(A.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}})_{i,j} = A_{r_{\text{reindex}}(i), c_{\text{reindex}}(j)}.$$

Matrix.submatrix_id_id theorem

(A : Matrix m n α) : A.submatrix id id = A

Full source

@[simp]
theorem submatrix_id_id (A : Matrix m n α) : A.submatrix id id = A :=
  ext fun _ _ => rfl

Submatrix Identity: $A.\text{submatrix}\, \text{id}\, \text{id} = A$

Informal description

For any matrix $A$ of size $m \times n$ with entries in $\alpha$, the submatrix obtained by reindexing both rows and columns with the identity function is equal to $A$ itself, i.e., $A.\text{submatrix}\, \text{id}\, \text{id} = A$.

Matrix.submatrix_submatrix theorem

 {l₂ o₂ : Type*} (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₂)

Full source

@[simp]
theorem submatrix_submatrix {l₂ o₂ : Type*} (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₂) :=
  ext fun _ _ => rfl

Iterated Submatrix Equals Composition of Reindexings

Informal description

Let $A$ be an $m \times n$ matrix with entries in $\alpha$, and let $r_1 : l \to m$ and $c_1 : o \to n$ be row and column reindexing functions. For any further reindexing functions $r_2 : l_2 \to l$ and $c_2 : o_2 \to o$, the iterated submatrix $(A.\text{submatrix}\, r_1\, c_1).\text{submatrix}\, r_2\, c_2$ is equal to the single submatrix $A.\text{submatrix}\, (r_1 \circ r_2)\, (c_1 \circ c_2)$.

Matrix.transpose_submatrix theorem

 (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) :
  (A.submatrix r_reindex c_reindex)ᵀ = Aᵀ.submatrix c_reindex r_reindex

Full source

@[simp]
theorem transpose_submatrix (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) :
    (A.submatrix r_reindex c_reindex)ᵀ = Aᵀ.submatrix c_reindex r_reindex :=
  ext fun _ _ => rfl

Transpose of Submatrix Equals Submatrix of Transpose with Swapped Reindexings

Informal description

Let $A$ be an $m \times n$ matrix with entries in $\alpha$, and let $r_{\text{reindex}} : l \to m$ and $c_{\text{reindex}} : o \to n$ be reindexing functions for the rows and columns, respectively. Then the transpose of the submatrix of $A$ obtained by these reindexings is equal to the submatrix of the transpose of $A$ obtained by swapping the row and column reindexing functions. In symbols: $$(A.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}})^\top = A^\top.\text{submatrix}\, c_{\text{reindex}}\, r_{\text{reindex}}.$$

Matrix.submatrix_add theorem

 [Add α] (A B : Matrix m n α) : ((A + B).submatrix : (l → m) → (o → n) → Matrix l o α) = A.submatrix + B.submatrix

Full source

theorem submatrix_add [Add α] (A B : Matrix m n α) :
    ((A + B).submatrix : (l → m) → (o → n) → Matrix l o α) = A.submatrix + B.submatrix :=
  rfl

Submatrix of Sum Equals Sum of Submatrices

Informal description

Let $\alpha$ be a type equipped with an addition operation, and let $A$ and $B$ be $m \times n$ matrices with entries in $\alpha$. For any row reindexing function $r_{\text{reindex}} : l \to m$ and column reindexing function $c_{\text{reindex}} : o \to n$, the submatrix of the sum $A + B$ is equal to the sum of the submatrices of $A$ and $B$: \[ (A + B).\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}} = A.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}} + B.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}}. \]

Matrix.submatrix_neg theorem

[Neg α] (A : Matrix m n α) : ((-A).submatrix : (l → m) → (o → n) → Matrix l o α) = -A.submatrix

Full source

theorem submatrix_neg [Neg α] (A : Matrix m n α) :
    ((-A).submatrix : (l → m) → (o → n) → Matrix l o α) = -A.submatrix :=
  rfl

Negation Commutes with Submatrix Operation

Informal description

For any matrix $A$ of size $m \times n$ with entries in a type $\alpha$ equipped with a negation operation, and for any reindexing functions $r_{\text{reindex}} : l \to m$ and $c_{\text{reindex}} : o \to n$, the submatrix of the negation of $A$ is equal to the negation of the submatrix of $A$. That is, $$(-A).\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}} = -(A.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}}).$$

Matrix.submatrix_sub theorem

 [Sub α] (A B : Matrix m n α) : ((A - B).submatrix : (l → m) → (o → n) → Matrix l o α) = A.submatrix - B.submatrix

Full source

theorem submatrix_sub [Sub α] (A B : Matrix m n α) :
    ((A - B).submatrix : (l → m) → (o → n) → Matrix l o α) = A.submatrix - B.submatrix :=
  rfl

Submatrix of Matrix Difference Equals Difference of Submatrices

Informal description

For any type $\alpha$ with a subtraction operation, and matrices $A, B$ of size $m \times n$ with entries in $\alpha$, the submatrix of the difference $A - B$ is equal to the difference of the submatrices of $A$ and $B$. That is, for any row reindexing function $r_{\text{reindex}} : l \to m$ and column reindexing function $c_{\text{reindex}} : o \to n$, we have $$(A - B).\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}} = A.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}} - B.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}}.$$

Matrix.submatrix_zero theorem

[Zero α] : ((0 : Matrix m n α).submatrix : (l → m) → (o → n) → Matrix l o α) = 0

Full source

@[simp]
theorem submatrix_zero [Zero α] :
    ((0 : Matrix m n α).submatrix : (l → m) → (o → n) → Matrix l o α) = 0 :=
  rfl

Submatrix of Zero Matrix is Zero Matrix

Informal description

For any type $\alpha$ with a zero element, the submatrix of the zero matrix (of size $m \times n$) obtained by reindexing rows and columns via functions $l \to m$ and $o \to n$ respectively, is equal to the zero matrix of size $l \times o$. In other words, if $0$ denotes the zero matrix in $\mathrm{Matrix}\, m\, n\, \alpha$, then for any reindexing functions $r : l \to m$ and $c : o \to n$, we have $(0.\text{submatrix}\, r\, c) = 0$.

Matrix.submatrix_smul theorem

 {R : Type*} [SMul R α] (r : R) (A : Matrix m n α) :
  ((r • A : Matrix m n α).submatrix : (l → m) → (o → n) → Matrix l o α) = r • A.submatrix

Full source

theorem submatrix_smul {R : Type*} [SMul R α] (r : R) (A : Matrix m n α) :
    ((r • A : Matrix m n α).submatrix : (l → m) → (o → n) → Matrix l o α) = r • A.submatrix :=
  rfl

Submatrix Commutes with Scalar Multiplication: $(r \cdot A)_{\text{sub}} = r \cdot A_{\text{sub}}$

Informal description

Let $R$ be a type with a scalar multiplication operation on a type $\alpha$, and let $r \in R$. For any matrix $A \in \text{Matrix}\, m\, n\, \alpha$ and reindexing functions $r_{\text{reindex}} : l \to m$ and $c_{\text{reindex}} : o \to n$, the submatrix of the scalar multiple $r \cdot A$ is equal to the scalar multiple of the submatrix of $A$. That is, $$(r \cdot A).\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}} = r \cdot (A.\text{submatrix}\, r_{\text{reindex}}\, c_{\text{reindex}}).$$

Matrix.submatrix_map theorem

 (f : α → β) (e₁ : l → m) (e₂ : o → n) (A : Matrix m n α) : (A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f

Full source

theorem submatrix_map (f : α → β) (e₁ : l → m) (e₂ : o → n) (A : Matrix m n α) :
    (A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f :=
  rfl

Commutativity of Submatrix and Entry-wise Map: $(A.\text{map}\, f).\text{submatrix}\, e_1\, e_2 = (A.\text{submatrix}\, e_1\, e_2).\text{map}\, f$

Informal description

Let $A$ be an $m \times n$ matrix with entries in $\alpha$, $f : \alpha \to \beta$ a function, and $e_1 : l \to m$, $e_2 : o \to n$ reindexing functions. Then the submatrix of the entry-wise mapped matrix $(A.\text{map}\, f)$ under reindexing $e_1$ and $e_2$ is equal to the entry-wise mapped submatrix of $A$ under the same reindexing, i.e., $$(A.\text{map}\, f).\text{submatrix}\, e_1\, e_2 = (A.\text{submatrix}\, e_1\, e_2).\text{map}\, f.$$

Matrix.reindex definition

(eₘ : m ≃ l) (eₙ : n ≃ o) : Matrix m n α ≃ Matrix l o α

Full source

/-- The natural map that reindexes a matrix's rows and columns with equivalent types is an
equivalence. -/
def reindex (eₘ : m ≃ l) (eₙ : n ≃ o) : MatrixMatrix m n α ≃ Matrix l o α where
  toFun M := M.submatrix eₘ.symm eₙ.symm
  invFun M := M.submatrix eₘ eₙ
  left_inv M := by simp
  right_inv M := by simp

Matrix reindexing equivalence

Informal description

Given an equivalence $e_m : m \simeq l$ between row index types and an equivalence $e_n : n \simeq o$ between column index types, the function `Matrix.reindex` defines a bijection between the space of $m \times n$ matrices over $\alpha$ and the space of $l \times o$ matrices over $\alpha$. Specifically: - The forward map takes a matrix $M$ and returns its submatrix obtained by reindexing rows via $e_m^{-1}$ and columns via $e_n^{-1}$. - The inverse map takes a matrix $N$ and returns its submatrix obtained by reindexing rows via $e_m$ and columns via $e_n$. This construction ensures that `Matrix.reindex` forms an equivalence (bijection with inverse) between the two matrix spaces.

Matrix.reindex_apply theorem

(eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) : reindex eₘ eₙ M = M.submatrix eₘ.symm eₙ.symm

Full source

@[simp]
theorem reindex_apply (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) :
    reindex eₘ eₙ M = M.submatrix eₘ.symm eₙ.symm :=
  rfl

Reindexed Matrix Equals Submatrix with Inverse Reindexing

Informal description

Given a matrix $M$ of size $m \times n$ with entries in $\alpha$, and equivalences $e_m : m \simeq l$ and $e_n : n \simeq o$ between index types, the reindexed matrix $\text{reindex}\, e_m\, e_n\, M$ is equal to the submatrix of $M$ obtained by reindexing rows via $e_m^{-1}$ and columns via $e_n^{-1}$. That is, $$\text{reindex}\, e_m\, e_n\, M = M.\text{submatrix}\, e_m^{-1}\, e_n^{-1}.$$

Matrix.reindex_refl_refl theorem

(A : Matrix m n α) : reindex (Equiv.refl _) (Equiv.refl _) A = A

Full source

theorem reindex_refl_refl (A : Matrix m n α) : reindex (Equiv.refl _) (Equiv.refl _) A = A :=
  A.submatrix_id_id

Matrix Reindexing with Identity Equivalences Preserves Matrix

Informal description

For any matrix $A$ of size $m \times n$ with entries in $\alpha$, reindexing $A$ using the identity equivalence on both row and column indices leaves the matrix unchanged, i.e., $\text{reindex}(\text{Equiv.refl}\, m, \text{Equiv.refl}\, n)\, A = A$.

Matrix.reindex_symm theorem

(eₘ : m ≃ l) (eₙ : n ≃ o) : (reindex eₘ eₙ).symm = (reindex eₘ.symm eₙ.symm : Matrix l o α ≃ _)

Full source

@[simp]
theorem reindex_symm (eₘ : m ≃ l) (eₙ : n ≃ o) :
    (reindex eₘ eₙ).symm = (reindex eₘ.symm eₙ.symm : MatrixMatrix l o α ≃ _) :=
  rfl

Inverse of Matrix Reindexing Equals Reindexing by Inverses

Informal description

Given bijections $e_m : m \leftrightarrow l$ between row index types and $e_n : n \leftrightarrow o$ between column index types, the inverse of the matrix reindexing operation `reindex eₘ eₙ` is equal to reindexing with the inverse bijections `reindex eₘ.symm eₙ.symm`. In other words, for any matrix $A$ of type $\text{Matrix } l o \alpha$, we have: $$(\text{reindex } e_m e_n)^{-1}(A) = \text{reindex } e_m^{-1} e_n^{-1}(A)$$

Matrix.reindex_trans theorem

 {l₂ o₂ : Type*} (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ₙ₂) : Matrix m n α ≃ _)

Full source

@[simp]
theorem reindex_trans {l₂ o₂ : Type*} (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ₙ₂) : MatrixMatrix m n α ≃ _) :=
  Equiv.ext fun A => (A.submatrix_submatrix eₘ.symm eₙ.symm eₘ₂.symm eₙ₂.symm :)

Composition of Matrix Reindexing Equivalences via Index Equivalence Composition

Informal description

Let $e_m : m \simeq l$ and $e_n : n \simeq o$ be equivalences between row and column index types, respectively, and let $e_{m_2} : l \simeq l_2$ and $e_{n_2} : o \simeq o_2$ be further equivalences. Then the composition of matrix reindexing equivalences $\text{reindex}\, e_m\, e_n$ and $\text{reindex}\, e_{m_2}\, e_{n_2}$ is equal to the single reindexing equivalence $\text{reindex}\, (e_m \circ e_{m_2})\, (e_n \circ e_{n_2})$.

Matrix.transpose_reindex theorem

(eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) : (reindex eₘ eₙ M)ᵀ = reindex eₙ eₘ Mᵀ

Full source

theorem transpose_reindex (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) :
    (reindex eₘ eₙ M)ᵀ = reindex eₙ eₘ Mᵀ :=
  rfl

Transpose Commutes with Reindexing: $(M_{e_m,e_n})^\top = (M^\top)_{e_n,e_m}$

Informal description

For any bijections $e_m : m \leftrightarrow l$ and $e_n : n \leftrightarrow o$ between index types, and any matrix $M \in \text{Matrix}\, m\, n\, \alpha$, the transpose of the reindexed matrix equals the reindexed transpose matrix. That is, $$(M_{e_m^{-1}(i), e_n^{-1}(j)})^\top = (M^\top)_{e_n^{-1}(j), e_m^{-1}(i)}$$ for all $i \in l$ and $j \in o$.

Matrix.subLeft abbrev

{m l r : Nat} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin l) α

Full source

/-- The left `n × l` part of an `n × (l+r)` matrix. -/
abbrev subLeft {m l r : Nat} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin l) α :=
  submatrix A id (Fin.castAdd r)

Left submatrix of a matrix with split columns

Informal description

For a matrix $A$ of size $m \times (l + r)$ with entries in type $\alpha$, the left submatrix $\text{subLeft}\, A$ is the $m \times l$ matrix consisting of the first $l$ columns of $A$.

Matrix.subRight abbrev

{m l r : Nat} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin r) α

Full source

/-- The right `n × r` part of an `n × (l+r)` matrix. -/
abbrev subRight {m l r : Nat} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin r) α :=
  submatrix A id (Fin.natAdd l)

Right submatrix of an $m \times (l + r)$ matrix

Informal description

Given a matrix $A$ of size $m \times (l + r)$ with entries in type $\alpha$, the submatrix $\text{subRight}\, A$ is the $m \times r$ matrix consisting of the rightmost $r$ columns of $A$.

Matrix.subUp abbrev

{d u n : Nat} (A : Matrix (Fin (u + d)) (Fin n) α) : Matrix (Fin u) (Fin n) α

Full source

/-- The top `u × n` part of a `(u+d) × n` matrix. -/
abbrev subUp {d u n : Nat} (A : Matrix (Fin (u + d)) (Fin n) α) : Matrix (Fin u) (Fin n) α :=
  submatrix A (Fin.castAdd d) id

Upper submatrix extraction: $\text{subUp}(A) = A_{\text{rows } 1..u}$

Informal description

For natural numbers $u$, $d$, and $n$, and a matrix $A$ of size $(u + d) \times n$ with entries in type $\alpha$, the submatrix $\text{subUp}(A)$ is the $u \times n$ matrix consisting of the first $u$ rows of $A$.

Matrix.subDown abbrev

{d u n : Nat} (A : Matrix (Fin (u + d)) (Fin n) α) : Matrix (Fin d) (Fin n) α

Full source

/-- The bottom `d × n` part of a `(u+d) × n` matrix. -/
abbrev subDown {d u n : Nat} (A : Matrix (Fin (u + d)) (Fin n) α) : Matrix (Fin d) (Fin n) α :=
  submatrix A (Fin.natAdd u) id

Bottom Submatrix of a Matrix

Informal description

Given a matrix $A$ of size $(u + d) \times n$ with entries in type $\alpha$, the submatrix $\text{subDown}\, A$ is the $d \times n$ matrix consisting of the bottom $d$ rows of $A$.

Matrix.subUpRight abbrev

{d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin u) (Fin r) α

Full source

/-- The top-right `u × r` part of a `(u+d) × (l+r)` matrix. -/
abbrev subUpRight {d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) :
    Matrix (Fin u) (Fin r) α :=
  subUp (subRight A)

Upper-right submatrix of a block matrix

Informal description

Given natural numbers $d, u, l, r$ and a matrix $A$ of size $(u + d) \times (l + r)$ with entries in type $\alpha$, the submatrix $\text{subUpRight}(A)$ is the $u \times r$ matrix consisting of the intersection of the first $u$ rows and the last $r$ columns of $A$.

Matrix.subDownRight abbrev

{d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin d) (Fin r) α

Full source

/-- The bottom-right `d × r` part of a `(u+d) × (l+r)` matrix. -/
abbrev subDownRight {d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) :
    Matrix (Fin d) (Fin r) α :=
  subDown (subRight A)

Bottom-Right Submatrix of a Matrix

Informal description

Given a matrix $A$ of size $(u + d) \times (l + r)$ with entries in type $\alpha$, the submatrix $\text{subDownRight}\, A$ is the $d \times r$ matrix consisting of the bottom $d$ rows and rightmost $r$ columns of $A$.

Matrix.subUpLeft abbrev

{d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin u) (Fin l) α

Full source

/-- The top-left `u × l` part of a `(u+d) × (l+r)` matrix. -/
abbrev subUpLeft {d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) :
    Matrix (Fin u) (Fin l) α :=
  subUp (subLeft A)

Top-left submatrix extraction: $\text{subUpLeft}(A) = A_{1..u, 1..l}$

Informal description

For natural numbers $u$, $d$, $l$, and $r$, and a matrix $A$ of size $(u + d) \times (l + r)$ with entries in type $\alpha$, the submatrix $\text{subUpLeft}(A)$ is the $u \times l$ matrix consisting of the top-left block of $A$ formed by the first $u$ rows and first $l$ columns.

Matrix.subDownLeft abbrev

{d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin d) (Fin l) α

Full source

/-- The bottom-left `d × l` part of a `(u+d) × (l+r)` matrix. -/
abbrev subDownLeft {d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) :
    Matrix (Fin d) (Fin l) α :=
  subDown (subLeft A)

Bottom-left submatrix of a matrix with split rows and columns

Informal description

Given a matrix $A$ of size $(u + d) \times (l + r)$ with entries in type $\alpha$, the submatrix $\text{subDownLeft}\, A$ is the $d \times l$ matrix consisting of the bottom $d$ rows and leftmost $l$ columns of $A$.

Matrix.row definition

(A : Matrix m n α) : m → n → α

Full source

/-- For an `m × n` `α`-matrix `A`, `A.row i` is the `i`th row of `A` as a vector in `n → α`.
`A.row` is defeq to `A`, but explicitly refers to the 'row function` of `A`
while avoiding defeq abuse and noisy eta-expansions,
such as in expressions like `Set.Injective A.row` and `Set.range A.row`.
(Note 2025-04-07 : the identifier `Matrix.row` used to refer to a matrix with all rows equal;
this is now called `Matrix.replicateRow`) -/
def row (A : Matrix m n α) : m → n → α := A

Row extraction function for a matrix

Informal description

For an $m \times n$ matrix $A$ with entries in $\alpha$, the function $A.\text{row}$ maps a row index $i$ to the $i$-th row of $A$, represented as a vector in $n \to \alpha$. This function is definitionally equal to $A$ itself, but is used to explicitly refer to the row function of $A$ to avoid defeq abuse and noisy eta-expansions in expressions like $\text{Set.Injective } A.\text{row}$ and $\text{Set.range } A.\text{row}$.

Matrix.col definition

(A : Matrix m n α) : n → m → α

Full source

/-- For an `m × n` `α`-matrix `A`, `A.col j` is the `j`th 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`) -/
def col (A : Matrix m n α) : n → m → α := Aᵀ

Column extraction function for a matrix

Informal description

For an $m \times n$ matrix $A$ with entries in $\alpha$, the function $A.\text{col}$ maps a column index $j$ to the $j$-th column of $A$, represented as a vector in $m \to \alpha$. This function is definitionally equal to the transpose $A^\top$, but is used to explicitly refer to the column function of $A$ to avoid defeq abuse and noisy eta-expansions in expressions like $\text{Set.Injective } A.\text{col}$ and $\text{Set.range } A.\text{col}$.

Matrix.row_eq_self theorem

(A : Matrix m n α) : A.row = of.symm A

Full source

lemma row_eq_self (A : Matrix m n α) : A.row = of.symm A := rfl

Row Extraction Equals Inverse of Matrix Construction

Informal description

For any matrix $A$ of type $\text{Matrix}\, m\, n\, \alpha$, the row extraction function $A.\text{row}$ is equal to the inverse of the matrix construction function $\text{Matrix.of}$ applied to $A$.

Matrix.col_eq_transpose theorem

(A : Matrix m n α) : A.col = of.symm Aᵀ

Full source

lemma col_eq_transpose (A : Matrix m n α) : A.col = of.symm Aᵀ := rfl

Column Extraction Equals Inverse Construction of Transpose

Informal description

For any matrix $A \in \text{Matrix}\, m\, n\, \alpha$, the column extraction function $A.\text{col}$ is equal to the inverse of the matrix construction function $\text{Matrix.of}$ applied to the transpose $A^\top$. That is, $A.\text{col} = \text{Matrix.of}^{-1}(A^\top)$.

Matrix.of_row theorem

(f : m → n → α) : (Matrix.of f).row = f

Full source

@[simp]
lemma of_row (f : m → n → α) : (Matrix.of f).row = f := rfl

Row Function of Matrix Construction from Function

Informal description

For any function $f : m \to n \to \alpha$, the row function of the matrix constructed from $f$ via `Matrix.of` is equal to $f$ itself. That is, $(\text{Matrix.of}\, f).\text{row} = f$.

Matrix.of_col theorem

(f : m → n → α) : (Matrix.of f)ᵀ.col = f

Full source

@[simp]
lemma of_col (f : m → n → α) : (Matrix.of f)ᵀ.col = f := rfl

Column Function Preservation under Matrix Construction and Transpose

Informal description

For any function $f : m \to n \to \alpha$, the column function of the transpose of the matrix constructed from $f$ via `Matrix.of` is equal to $f$ itself. That is, $(\text{Matrix.of}\, f)^\top.\text{col} = f$.

Matrix.row_def theorem

(A : Matrix m n α) : A.row = fun i ↦ A i

Full source

lemma row_def (A : Matrix m n α) : A.row = fun i ↦ A i := rfl

Definition of Matrix Row Function

Informal description

For any $m \times n$ matrix $A$ with entries in type $\alpha$, the row function $A.\text{row}$ is equal to the function mapping each row index $i$ to the $i$-th row of $A$ (i.e., $\lambda i, A i$).

Matrix.col_def theorem

(A : Matrix m n α) : A.col = fun j ↦ Aᵀ j

Full source

lemma col_def (A : Matrix m n α) : A.col = fun j ↦ Aᵀ j := rfl

Column Function as Transpose Rows: $A.\text{col} = \lambda j, A^\top j$

Informal description

For any $m \times n$ matrix $A$ with entries in type $\alpha$, the column function $A.\text{col}$ is equal to the function mapping each column index $j$ to the $j$-th column of the transpose matrix $A^\top$.

Matrix.row_apply theorem

(A : Matrix m n α) (i : m) (j : n) : A.row i j = A i j

Full source

@[simp]
lemma row_apply (A : Matrix m n α) (i : m) (j : n) : A.row i j = A i j := rfl

Matrix Row Entry Equivalence: $(A.\text{row}\ i)\ j = A\ i\ j$

Informal description

For any $m \times n$ matrix $A$ with entries in type $\alpha$, and for any row index $i \in m$ and column index $j \in n$, the entry in the $i$-th row and $j$-th column of $A$ is equal to the $(i,j)$-th entry of $A$ when accessed directly, i.e., $(A.\text{row}\ i)\ j = A\ i\ j$.

Matrix.row_apply' theorem

(A : Matrix m n α) (i : m) : A.row i = A i

Full source

/-- A partially applied version of `Matrix.row_apply` -/
lemma row_apply' (A : Matrix m n α) (i : m) : A.row i = A i := rfl

Row Extraction Identity: $A.\text{row}(i) = A i$

Informal description

For any $m \times n$ matrix $A$ with entries in a type $\alpha$ and any row index $i \in m$, the $i$-th row of $A$ (as a function) is equal to the function $A i$ representing the entries in the $i$-th row. That is, $A.\text{row}(i) = A i$.

Matrix.col_apply theorem

(A : Matrix m n α) (i : n) (j : m) : A.col i j = A j i

Full source

@[simp]
lemma col_apply (A : Matrix m n α) (i : n) (j : m) : A.col i j = A j i := rfl

Matrix Column Entry Equivalence: $(A.\text{col}\ i)\ j = A\ j\ i$

Informal description

For any $m \times n$ matrix $A$ with entries in a type $\alpha$, and for any column index $i \in n$ and row index $j \in m$, the entry in the $i$-th column and $j$-th row of $A$ is equal to the $(j,i)$-th entry of $A$ when accessed directly, i.e., $(A.\text{col}\ i)\ j = A\ j\ i$.

Matrix.col_apply' theorem

(A : Matrix m n α) (i : n) : A.col i = fun j ↦ A j i

Full source

/-- A partially applied version of `Matrix.col_apply` -/
lemma col_apply' (A : Matrix m n α) (i : n) : A.col i = fun j ↦ A j i := rfl

Column Extraction Identity: $A.\text{col}(i) = (\lambda j, A j i)$

Informal description

For any $m \times n$ matrix $A$ with entries in a type $\alpha$ and any column index $i \in n$, the $i$-th column of $A$ (as a function) is equal to the function $\lambda j, A j i$ representing the entries in the $i$-th column. That is, $A.\text{col}(i) = (\lambda j, A j i)$.

Matrix.row_submatrix theorem

 {m₀ n₀ : Type*} (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)

Full source

lemma row_submatrix {m₀ n₀ : Type*} (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) := rfl

Row Extraction of Submatrix via Row Reindexing

Informal description

Let $A$ be an $m \times n$ matrix with entries in a type $\alpha$, and let $r : m_0 \to m$ and $c : n_0 \to n$ be reindexing functions. For any row index $i \in m_0$, the $i$-th row of the submatrix $A.\text{submatrix}\, r\, c$ is equal to the $r(i)$-th row of the submatrix $A.\text{submatrix}\, \text{id}\, c$.

Matrix.row_submatrix_eq_comp theorem

 {m₀ n₀ : Type*} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (i : m₀) : (A.submatrix r c).row i = A.row (r i) ∘ c

Full source

lemma row_submatrix_eq_comp {m₀ n₀ : Type*} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (i : m₀) :
    (A.submatrix r c).row i = A.row (r i) ∘ c := rfl

Row of Submatrix as Composition of Row and Reindexing Function

Informal description

For any matrix $A$ of size $m \times n$ with entries in $\alpha$, and reindexing functions $r : m_0 \to m$ for rows and $c : n_0 \to n$ for columns, the $i$-th row of the submatrix $A.\text{submatrix}\, r\, c$ is equal to the composition of the $r(i)$-th row of $A$ with the column reindexing function $c$. That is, $(A.\text{submatrix}\, r\, c).\text{row}\, i = A.\text{row}\, (r\, i) \circ c$.

Matrix.col_submatrix theorem

 {m₀ n₀ : Type*} (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)

Full source

lemma col_submatrix {m₀ n₀ : Type*} (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) := rfl

Column Extraction of Submatrix via Column Reindexing

Informal description

Let $A$ be an $m \times n$ matrix with entries in a type $\alpha$, and let $r : m_0 \to m$ and $c : n_0 \to n$ be reindexing functions. For any column index $j \in n_0$, the $j$-th column of the submatrix $A.\text{submatrix}\, r\, c$ is equal to the $c(j)$-th column of the submatrix $A.\text{submatrix}\, r\, \text{id}$.

Matrix.col_submatrix_eq_comp theorem

 {m₀ n₀ : Type*} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (j : n₀) : (A.submatrix r c).col j = A.col (c j) ∘ r

Full source

lemma col_submatrix_eq_comp {m₀ n₀ : Type*} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (j : n₀) :
    (A.submatrix r c).col j = A.col (c j) ∘ r := rfl

Column of Submatrix as Composition of Column and Reindexing Function

Informal description

For any matrix $A$ of size $m \times n$ with entries in $\alpha$, reindexing functions $r : m_0 \to m$ for rows and $c : n_0 \to n$ for columns, and column index $j \in n_0$, the $j$-th column of the submatrix $A.\text{submatrix}\, r\, c$ is equal to the composition of the $c(j)$-th column of $A$ with the row reindexing function $r$. That is, $(A.\text{submatrix}\, r\, c).\text{col}\, j = A.\text{col}\, (c\, j) \circ r$.

Matrix.row_map theorem

(A : Matrix m n α) (f : α → β) (i : m) : (A.map f).row i = f ∘ A.row i

Full source

lemma row_map (A : Matrix m n α) (f : α → β) (i : m) : (A.map f).row i = f ∘ A.row i := rfl

Row-wise Mapping of Matrix Entries via Function Composition

Informal description

For any matrix $A \in \text{Matrix}\, m\, n\, \alpha$, any function $f : \alpha \to \beta$, and any row index $i \in m$, the $i$-th row of the mapped matrix $A.\text{map}\, f$ is equal to the composition $f \circ (A.\text{row}\, i)$. In other words, $(A.\text{map}\, f)_{i*} = f \circ A_{i*}$ where $A_{i*}$ denotes the $i$-th row of $A$.

Matrix.col_map theorem

(A : Matrix m n α) (f : α → β) (j : n) : (A.map f).col j = f ∘ A.col j

Full source

lemma col_map (A : Matrix m n α) (f : α → β) (j : n) : (A.map f).col j = f ∘ A.col j := rfl

Column-wise Mapping of Matrix Entries via Function Composition

Informal description

For any $m \times n$ matrix $A$ with entries in $\alpha$, any function $f : \alpha \to \beta$, and any column index $j \in n$, the $j$-th column of the mapped matrix $A.\text{map}\, f$ is equal to the composition $f \circ (A.\text{col}\, j)$. In other words, $(A.\text{map}\, f)_{*j} = f \circ A_{*j}$ where $A_{*j}$ denotes the $j$-th column of $A$.

Matrix.row_transpose theorem

(A : Matrix m n α) : Aᵀ.row = A.col

Full source

@[simp]
lemma row_transpose (A : Matrix m n α) : Aᵀ.row = A.col := rfl

Row Function of Transpose Equals Column Function

Informal description

For any $m \times n$ matrix $A$ with entries in $\alpha$, the row function of the transpose matrix $A^\top$ is equal to the column function of $A$, i.e., $(A^\top).\text{row} = A.\text{col}$.

Matrix.col_transpose theorem

(A : Matrix m n α) : Aᵀ.col = A.row

Full source

@[simp]
lemma col_transpose (A : Matrix m n α) : Aᵀ.col = A.row := rfl

Transpose Column-Row Equality: $(A^\top).\text{col} = A.\text{row}$

Informal description

For any $m \times n$ matrix $A$ with entries in a type $\alpha$, the column function of the transpose matrix $A^\top$ is equal to the row function of $A$. That is, for every column index $j$, the $j$-th column of $A^\top$ is the $j$-th row of $A$.

Mathlib.Data.Matrix.Defs

Main definitions

Notation

Implementation notes