lid_symm_apply

Mathlib.RingTheory.Bialgebra.TensorProduct

URI: https://scilib.ai/kg/mathlib#Bialgebra.TensorProduct.lid_symm_apply

English

The inverse of the left-identity lid sends an element a to 1 ⊗ a.

Русский

Обратное отображение левого идентификатора lid отправляет элемент a в 1 ⊗ a.

LaTeX

$$$\big(\mathrm{lid}_{R,B}\big)^{-1} a = 1 \otimes a$$$

Lean4

@[simp]
theorem lid_symm_apply (a : B) : (Bialgebra.TensorProduct.lid R B).symm a = 1 ⊗ₜ a :=
  rfl

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

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

Разделы

Аффилиация

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