equiv — Mathlib

English

For a given uncurry, uncurry_apply shows the expected equality on simple tensors.

Русский

Для заданного uncurry, uncurry_apply демонстрирует ожидаемое равенство на простых тензорах.

LaTeX

$$$\\uncurry\\ R\\ M\\ N\\ P\\ f\\ (m ⊗_R n) = f m n.$$$

Lean4

/-- A linear equivalence constructing a linear map `M ⊗ N → P` given a bilinear map `M → N → P`
with the property that its composition with the canonical bilinear map `M → N → M ⊗ N` is
the given bilinear map `M → N → P`. -/
def equiv : (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] M ⊗[R] N →ₗ[R] P :=
  { uncurry R M N P with invFun := fun f => (mk R M N).compr₂ f }

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