_example

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#TensorProduct._example

English

For any bilinear f, uncurry f evaluated on m ⊗ n equals f m n.

Русский

Для билинейного f: uncurry f (m ⊗ n) = f m n.

LaTeX

$$$\\mathrm{uncurry\\_apply} (f)\\ (m)\\ (n) = f m n.$$$

Lean4

example : M → N → (M → N → P) → P := fun m => flip fun f => f m

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

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

Разделы

Аффилиация

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