tensorProduct_isLocalizedModule — Mathlib

English

The inverse tensor-product equivalence sends 1 ⊗ x to mk x 1.

Русский

Обратное к эквивалентности тензорного произведения отправляет 1 ⊗ x в mk x 1.

LaTeX

$$$(\mathrm{equivTensorProduct}\,S\,M)^{-1}(1 \otimes x) = \mathrm{mk}\, x\, 1$$$

Lean4

instance tensorProduct_isLocalizedModule : IsLocalizedModule S (TensorProduct.mk R A M 1) :=
  (isLocalizedModule_iff_isBaseChange _ A _).mpr (TensorProduct.isBaseChange _ _ _)

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