equivTensorProduct_apply_mk — Mathlib

English

The inverse of the tensor product equivalence sends a simple tensor to the corresponding scaled generator: (equivTensorProduct S M).symm (Localization.mk r s ⊗ x) = r • mk x s.

Русский

Обратное к эквивалентности тензорного произведения отправляет простой тензор в соответствующий масштабированный генератор: (equivTensorProduct S M).symm (Localization.mk r s ⊗ x) = r • mk x s.

LaTeX

$$$\bigl(\mathrm{equivTensorProduct}\,S\,M\bigr)^{-1}\bigl(\mathrm{Localization.mk}\, r\, s \otimes x\bigr) = r \cdot (\mathrm{mk}\, x\, s)$$$

Lean4

@[simp]
theorem equivTensorProduct_apply_mk (x : M) (s : S) : equivTensorProduct S M (mk x s) = Localization.mk 1 s ⊗ₜ[R] x :=
  by
  apply (equivTensorProduct S M).symm.injective
  simp

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