finsuppProdLEquiv_symm_apply_apply

English

The inverse of finsuppProdLEquiv maps a bilinear function f back to its two-argument form by evaluating at the pair (xy).

Русский

Обратное к finsuppProdLEquiv отображает двувариантную функцию f обратно к форме двух аргументов, оценивая на паре (x,y).

LaTeX

$$$$ (finsuppProdLEquiv R)^{-1} f (x,y) = f \;x\; y. $$$$

Lean4

theorem finsuppProdLEquiv_symm_apply_apply (f : α →₀ β →₀ M) (xy) : (finsuppProdLEquiv R).symm f xy = f xy.1 xy.2 :=
  rfl

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