lid_tmul

Mathlib.RingTheory.Bialgebra.TensorProduct

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

English

The left-identity equivalence lid coincides with Algebra.TensorProduct.lid at the level of AlgHom.

Русский

Левый идентификатор lid совпадает по смыслу с Algebra.TensorProduct.lid как алгебродомферм.

LaTeX

$$$\text{lid}_{R,B} : R ⊗ B \to_{alg} B = \text{Algebra.TensorProduct.lid } R B$$$

Lean4

@[simp]
theorem lid_tmul (r : R) (a : B) : Bialgebra.TensorProduct.lid R B (r ⊗ₜ a) = r • a :=
  rfl

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

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

Разделы

Аффилиация

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