tmul — Mathlib

English

If a₁ semiconjugates to a₃ by a₂, and b₁ semiconjugates to b₃ by b₂, then a₁ ⊗ b₁ semiconjugates to a₃ ⊗ b₃ by a₂ ⊗ b₂.

Русский

Если a₁ полусопряжён к a₃ через a₂, а b₁ — через b₂, то тензор a₁ ⊗ b₁ полусопряжён к a₃ ⊗ b₃ через a₂ ⊗ b₂.

LaTeX

$$$ \text{SemiconjBy } a_1 a_2 a_3 \rightarrow \text{SemiconjBy } b_1 b_2 b_3 \Rightarrow \text{SemiconjBy } (a_1 \otimes_R b_1) (a_2 \otimes_R b_2) (a_3 \otimes_R b_3) $$$

Lean4

theorem _root_.SemiconjBy.tmul {a₁ a₂ a₃ : A} {b₁ b₂ b₃ : B} (ha : SemiconjBy a₁ a₂ a₃) (hb : SemiconjBy b₁ b₂ b₃) :
    SemiconjBy (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃) :=
  congr_arg₂ (· ⊗ₜ[R] ·) ha.eq hb.eq

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