uncurry_apply — Mathlib

English

Applying the equivalence lift.equiv to a bilinear map f returns the corresponding map on tensors evaluated at a simple tensor.

Русский

Применение эквивалентности lift.equiv к билинейному отображению f возвращает соответствующее отображение на тензоре и вычисление на простом тензоре.

LaTeX

$$$\\mathrm{lift\\,equiv}\\ f\\ (m ⊗ n) = f\\,m\\,n.$$$

Lean4

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

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