comm_trans_rid — Mathlib

English

The composite of commutativity with rid equals lid, reflecting the symmetry of left and right unit structures in the tensor product.

Русский

Сложение коммутативности с rid даёт lid, отражая симметрию левой и правой единичности в тензорном произведении.

LaTeX

$$$ TensorProduct.comm R R M \\; ≪≫ₗ \\; TensorProduct.rid R M = TensorProduct.lid R M $$$

Lean4

@[simp]
theorem comm_trans_rid : TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M = TensorProduct.lid R M :=
  LinearEquiv.toLinearMap_injective (ext (by ext; rfl))

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