toIsometry_inv_rightUnitor — Mathlib

English

The inverse right unitor yields the inverse tensor right isometry: (ρ_ M).inv.toIsometry = (tensorRId _).symm.toIsometry.

Русский

Обратная изометрия правого унитора равна обратной изометрии: (ρ_ M).inv.toIsometry = (tensorRId _).symm.toIsometry.

LaTeX

$$$ (\\rho_ M).inv.toIsometry = (tensorRId _).symm.toIsometry $$$

Lean4

theorem toIsometry_inv_rightUnitor {M : QuadraticModuleCat.{u} R} :
    (ρ_ M).inv.toIsometry = (tensorRId _).symm.toIsometry :=
  rfl

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