productMap_apply_tmul

Mathlib.RingTheory.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.TensorProduct.productMap_apply_tmul

English

On a simple tensor a ⊗ b, the product map sends it to f(a) g(b).

Русский

На простом тензоре a ⊗ b отображение продукта отправляет в f(a) g(b).

LaTeX

$$productMap f g (a \otimes b) = f(a) \cdot g(b)$$

Lean4

@[simp]
theorem productMap_apply_tmul (a : A) (b : B) : productMap f g (a ⊗ₜ b) = f a * g b :=
  rfl

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

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

Разделы

Аффилиация

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