lid_eq_rid — Mathlib

English

For a commutative semiring R, the left-unit and right-unit isomorphisms for the tensor product R ⊗R R coincide; i.e., the canonical left unit map equals the canonical right unit map.

Русский

Для коммутативного полугリングa R тензорные единичные отображения слева и справа для R ⊗R R совпадают; тождественный изоморфизм слева совпадает с изоморфизмом справа.

LaTeX

$$$\\mathrm{lid}_R = \\mathrm{rid}_R.$$$

Lean4

theorem lid_eq_rid : TensorProduct.lid R R = TensorProduct.rid R R :=
  LinearEquiv.toLinearMap_injective <| ext' mul_comm

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