lid_toAlgEquiv — Mathlib

English

The left-identity equivalence lid agrees with Algebra.TensorProduct.lid when viewed as an algebra equivalence.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem lid_toAlgEquiv : (Bialgebra.TensorProduct.lid R B : R ⊗[R] B ≃ₐ[R] B) = Algebra.TensorProduct.lid R B :=
  rfl

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