DMatrix

Mathlib.Data.Matrix.DMatrix

URI: https://scilib.ai/kg/mathlib#DMatrix

Lean4

/-- `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. -/
def DMatrix (m : Type u) (n : Type u') (α : m → n → Type v) : Type max u u' v :=
  ∀ i j, α i j

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru