Matrices #

def DMatrix (m : Type u) (n : Type u') [Fintype m] [Fintype n] (α : 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 fintype m and whose columns are indexed by the fintype n.

Equations

DMatrix m n α = ((i : m) → (j : n) → α i j)

Instances For

source

theorem DMatrix.ext_iff {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : m → n → Type v} {M : DMatrix m n α} {N : DMatrix m n α} :

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

source

theorem DMatrix.ext {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : m → n → Type v} {M : DMatrix m n α} {N : DMatrix m n α} :

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

source

def DMatrix.map {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : 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

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

Instances For

source

@[simp]

theorem DMatrix.map_apply {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : 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} :

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

source

@[simp]

theorem DMatrix.map_map {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : 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} :

DMatrix.map (DMatrix.map M f) g = DMatrix.map M fun i j x => g i j (f i j x)

source

def DMatrix.transpose {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : m → n → Type v} (M : DMatrix m n α) :

DMatrix n m fun j i => α i j

The transpose of a dmatrix.

Equations

DMatrix.transpose M x x = match x, x with | x, y => M y x

Instances For

source

def DMatrix.«term_ᵀ» :

Lean.TrailingParserDescr

The transpose of a dmatrix.

Equations

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

Instances For

source

def DMatrix.col {m : Type u_2} [Fintype m] {α : m → Type 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

DMatrix.col w x x = match x, x with | x, _y => w x

Instances For

source

def DMatrix.row {n : Type u_3} [Fintype n] {α : n → Type 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

DMatrix.row v x x = match x, x with | _x, y => v y

Instances For

source

instance DMatrix.instInhabitedDMatrix {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : m → n → Type v} [inst : (i : m) → (j : n) → Inhabited (α i j)] :

Inhabited (DMatrix m n α)

Equations

DMatrix.instInhabitedDMatrix = { default := fun i j => default }

source

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

Add (DMatrix m n α)

Equations

DMatrix.instAddDMatrix = Pi.instAdd

source

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

AddSemigroup (DMatrix m n α)

Equations

DMatrix.instAddSemigroupDMatrix = Pi.addSemigroup

source

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

AddCommSemigroup (DMatrix m n α)

Equations

DMatrix.instAddCommSemigroupDMatrix = Pi.addCommSemigroup

source

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

Zero (DMatrix m n α)

Equations

DMatrix.instZeroDMatrix = Pi.instZero

source

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

AddMonoid (DMatrix m n α)

Equations

DMatrix.instAddMonoidDMatrix = Pi.addMonoid

source

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

AddCommMonoid (DMatrix m n α)

Equations

DMatrix.instAddCommMonoidDMatrix = Pi.addCommMonoid

source

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

Neg (DMatrix m n α)

Equations

DMatrix.instNegDMatrix = Pi.instNeg

source

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

Sub (DMatrix m n α)

Equations

DMatrix.instSubDMatrix = Pi.instSub

source

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

AddGroup (DMatrix m n α)

Equations

DMatrix.instAddGroupDMatrix = Pi.addGroup

source

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

AddCommGroup (DMatrix m n α)

Equations

DMatrix.instAddCommGroupDMatrix = Pi.addCommGroup

source

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

Unique (DMatrix m n α)

Equations

DMatrix.instUniqueDMatrix = Pi.unique

source

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

Subsingleton (DMatrix m n α)

Equations

@DMatrix.instSubsingletonDMatrix = @DMatrix.instSubsingletonDMatrix.proof_1

source

@[simp]

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

OfNat.ofNat (DMatrix m n α) 0 Zero.toOfNat0 i j = 0

source

@[simp]

theorem DMatrix.neg_apply {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : m → n → Type v} [(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

source

@[simp]

theorem DMatrix.add_apply {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : m → n → Type v} [(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

source

@[simp]

theorem DMatrix.sub_apply {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : m → n → Type v} [(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

source

@[simp]

theorem DMatrix.map_zero {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : 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 i j 0 = 0) :

DMatrix.map 0 f = 0

source

theorem DMatrix.map_add {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : 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 α) (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)

source

theorem DMatrix.map_sub {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : 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 : 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)

source

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

Subsingleton (DMatrix m n α)

Equations

@DMatrix.subsingleton_of_empty_left = @DMatrix.subsingleton_of_empty_left.proof_1

source

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

Subsingleton (DMatrix m n α)

Equations

@DMatrix.subsingleton_of_empty_right = @DMatrix.subsingleton_of_empty_right.proof_1

source

def AddMonoidHom.mapDMatrix {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : 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

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem AddMonoidHom.mapDMatrix_apply {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] {α : 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 = DMatrix.map M fun i j => ↑(f i j)