Dependent-typed matrices #
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.
Instances For
@[simp]
The transpose of a dmatrix.
Equations
- DMatrix.«term_ᵀ» = Lean.ParserDescr.trailingNode `DMatrix.«term_ᵀ» 1024 1024 (Lean.ParserDescr.symbol "ᵀ")
Instances For
DMatrix.col u
is the column matrix whose entries are given by u
.
Equations
- DMatrix.col w x✝¹ x✝ = w x✝¹
Instances For
DMatrix.row u
is the row matrix whose entries are given by u
.
Equations
- DMatrix.row v x✝¹ x✝ = v x✝
Instances For
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))
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))
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))
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))
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 α)
instance
DMatrix.subsingleton_of_empty_left
{m : Type u_1}
{n : Type u_2}
{α : m → n → Type v}
[IsEmpty m]
:
Subsingleton (DMatrix m n α)
instance
DMatrix.subsingleton_of_empty_right
{m : Type u_1}
{n : Type u_2}
{α : m → n → Type v}
[IsEmpty n]
:
Subsingleton (DMatrix m n α)
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)
:
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' := ⋯ }
Instances For
@[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