includeRight_apply

Mathlib.RingTheory.TensorProduct.Basic

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

English

For every b in B, includeRight(b) = 1 ⊗ b.

Русский

Для каждого b в B includeRight(b) = 1 ⊗ b.

LaTeX

$$$i_R(b)=1\otimes b\quad(b\in B).$$$

Lean4

@[simp]
theorem includeRight_apply (b : B) : (includeRight : B →ₐ[R] A ⊗[R] B) b = 1 ⊗ₜ b :=
  rfl

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

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

Разделы

Аффилиация

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