lid_toLinearEquiv — Mathlib

English

The linear equivalence underlying the lid construction coincides with the standard linear equivalence on the tensor product.

Русский

Линейное эквивалентное отображение, лежащее в основе конструкций lid, совпадает с обычным линейным эквивалентом на тензорном произведении.

LaTeX

$$$(\\mathrm{lid}\\, R\\, A).\\mathrm{toLinearEquiv} = \\mathsf{TensorProduct}.\\mathrm{lid}\\ R\\ A$$$

Lean4

@[simp]
theorem lid_toLinearEquiv : (TensorProduct.lid R A).toLinearEquiv = _root_.TensorProduct.lid R A :=
  rfl

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