lift_apply

Mathlib.Algebra.Lie.TensorProduct

URI: https://scilib.ai/kg/mathlib#TensorProduct.LieModule.lift_apply

English

The lift map on a pure tensor acts by evaluating the bilinear map: lift(f)(m ⊗ n) = f(m)(n).

Русский

Отображение подъема на чистом тензоре действует по формуле: lift(f)(m ⊗ n) = f(m)(n).

LaTeX

$$$\mathrm{lift}\,R\,L\,M\,N\,P\,f\,(m\otimes n) = f(m)(n).$$$

Lean4

@[simp]
theorem lift_apply (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) : lift R L M N P f (m ⊗ₜ n) = f m n :=
  rfl

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

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

Разделы

Аффилиация

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