toIsometry_inv_leftUnitor — Mathlib

English

For any M, the inverse of the left unitor induces the inverse left tensor isometry: (λ_ M).inv.toIsometry = (tensorLId _).symm.toIsometry.

Русский

Для любого M обратная левого унитора задаёт обратную изометрии тензорной единицы: (λ_ M).inv.toIsometry = (tensorLId _).symm.toIsometry.

LaTeX

$$$ (\lambda_ M).inv.toIsometry = (tensorLId _).symm.toIsometry $$$

Lean4

theorem toIsometry_inv_leftUnitor {M : QuadraticModuleCat.{u} R} :
    (λ_ M).inv.toIsometry = (tensorLId _).symm.toIsometry :=
  rfl

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