Documentation

Mathlib.Data.Matrix.DMatrix

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)] :
              Add (DMatrix m n α)
              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)] :
              AddGroup (DMatrix m n α)
              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) :
              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} [IsEmpty m] :
              Equations
              • =
              instance DMatrix.subsingleton_of_empty_right {m : Type u_2} {n : Type u_3} {α : mnType v} [IsEmpty n] :
              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
              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 α) :
                (AddMonoidHom.mapDMatrix f) M = M.map fun (i : m) (j : n) => f