mathlib3 documentation

data.matrix.dmatrix

Matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[nolint]
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
Instances for dmatrix
source
theorem dmatrix.ext_iff {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} {M N : dmatrix m n α} :
(∀ (i : m) (j : n), M i j = N i j) ↔ M = N
source
@[ext]
theorem dmatrix.ext {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : 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_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
  • M.map f = λ (i : m) (j : n), f (M i j)
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} :
M.map f i j = f (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} :
(M.map f).map g = M.map (λ (i : m) (j : n) (x : α i j), g (f 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 (λ (j : n) (i : m), α i j)

The transpose of a dmatrix.

Equations
source
def dmatrix.col {m : Type u_2} [fintype m] {α : m → Type v} (w : Π (i : m), α i) :
dmatrix m unit (λ (i : m) (j : unit), α i)

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

Equations
source
def dmatrix.row {n : Type u_3} [fintype n] {α : n → Type v} (v : Π (j : n), α j) :
dmatrix unit n (λ (i : unit) (j : n), α j)

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

Equations
source
@[protected, instance]
def dmatrix.inhabited {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), inhabited (α i j)] :
inhabited (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.has_add {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), has_add (α i j)] :
has_add (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.add_semigroup {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), add_semigroup (α i j)] :
add_semigroup (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.add_comm_semigroup {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), add_comm_semigroup (α i j)] :
add_comm_semigroup (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.has_zero {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), has_zero (α i j)] :
has_zero (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.add_monoid {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), add_monoid (α i j)] :
add_monoid (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.add_comm_monoid {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), add_comm_monoid (α i j)] :
add_comm_monoid (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.has_neg {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), has_neg (α i j)] :
has_neg (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.has_sub {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), has_sub (α i j)] :
has_sub (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.add_group {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), add_group (α i j)] :
add_group (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.add_comm_group {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), add_comm_group (α i j)] :
add_comm_group (dmatrix m n α)
Equations
source
@[protected, instance]
def dmatrix.unique {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
source
@[protected, instance]
def dmatrix.subsingleton {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 α)
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), has_zero (α i j)] (i : m) (j : n) :
0 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), has_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_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), has_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_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), has_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_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), has_zero (α i j)] {β : m → n → Type w} [Π (i : m) (j : n), has_zero (β i j)] {f : Π ⦃i : m⦄ ⦃j : n⦄, α i j → β i j} (h : ∀ (i : m) (j : n), f 0 = 0) :
0.map 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), add_monoid (α i j)] {β : m → n → Type w} [Π (i : m) (j : n), add_monoid (β i j)] (f : Π ⦃i : m⦄ ⦃j : n⦄, α i j →+ β i j) (M N : dmatrix m n α) :
(M + N).map (λ (i : m) (j : n), ⇑f) = M.map (λ (i : m) (j : n), ⇑f) + N.map (λ (i : m) (j : n), ⇑f)
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), add_group (α i j)] {β : m → n → Type w} [Π (i : m) (j : n), add_group (β i j)] (f : Π ⦃i : m⦄ ⦃j : n⦄, α i j →+ β i j) (M N : dmatrix m n α) :
(M - N).map (λ (i : m) (j : n), ⇑f) = M.map (λ (i : m) (j : n), ⇑f) - N.map (λ (i : m) (j : n), ⇑f)
source
@[protected, instance]
def dmatrix.subsingleton_of_empty_left {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [is_empty m] :
subsingleton (dmatrix m n α)
source
@[protected, instance]
def dmatrix.subsingleton_of_empty_right {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [is_empty n] :
subsingleton (dmatrix m n α)
source
def add_monoid_hom.map_dmatrix {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), add_monoid (α i j)] {β : m → n → Type w} [Π (i : m) (j : n), add_monoid (β i j)] (f : Π ⦃i : m⦄ ⦃j : n⦄, α i j →+ β i j) :
dmatrix m n α →+ dmatrix m n β

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

Equations
source
@[simp]
theorem add_monoid_hom.map_dmatrix_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : m → n → Type v} [Π (i : m) (j : n), add_monoid (α i j)] {β : m → n → Type w} [Π (i : m) (j : n), add_monoid (β i j)] (f : Π ⦃i : m⦄ ⦃j : n⦄, α i j →+ β i j) (M : dmatrix m n α) :
⇑(add_monoid_hom.map_dmatrix f) M = M.map (λ (i : m) (j : n), ⇑f)