mulMap_tmul

Mathlib.LinearAlgebra.TensorProduct.Subalgebra

URI: https://scilib.ai/kg/mathlib#Subalgebra.mulMap_tmul

English

For a ∈ A and b ∈ B, mulMap A B applied to a ⊗ b equals the product a.1 * b.1 in S.

Русский

Для a ∈ A и b ∈ B, mulMap A B, применяемый к a ⊗ b, равно произведению a.1 · b.1 в S.

LaTeX

$$$\text{mulMap } A B (a \otimes_R b) = a.1 \cdot b.1$$$

Lean4

@[simp]
theorem mulMap_tmul (a : A) (b : B) : mulMap A B (a ⊗ₜ[R] b) = a.1 * b.1 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru