equiv — Mathlib

English

If f defines a tensor product, there exists a linear equivalence h.equiv: M1 ⊗ M2 ≃ M.

Русский

Если f задаёт тензорное произведение, существует линейное эквивалентное отображение h.equiv: M1 ⊗ M2 ≃ M.

LaTeX

$$IsTensorProduct.equiv$$

Lean4

/-- If `M` is the tensor product of `M₁` and `M₂`, it is linearly equivalent to `M₁ ⊗[R] M₂`. -/
@[simps! apply]
noncomputable def equiv (h : IsTensorProduct f) : M₁ ⊗[R] M₂ ≃ₗ[R] M :=
  LinearEquiv.ofBijective _ h

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