auxEquiv_tmul — Mathlib

English

For basic tensors a ᵍ⊗ₜ b, the auxiliary equivalence maps it to the tensor product of their decompositions: auxEquiv R 𝒜 ℬ (a ᵍ⊗ₜ b) = decompose 𝒜 a ⊗ₜ decompose ℬ b.

Русский

Для базового тензора a ᵍ⊗ₜ b отображение-эквивалент auxEquiv переводит его в тензор произведение разложенных элементов: auxEquiv R 𝒜 ℬ (a ᵍ⊗ₜ b) = decompose 𝒜 a ⊗ₜ decompose ℬ b.

LaTeX

$$$\operatorname{auxEquiv}_R(𝒜,ℬ)(a \ ᵍ⊗ₜ b) = \operatorname{decompose}_{𝒜}(a) \otimes_⎯ b$$$

Lean4

theorem auxEquiv_tmul (a : A) (b : B) : auxEquiv R 𝒜 ℬ (a ᵍ⊗ₜb) = decompose 𝒜 a ⊗ₜ decompose ℬ b :=
  rfl

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