comm_trans_lid — Mathlib

English

The same relationship holds for the transitive composition in the other direction: comm followed by rid equals lid.

Русский

Та же связь сохраняется и в обратном направлении: comm затем rid равняется lid.

LaTeX

$$$ (TensorProduct.comm R R M).trans (TensorProduct.rid R M) = TensorProduct.lid R M $$$

Lean4

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

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