lift_compr₂

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#TensorProduct.lift_compr₂

English

Applying uncurry to f and two inputs m,n yields f m n.

Русский

Применение uncurry к f и двум входам m,n даёт f m n.

LaTeX

$$$\\mathrm{uncurry}\\ R\\ M\\ N\\ P\\ f (m \\otimes_R n) = f m n.$$$

Lean4

theorem lift_compr₂ (g : P →ₗ[R] Q) : lift (f.compr₂ g) = g.comp (lift f) :=
  Eq.symm <| lift.unique fun _ _ => by simp

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

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

Разделы

Аффилиация

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