vec_of

Mathlib.LinearAlgebra.Matrix.Vec

URI: https://scilib.ai/kg/mathlib#Matrix.vec_of

English

For any function f: m × n → R, vec(of f) equals uncurry (flip f).

Русский

Для любой функции f: m×n → R, vec(мatrix из f) равен uncurry (flip f).

LaTeX

$$$\mathrm{vec}(\mathrm{of} \, f) = \mathrm{Function.uncurry} (\mathrm{flip} \, f)$$$

Lean4

@[simp]
theorem vec_of (f : m → n → R) : vec (of f) = Function.uncurry (flip f) :=
  rfl

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

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

Разделы

Аффилиация

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