isTensorProduct — Mathlib

English

The canonical tensor product construction TensorProduct.mk R M N satisfies the IsTensorProduct property.

Русский

Каноническая конструкция тензорного произведения TensorProduct.mk R M N удовлетворяет свойству IsTensorProduct.

LaTeX

$$IsTensorProduct (TensorProduct.mk R M N)$$

Lean4

theorem isTensorProduct : IsTensorProduct (TensorProduct.mk R M N) :=
  by
  delta IsTensorProduct
  convert_to Function.Bijective (LinearMap.id : M ⊗[R] N →ₗ[R] M ⊗[R] N) using 2
  · apply TensorProduct.ext'
    simp
  · exact Function.bijective_id

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