etaExpand — Mathlib

English

etaExpand expands a finite matrix by placing its entries into a larger block whose outer entries are filled with appropriate zeros (i.e., it expands A to !![A 0 0, ..., A m n]).

Русский

etaExpand разворачивает матрицу в больший блок, заполняя внешние позиции нулями, то есть восстанавливает матрицу из меньшей размерности в представлении Fin.

LaTeX

$$etaExpand {m} {n} (A) : Matrix (Fin m) (Fin n) α → Matrix (Fin m) (Fin n) α$$

Lean4

/-- Expand `A` to `!![A 0 0, ...; ..., A m n]` -/
def etaExpand {m n} (A : Matrix (Fin m) (Fin n) α) : Matrix (Fin m) (Fin n) α :=
  Matrix.of (FinVec.etaExpand fun i => FinVec.etaExpand fun j => A i j)

Похожие утверждения