lift_mk

Mathlib.LinearAlgebra.TensorProduct.Basic

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

English

Lift of mk.compr₂ f equals f for any bilinear f.

Русский

Lift от mk.compr₂ f равен f для любого билинейного отображения f.

LaTeX

$$$\\mathrm{lift}(\\mathrm{mk}\\ R\\ M\\ N).compr_2 f = f.$$$

Lean4

theorem lift_mk : lift (mk R M N) = LinearMap.id :=
  Eq.symm <| lift.unique fun _ _ => rfl

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

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

Разделы

Аффилиация

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