# Documentation

Mathlib.Data.Matrix.DMatrix

# Matrices #

def DMatrix (m : Type u) (n : Type u') [inst : ] [inst : ] (α : mnType v) :
Type (maxuu'v)

DMatrix m n is the type of dependently typed matrices whose rows are indexed by the fintype m and whose columns are indexed by the fintype n.

Equations
• DMatrix m n α = ((i : m) → (j : n) → α i j)
theorem DMatrix.ext_iff {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} {M : DMatrix m n α} {N : DMatrix m n α} :
(∀ (i : m) (j : n), M i j = N i j) M = N
theorem DMatrix.ext {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} {M : DMatrix m n α} {N : DMatrix m n α} :
(∀ (i : m) (j : n), M i j = N i j) → M = N
def DMatrix.map {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} (M : DMatrix m n α) {β : mnType w} (f : i : m⦄ → j : n⦄ → α i jβ i j) :
DMatrix m n β

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

Equations
@[simp]
theorem DMatrix.map_apply {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} {M : DMatrix m n α} {β : mnType w} {f : i : m⦄ → j : n⦄ → α i jβ i j} {i : m} {j : n} :
DMatrix.map M f i j = f i j (M i j)
@[simp]
theorem DMatrix.map_map {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} {M : DMatrix m n α} {β : mnType w} {γ : mnType z} {f : i : m⦄ → j : n⦄ → α i jβ i j} {g : i : m⦄ → j : n⦄ → β i jγ i j} :
DMatrix.map () g = DMatrix.map M fun i j x => g i j (f i j x)
def DMatrix.transpose {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} (M : DMatrix m n α) :
DMatrix n m fun j i => α i j

The transpose of a dmatrix.

Equations
• = match x, x with | x, y => M y x

The transpose of a dmatrix.

Equations
def DMatrix.col {m : Type u_1} [inst : ] {α : mType v} (w : (i : m) → α i) :
DMatrix m Unit fun i _j => α i

dmatrix.col u is the column matrix whose entries are given by u.

Equations
def DMatrix.row {n : Type u_1} [inst : ] {α : nType v} (v : (j : n) → α j) :
DMatrix Unit n fun _i j => α j

dmatrix.row u is the row matrix whose entries are given by u.

Equations
instance DMatrix.instInhabitedDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Inhabited (α i j)] :
Equations
• DMatrix.instInhabitedDMatrix = { default := fun i j => default }
instance DMatrix.instAddDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Add (α i j)] :
Equations
instance DMatrix.instAddSemigroupDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddSemigroup (α i j)] :
Equations
instance DMatrix.instAddCommSemigroupDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddCommSemigroup (α i j)] :
Equations
instance DMatrix.instZeroDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Zero (α i j)] :
Zero (DMatrix m n α)
Equations
• DMatrix.instZeroDMatrix = Pi.instZero
instance DMatrix.instAddMonoidDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddMonoid (α i j)] :
Equations
instance DMatrix.instAddCommMonoidDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddCommMonoid (α i j)] :
Equations
instance DMatrix.instNegDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Neg (α i j)] :
Neg (DMatrix m n α)
Equations
• DMatrix.instNegDMatrix = Pi.instNeg
instance DMatrix.instSubDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Sub (α i j)] :
Sub (DMatrix m n α)
Equations
• DMatrix.instSubDMatrix = Pi.instSub
instance DMatrix.instAddGroupDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddGroup (α i j)] :
Equations
instance DMatrix.instAddCommGroupDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddCommGroup (α i j)] :
Equations
instance DMatrix.instUniqueDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Unique (α i j)] :
Unique (DMatrix m n α)
Equations
• DMatrix.instUniqueDMatrix = Pi.unique
instance DMatrix.instSubsingletonDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : ∀ (i : m) (j : n), Subsingleton (α i j)] :
Equations
@[simp]
theorem DMatrix.zero_apply {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Zero (α i j)] (i : m) (j : n) :
OfNat.ofNat (DMatrix m n α) 0 Zero.toOfNat0 i j = 0
@[simp]
theorem DMatrix.neg_apply {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Neg (α i j)] (M : DMatrix m n α) (i : m) (j : n) :
(-DMatrix m n α) DMatrix.instNegDMatrix M i j = -M i j
@[simp]
theorem DMatrix.add_apply {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Add (α i j)] (M : DMatrix m n α) (N : DMatrix m n α) (i : m) (j : n) :
(DMatrix m n α + DMatrix m n α) (DMatrix m n α) instHAdd M N i j = M i j + N i j
@[simp]
theorem DMatrix.sub_apply {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Sub (α i j)] (M : DMatrix m n α) (N : DMatrix m n α) (i : m) (j : n) :
(DMatrix m n α - DMatrix m n α) (DMatrix m n α) instHSub M N i j = M i j - N i j
@[simp]
theorem DMatrix.map_zero {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → Zero (α i j)] {β : mnType w} [inst : (i : m) → (j : n) → Zero (β i j)] {f : i : m⦄ → j : n⦄ → α i jβ i j} (h : ∀ (i : m) (j : n), f i j 0 = 0) :
= 0
theorem DMatrix.map_add {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddMonoid (α i j)] {β : mnType w} [inst : (i : m) → (j : n) → AddMonoid (β i j)] (f : i : m⦄ → j : n⦄ → α i j →+ β i j) (M : DMatrix m n α) (N : DMatrix m n α) :
(DMatrix.map (M + N) fun i j => ↑(f i j)) = (DMatrix.map M fun i j => ↑(f i j)) + DMatrix.map N fun i j => ↑(f i j)
theorem DMatrix.map_sub {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddGroup (α i j)] {β : mnType w} [inst : (i : m) → (j : n) → AddGroup (β i j)] (f : i : m⦄ → j : n⦄ → α i j →+ β i j) (M : DMatrix m n α) (N : DMatrix m n α) :
(DMatrix.map (M - N) fun i j => ↑(f i j)) = (DMatrix.map M fun i j => ↑(f i j)) - DMatrix.map N fun i j => ↑(f i j)
instance DMatrix.subsingleton_of_empty_left {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : ] :
Equations
instance DMatrix.subsingleton_of_empty_right {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : ] :
Equations
def AddMonoidHom.mapDMatrix {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddMonoid (α i j)] {β : mnType w} [inst : (i : m) → (j : n) → AddMonoid (β i j)] (f : i : m⦄ → j : n⦄ → α i j →+ β i j) :
DMatrix m n α →+ DMatrix m n β

The AddMonoidHom between spaces of dependently typed matrices induced by an AddMonoidHom between their coefficients.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddMonoidHom.mapDMatrix_apply {m : Type u_1} {n : Type u_2} [inst : ] [inst : ] {α : mnType v} [inst : (i : m) → (j : n) → AddMonoid (α i j)] {β : mnType w} [inst : (i : m) → (j : n) → AddMonoid (β i j)] (f : i : m⦄ → j : n⦄ → α i j →+ β i j) (M : DMatrix m n α) :
↑() M = DMatrix.map M fun i j => ↑(f i j)