row

Mathlib.Data.Matrix.DMatrix

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

Lean4

/-- `DMatrix.row u` is the row matrix whose entries are given by `u`. -/
def row {α : n → Type v} (v : ∀ j, α j) : DMatrix Unit n fun _i j => α j
  | _x, y => v y

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

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

Разделы

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

Аффилиация

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