cancelBaseChange_symm_tmul — Mathlib

English

The inverse base-change sends a ⊗ b to a ⊗ (1 ⊗ b).

Русский

Обратная отмена базового изменения отправляет a ⊗ b в a ⊗ (1 ⊗ b).

LaTeX

$$$ (\\mathrm{cancelBaseChange}_{R,S,T})^{-1}(a \\otimes b) = a \\otimes (1 \\otimes b) $$$

Lean4

@[simp]
theorem cancelBaseChange_symm_tmul (a : A) (b : B) :
    (Algebra.TensorProduct.cancelBaseChange R S T A B).symm (a ⊗ₜ b) = a ⊗ₜ (1 ⊗ₜ b) :=
  TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul R S T a b

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