# Dependent-typed matrices #

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

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

In most applications m and n are finite types.

Equations
• DMatrix m n α = ((i : m) → (j : n) → α i j)
Instances For
theorem DMatrix.ext_iff {m : Type u_2} {n : Type u_3} {α : 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_2} {n : Type u_3} {α : 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_2} {n : Type u_3} {α : 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
• M.map f i j = f (M i j)
Instances For
@[simp]
theorem DMatrix.map_apply {m : Type u_2} {n : Type u_3} {α : mnType v} {M : DMatrix m n α} {β : mnType w} {f : i : m⦄ → j : n⦄ → α i jβ i j} {i : m} {j : n} :
M.map f i j = f (M i j)
@[simp]
theorem DMatrix.map_map {m : Type u_2} {n : Type u_3} {α : 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} :
(M.map f).map g = M.map fun (i : m) (j : n) (x : α i j) => g (f x)
def DMatrix.transpose {m : Type u_2} {n : Type u_3} {α : mnType v} (M : DMatrix m n α) :
DMatrix n m fun (j : n) (i : m) => α i j

The transpose of a dmatrix.

Equations
• M.transpose x✝ x = match x✝, x with | x, y => M y x
Instances For

The transpose of a dmatrix.

Equations
Instances For
def DMatrix.col {m : Type u_2} {α : mType v} (w : (i : m) → α i) :
DMatrix m Unit fun (i : m) (_j : Unit) => α i

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

Equations
Instances For
def DMatrix.row {n : Type u_3} {α : nType v} (v : (j : n) → α j) :
DMatrix Unit n fun (_i : Unit) (j : n) => α j

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

Equations
Instances For
instance DMatrix.instInhabited {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Inhabited (α i j)] :
Equations
instance DMatrix.instAdd {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Add (α i j)] :
Equations
instance DMatrix.instAddSemigroup {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddSemigroup (α i j)] :
Equations
instance DMatrix.instAddCommSemigroup {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddCommSemigroup (α i j)] :
Equations
instance DMatrix.instZero {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Zero (α i j)] :
Zero (DMatrix m n α)
Equations
instance DMatrix.instAddMonoid {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddMonoid (α i j)] :
Equations
instance DMatrix.instAddCommMonoid {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddCommMonoid (α i j)] :
Equations
instance DMatrix.instNeg {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Neg (α i j)] :
Neg (DMatrix m n α)
Equations
instance DMatrix.instSub {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Sub (α i j)] :
Sub (DMatrix m n α)
Equations
instance DMatrix.instAddGroup {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddGroup (α i j)] :
Equations
instance DMatrix.instAddCommGroup {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddCommGroup (α i j)] :
Equations
instance DMatrix.instUnique {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Unique (α i j)] :
Unique (DMatrix m n α)
Equations
instance DMatrix.instSubsingleton {m : Type u_2} {n : Type u_3} {α : mnType v} [∀ (i : m) (j : n), Subsingleton (α i j)] :
Equations
• =
@[simp]
theorem DMatrix.zero_apply {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Zero (α i j)] (i : m) (j : n) :
0 i j = 0
@[simp]
theorem DMatrix.neg_apply {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Neg (α i j)] (M : DMatrix m n α) (i : m) (j : n) :
(-M) i j = -M i j
@[simp]
theorem DMatrix.add_apply {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Add (α i j)] (M : DMatrix m n α) (N : DMatrix m n α) (i : m) (j : n) :
(M + N) i j = M i j + N i j
@[simp]
theorem DMatrix.sub_apply {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Sub (α i j)] (M : DMatrix m n α) (N : DMatrix m n α) (i : m) (j : n) :
(M - N) i j = M i j - N i j
@[simp]
theorem DMatrix.map_zero {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → Zero (α i j)] {β : mnType w} [(i : m) → (j : n) → Zero (β i j)] {f : i : m⦄ → j : n⦄ → α i jβ i j} (h : ∀ (i : m) (j : n), f 0 = 0) :
= 0
theorem DMatrix.map_add {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddMonoid (α i j)] {β : mnType w} [(i : m) → (j : n) → AddMonoid (β i j)] (f : i : m⦄ → j : n⦄ → α i j →+ β i j) (M : DMatrix m n α) (N : DMatrix m n α) :
((M + N).map fun (i : m) (j : n) => f) = (M.map fun (i : m) (j : n) => f) + N.map fun (i : m) (j : n) => f
theorem DMatrix.map_sub {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddGroup (α i j)] {β : mnType w} [(i : m) → (j : n) → AddGroup (β i j)] (f : i : m⦄ → j : n⦄ → α i j →+ β i j) (M : DMatrix m n α) (N : DMatrix m n α) :
((M - N).map fun (i : m) (j : n) => f) = (M.map fun (i : m) (j : n) => f) - N.map fun (i : m) (j : n) => f
instance DMatrix.subsingleton_of_empty_left {m : Type u_2} {n : Type u_3} {α : mnType v} [] :
Equations
• =
instance DMatrix.subsingleton_of_empty_right {m : Type u_2} {n : Type u_3} {α : mnType v} [] :
Equations
• =
def AddMonoidHom.mapDMatrix {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddMonoid (α i j)] {β : mnType w} [(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
• = { toFun := fun (M : DMatrix m n α) => M.map fun (i : m) (j : n) => f, map_zero' := , map_add' := }
Instances For
@[simp]
theorem AddMonoidHom.mapDMatrix_apply {m : Type u_2} {n : Type u_3} {α : mnType v} [(i : m) → (j : n) → AddMonoid (α i j)] {β : mnType w} [(i : m) → (j : n) → AddMonoid (β i j)] (f : i : m⦄ → j : n⦄ → α i j →+ β i j) (M : DMatrix m n α) :
= M.map fun (i : m) (j : n) => f