Documentation

Mathlib.Tactic.Matrix.OfLists

Matrices from lists of rows #

ofLists reads a list of rows as a Matrix, and the results here transport the list operations to the matrix ones.

Main results #

Implementation notes #

The definitions recurse on the dimensions, so on literals they reduce in the kernel to the vecCons form of the !![…] notation, and a literal in that notation is definitionally an ofLists term.

source
def Mathlib.Tactic.Matrix.ofList {α : Type u_1} [Zero α] (n : ℕ) :
List α → Fin n → α

Construct a vector from the first n elements of a list, padded with 0.

Equations
Instances For
    source
    @[simp]
    theorem Mathlib.Tactic.Matrix.ofList_apply {α : Type u_1} [Zero α] (n : ℕ) (l : List α) (i : Fin n) :
    ofList n l i = l.getD (↑i) 0
    source
    def Mathlib.Tactic.Matrix.ofListsFun {α : Type u_1} [Zero α] (m n : ℕ) :
    List (List α) → Fin m → Fin n → α

    The first n elements of the first m lists as a function of two indices, padded with 0.

    Equations
    Instances For
      source
      def Mathlib.Tactic.Matrix.ofLists {α : Type u_1} [Zero α] (m n : ℕ) (rows : List (List α)) :
      Matrix (Fin m) (Fin n) α

      Construct a matrix from the first n elements of the first m lists, padded with 0.

      Equations
      Instances For
        source
        @[simp]
        theorem Mathlib.Tactic.Matrix.ofLists_apply {α : Type u_1} [Zero α] (m n : ℕ) (rows : List (List α)) (i : Fin m) :
        ofLists m n rows i = ofList n (rows.getD ↑i [])
        source
        @[simp]
        theorem Mathlib.Tactic.Matrix.ListMatrix.dotProduct_eq {α : Type u_1} [Mul α] [AddCommMonoid α] (n : ℕ) (l₁ l₂ : List α) :
        dotProduct n l₁ l₂ = ofList n l₁ ⬝ᵥ ofList n l₂
        source
        @[simp]
        theorem Mathlib.Tactic.Matrix.ofLists_transpose {α : Type u_1} [Zero α] (m n : ℕ) (rows : List (List α)) :
        ofLists n m (ListMatrix.transpose n rows) = (ofLists m n rows).transpose
        source
        theorem Mathlib.Tactic.Matrix.ofLists_mul {α : Type u_1} [Mul α] [AddCommMonoid α] {l m n : ℕ} {A B C : List (List α)} (h : ListMatrix.mul l m n A B = C) :
        ofLists l m A * ofLists m n B = ofLists l n C