Dependent-typed matrices #

def DMatrix (m : Type u) (n : Type u') (α : m → n → Type 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

source

theorem DMatrix.ext_iff {m : Type u_1} {n : Type u_2} {α : m → n → Type v} {M N : DMatrix m n α} :

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

source

theorem DMatrix.ext {m : Type u_1} {n : Type u_2} {α : m → n → Type v} {M N : DMatrix m n α} :

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

source

def DMatrix.map {m : Type u_1} {n : Type u_2} {α : m → n → Type v} (M : DMatrix m n α) {β : m → n → Type 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)

source

@[simp]

theorem DMatrix.map_apply {m : Type u_1} {n : Type u_2} {α : m → n → Type v} {M : DMatrix m n α} {β : m → n → Type w} {f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j} {i : m} {j : n} :

M.map f i j = f (M i j)

source

@[simp]

theorem DMatrix.map_map {m : Type u_1} {n : Type u_2} {α : m → n → Type v} {M : DMatrix m n α} {β : m → n → Type w} {γ : m → n → Type 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 (x : m) (x_1 : n) (x_2 : α x x_1) => g (f x_2)

source

def DMatrix.transpose {m : Type u_1} {n : Type u_2} {α : m → n → Type 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 = M x x✝

source

def DMatrix.«term_ᵀ» :

Lean.TrailingParserDescr

The transpose of a dmatrix.

Equations

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

source

def DMatrix.col {m : Type u_1} {α : m → Type 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

DMatrix.col w x✝ x = w x✝

source

def DMatrix.row {n : Type u_2} {α : n → Type 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

DMatrix.row v x✝ x = v x

source

instance DMatrix.instInhabited {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Inhabited (α i j)] :

Inhabited (DMatrix m n α)

Equations

DMatrix.instInhabited = inferInstanceAs (Inhabited ((i : m) → (j : n) → α i j))

source

instance DMatrix.instAdd {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Add (α i j)] :

Add (DMatrix m n α)

Equations

DMatrix.instAdd = inferInstanceAs (Add ((i : m) → (j : n) → α i j))

source

instance DMatrix.instAddSemigroup {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddSemigroup (α i j)] :

AddSemigroup (DMatrix m n α)

Equations

DMatrix.instAddSemigroup = inferInstanceAs (AddSemigroup ((i : m) → (j : n) → α i j))

source

instance DMatrix.instAddCommSemigroup {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddCommSemigroup (α i j)] :

AddCommSemigroup (DMatrix m n α)

Equations

DMatrix.instAddCommSemigroup = inferInstanceAs (AddCommSemigroup ((i : m) → (j : n) → α i j))

source

instance DMatrix.instZero {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Zero (α i j)] :

Zero (DMatrix m n α)

Equations

DMatrix.instZero = inferInstanceAs (Zero ((i : m) → (j : n) → α i j))

source

instance DMatrix.instAddMonoid {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddMonoid (α i j)] :

AddMonoid (DMatrix m n α)

Equations

DMatrix.instAddMonoid = inferInstanceAs (AddMonoid ((i : m) → (j : n) → α i j))

source

instance DMatrix.instAddCommMonoid {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddCommMonoid (α i j)] :

AddCommMonoid (DMatrix m n α)

Equations

DMatrix.instAddCommMonoid = inferInstanceAs (AddCommMonoid ((i : m) → (j : n) → α i j))

source

instance DMatrix.instNeg {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Neg (α i j)] :

Neg (DMatrix m n α)

Equations

DMatrix.instNeg = inferInstanceAs (Neg ((i : m) → (j : n) → α i j))

source

instance DMatrix.instSub {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Sub (α i j)] :

Sub (DMatrix m n α)

Equations

DMatrix.instSub = inferInstanceAs (Sub ((i : m) → (j : n) → α i j))

source

instance DMatrix.instAddGroup {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddGroup (α i j)] :

AddGroup (DMatrix m n α)

Equations

DMatrix.instAddGroup = inferInstanceAs (AddGroup ((i : m) → (j : n) → α i j))

source

instance DMatrix.instAddCommGroup {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddCommGroup (α i j)] :

AddCommGroup (DMatrix m n α)

Equations

DMatrix.instAddCommGroup = inferInstanceAs (AddCommGroup ((i : m) → (j : n) → α i j))

source

instance DMatrix.instUnique {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Unique (α i j)] :

Unique (DMatrix m n α)

Equations

DMatrix.instUnique = inferInstanceAs (Unique ((i : m) → (j : n) → α i j))

source

instance DMatrix.instSubsingleton {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [∀ (i : m) (j : n), Subsingleton (α i j)] :

Subsingleton (DMatrix m n α)

Equations

⋯ = ⋯

source

@[simp]

theorem DMatrix.zero_apply {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Zero (α i j)] (i : m) (j : n) :

0 i j = 0

source

@[simp]

theorem DMatrix.neg_apply {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Neg (α i j)] (M : DMatrix m n α) (i : m) (j : n) :

(-M) i j = -M i j

source

@[simp]

theorem DMatrix.add_apply {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Add (α i j)] (M N : DMatrix m n α) (i : m) (j : n) :

(M + N) i j = M i j + N i j

source

@[simp]

theorem DMatrix.sub_apply {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Sub (α i j)] (M N : DMatrix m n α) (i : m) (j : n) :

(M - N) i j = M i j - N i j

source

@[simp]

theorem DMatrix.map_zero {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → Zero (α i j)] {β : m → n → Type 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) :

DMatrix.map 0 f = 0

source

theorem DMatrix.map_add {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddMonoid (α i j)] {β : m → n → Type w} [(i : m) → (j : n) → AddMonoid (β i j)] (f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j) (M 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

source

theorem DMatrix.map_sub {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddGroup (α i j)] {β : m → n → Type w} [(i : m) → (j : n) → AddGroup (β i j)] (f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j) (M 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

source

instance DMatrix.subsingleton_of_empty_left {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [IsEmpty m] :

Subsingleton (DMatrix m n α)

Equations

⋯ = ⋯

source

instance DMatrix.subsingleton_of_empty_right {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [IsEmpty n] :

Subsingleton (DMatrix m n α)

Equations

⋯ = ⋯

source

def AddMonoidHom.mapDMatrix {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddMonoid (α i j)] {β : m → n → Type 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

AddMonoidHom.mapDMatrix f = { toFun := fun (M : DMatrix m n α) => M.map fun (i : m) (j : n) => ⇑f, map_zero' := ⋯, map_add' := ⋯ }

source

@[simp]

theorem AddMonoidHom.mapDMatrix_apply {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [(i : m) → (j : n) → AddMonoid (α i j)] {β : m → n → Type w} [(i : m) → (j : n) → AddMonoid (β i j)] (f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j) (M : DMatrix m n α) :

(AddMonoidHom.mapDMatrix f) M = M.map fun (i : m) (j : n) => ⇑f

Documentation

Mathlib.Data.Matrix.DMatrix

Dependent-typed matrices #