lTensor_refl — Mathlib

English

Let R be a commutative semiring and M,N be R-modules. The linear equivalence on M ⊗_R N obtained by applying the identity on N (on the right factor) is the identity on M ⊗_R N.

Русский

Пусть R — коммутативный полукольцо, M и N — модулей над R. Линейное взаимнооднозначное отображение на тензорном произведении M ⊗_R N, полученное из тождества на N (со стороны правого множителя), есть тождественное отображение на M ⊗_R N.

LaTeX

$$$$(\mathrm{id}_N) \\otimes_R \\mathrm{id}_M = \\mathrm{id}_{M \\otimes_R N}.$$$$

Lean4

@[simp]
theorem lTensor_refl : (refl R N).lTensor M = refl R _ :=
  TensorProduct.congr_refl_refl

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