productMap_left_apply

Mathlib.RingTheory.TensorProduct.Basic

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

English

The product map evaluated at a ⊗ 1 equals f(a).

Русский

Значение productMap на a ⊗ 1 равно f(a).

LaTeX

$$productMap f g (a ⊗ 1) = f(a)$$

Lean4

theorem productMap_left_apply (a : A) : productMap f g (a ⊗ₜ 1) = f a := by simp

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

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

Разделы

Аффилиация

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