rid_tmul

Mathlib.RingTheory.Bialgebra.TensorProduct

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

English

The right-identity rid coincides with Algebra.TensorProduct.rid as an AlgEquiv.

Русский

rid совпадает с Algebra.TensorProduct.rid как алгебра-эквив.

LaTeX

$$$\text{rid}_{R,S,A} = \text{Algebra.TensorProduct.rid } R S A$$$

Lean4

@[simp]
theorem rid_tmul (r : R) (a : A) : Bialgebra.TensorProduct.rid R S A (a ⊗ₜ r) = r • a :=
  rfl

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

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

Разделы

Аффилиация

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