lid — Mathlib

English

The base ring R acts as a left identity for the tensor product with any B; there is a canonical BialgEquiv between R ⊗ B and B (over R).

Русский

Базовое кольцо R выступает левым единичным элементом для тензорного произведения с B; существует каноническая билигебраическая эквивалентность между R ⊗ B и B над R.

LaTeX

$$$\text{lid } : R ⊗[R] B \simeq_{\text{bialg over }R} B$$$

Lean4

/-- The base ring is a left identity for the tensor product of bialgebras, up to
bialgebra equivalence. -/
protected noncomputable def lid : R ⊗[R] B ≃ₐc[R] B :=
  { Coalgebra.TensorProduct.lid R B, Algebra.TensorProduct.lid R B with }

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