hom_inv_rightUnitor — Mathlib

English

The inverse of the right unitor has hom component equal to rid_symm: (ρ_M).inv.hom = (TensorProduct.rid _ _).symm.toLinearMap.

Русский

Обратное к правому унитору имеет гом-компоненту rid_symm: (ρ_M).inv.hom = (TensorProduct.rid _ _).symm.toLinearMap.

LaTeX

$$$ (\\rho_M).inv.hom = (\\text{TensorProduct}.rid \\; R \\; M)^{\\mathrm{symm}}^{\\;toLinearMap} $$$

Lean4

theorem hom_inv_rightUnitor {M : ModuleCat.{u} R} : (ρ_ M).inv.hom = (TensorProduct.rid _ _).symm.toLinearMap :=
  rfl

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