val_mulMap'_tmul

Mathlib.LinearAlgebra.TensorProduct.Subalgebra

URI: https://scilib.ai/kg/mathlib#Subalgebra.val_mulMap'_tmul

English

For a ∈ A and b ∈ B, the value of mulMap' on a ⊗ b, seen in S, equals a·b.

Русский

Для a ∈ A и b ∈ B значение mulMap' на a ⊗ b, как элемент S, равно a·b.

LaTeX

$$$(mulMap' A B (a \otimes b) : S) = a.1 \cdot b.1$$$

Lean4

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

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

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

Разделы

Аффилиация

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