rid_symm_apply — Mathlib

English

The composition of the commutativity isomorphism with the right-identity equals the left-identity, giving a canonical comparison between left and right unit structures.

Русский

Состав коммутативности и правого идентификатора даёт левый единичный объект и эквивалентную конструкцию.

LaTeX

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

Lean4

@[simp]
theorem rid_symm_apply (m : M) : (TensorProduct.rid R M).symm m = m ⊗ₜ 1 :=
  rfl

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