theorem HexMatrixMathlib.getD_eq_getElem' {α : Type u_1} (l : List α) (i : ℕ) (d : α) (h : i < l.length) : l.getD i d = l[i]

theorem HexMatrixMathlib.getD_eq_default' {α : Type u_1} (l : List α) (i : ℕ) (d : α) (h : l.length ≤ i) : l.getD i d = d

def HexMatrixMathlib.vecOfList {α : Type u_1} [Zero α] (k : ℕ) : List α → Fin k → α

A list as a vector, padded with zeros; vecOfList (k + 1) (a :: l) unfolds to vecCons a (vecOfList k l), so a ![…] literal is definitionally vecOfList of its entries.

Equations

• HexMatrixMathlib.vecOfList 0 x✝ = ![]
• HexMatrixMathlib.vecOfList k.succ (a :: l) = Matrix.vecCons a (HexMatrixMathlib.vecOfList k l)
• HexMatrixMathlib.vecOfList n.succ [] = fun (x : Fin (n + 1)) => 0

def HexMatrixMathlib.ofLists {α : Type u_1} [Zero α] (n m : ℕ) (L : List (List α)) : Matrix (Fin n) (Fin m) α

The Mathlib matrix of a row list, padded with zeros.

Equations

• HexMatrixMathlib.ofLists n m L = Matrix.of (HexMatrixMathlib.vecOfList n (List.map (HexMatrixMathlib.vecOfList m) L))

theorem HexMatrixMathlib.vecOfList_apply {α : Type u_1} [Zero α] (k : ℕ) (l : List α) (i : Fin k) : vecOfList k l i = l.getD (↑i) 0

theorem HexMatrixMathlib.ofLists_apply {α : Type u_1} [Zero α] (n m : ℕ) (L : List (List α)) (i : Fin n) (j : Fin m) : ofLists n m L i j = (L.getD ↑i []).getD (↑j) 0

def HexMatrixMathlib.entriesEq {α : Type u_1} [Zero α] [DecidableEq α] (n m : ℕ) (A : Matrix (Fin n) (Fin m) α) (L : List (List α)) : Bool

The entrywise comparison of a matrix with its row list, as a Boolean the kernel evaluates by enumerating every index pair.

Equations

• HexMatrixMathlib.entriesEq n m A L = (List.finRange n).all fun (i : Fin n) => (List.finRange m).all fun (j : Fin m) => decide (A i j = HexMatrixMathlib.ofLists n m L i j)

theorem HexMatrixMathlib.eq_ofLists_of_entriesEq {α : Type u_1} [Zero α] [DecidableEq α] (n m : ℕ) (A : Matrix (Fin n) (Fin m) α) (L : List (List α)) (h : entriesEq n m A L = true) : A = ofLists n m L

A passing entrywise comparison identifies the matrix with its row list.

structure HexMatrixMathlib.Certified {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : Type u_2

The record returned by the result-producing term forms (det% A): the value of f a and the proof.

• value : β

  The computed value.

• proof : f a = self.value

  The certificate that it is f a.

inductive HexMatrixMathlib.Literal.Route : Type

How a recognized literal is identified with its row list.

• chain : Route

  A Matrix.of vector chain (!![…], Matrix.of ![…]): A = ofLists n m L is rfl.

• entrywise : Route

  A fun i j => … or Matrix.ofArray xs h literal: A = ofLists n m L by one kernel decide on entriesEq.

@[instance_reducible]

instance HexMatrixMathlib.Literal.instReprRoute : Repr Route

Equations

• HexMatrixMathlib.Literal.instReprRoute = { reprPrec := HexMatrixMathlib.Literal.instReprRoute.repr }

def HexMatrixMathlib.Literal.instReprRoute.repr : Route → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HexMatrixMathlib.Literal.instDecidableEqRoute : DecidableEq Route

Equations

• HexMatrixMathlib.Literal.instDecidableEqRoute x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure HexMatrixMathlib.Literal.Recognized : Type

A recognized closed matrix literal.

• n : ℕ

  Rows.

• m : ℕ

  Columns.

• carrier : Lean.Expr

  The entry carrier.

• entries : Array (Array Lean.Expr)

  The entry expressions, row-major, as they appear in the literal (or, for the fun and ofArray forms, as instantiated at each index pair).

• route : Route

  The identification route.

def HexMatrixMathlib.Literal.unfoldBudget : ℕ

How many definitions are unfolded when looking for a literal.

Equations

• HexMatrixMathlib.Literal.unfoldBudget = 8

def HexMatrixMathlib.Literal.shape? (ty : Lean.Expr) : Lean.MetaM (Option (ℕ × ℕ × Lean.Expr))

The shape of the type Matrix (Fin n) (Fin m) R with closed dimensions: (n, m, R), or of the function type Fin n → Fin m → R a bare lambda has. The dimensions may be any closed expressions that evaluate to numerals, as Matrix.of ![…] elaborates them as Nat.succ chains.

Equations

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

def HexMatrixMathlib.Literal.matchChain? (n m : ℕ) (A : Lean.Expr) : Lean.MetaM (Option (Array (Array Lean.Expr)))

Match a Matrix.of ![…] chain (the !![…] notation included) of the given shape. Like Mathlib's matchMatrixLit?, but every vecCons chain must end in vecEmpty, so that the literal is definitionally the ofLists of its entries.

Equations

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

def HexMatrixMathlib.Literal.finLit (n k : ℕ) : Lean.MetaM Lean.Expr

⟨k, _⟩ : Fin n.

Equations

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

def HexMatrixMathlib.Literal.matchFn? (n m : ℕ) (A : Lean.Expr) : Lean.MetaM (Option (Array (Array Lean.Expr)))

Match a fun i j => … literal: the body instantiated at every index pair.

Equations

• One or more equations did not get rendered due to their size.
• HexMatrixMathlib.Literal.matchFn? n m A = pure none

def HexMatrixMathlib.Literal.matchOfArray? (n m : ℕ) (A : Lean.Expr) : Lean.MetaM (Option (Array (Array Lean.Expr)))

Match a Matrix.ofArray xs h literal whose array is a #[…] literal of n * m entries.

Equations

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

partial def HexMatrixMathlib.Literal.matchLiteral? (n m : ℕ) (R A : Lean.Expr) (budget : ℕ := unfoldBudget) : Lean.MetaM (Option Recognized)

Find the literal behind A : Matrix (Fin n) (Fin m) R, unfolding definitions within unfoldBudget; an open term is not a literal.

def HexMatrixMathlib.Literal.literal? (A : Lean.Expr) : Lean.MetaM (Option Recognized)

Recognize a closed matrix literal from its type and its expression.

Equations

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

def HexMatrixMathlib.Literal.evalEntry (e : Lean.Expr) : Lean.MetaM ℚ

Evaluate an entry to a rational with norm_num; an entry norm_num alone does not evaluate (the fun i j => … form instantiates its body at Fin literals, leaving Fin.val, casts and if i = j tests) is first simplified with the default simp set. An entry that is not a closed numeric expression is an error naming it.

Equations

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

def HexMatrixMathlib.Literal.evalEntries (lit : Recognized) : Lean.MetaM (Array (Array ℚ))

Evaluate every entry to a rational.

Equations

• HexMatrixMathlib.Literal.evalEntries lit = Array.mapM (fun (x : Array Lean.Expr) => Array.mapM HexMatrixMathlib.Literal.evalEntry x) lit.entries

def HexMatrixMathlib.Literal.rowList (type : Lean.Expr) (rows : Array (Array Lean.Expr)) : Lean.MetaM Lean.Expr

The row list of quoted entries, as a List (List type).

Equations

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

def HexMatrixMathlib.Literal.decideProof (prop : Lean.Expr) : Lean.MetaM Lean.Expr

of_decide_eq_true on a closed decidable proposition, for the kernel to evaluate; no elaborator-side evaluation happens.

Equations

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

def HexMatrixMathlib.Literal.identification (lit : Recognized) (A L : Lean.Expr) : Lean.MetaM Lean.Expr

The proof of A = ofLists n m L along the literal's route: rfl for a vector chain, one kernel decide on entriesEq otherwise.

Equations

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

def HexMatrixMathlib.Literal.elabArgument (t : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

Elaborate a matrix argument of a term form. The !![…] notations are given an integer entry expectation so their numerals do not default to Nat.

Equations

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