toIsometry_hom_rightUnitor — Mathlib

English

The isometry arising from the right unitor is given by tensorRId: (ρ_ M).hom.toIsometry = (tensorRId _).toIsometry.

Русский

Изометрия правого унитора равна изометрии тензорного правого единичного объекта: (ρ_ M).hom.toIsometry = (tensorRId _).toIsometry.

LaTeX

$$$ (\\rho_ M).hom.toIsometry = (tensorRId _).toIsometry $$$

Lean4

theorem toIsometry_hom_rightUnitor {M : QuadraticModuleCat.{u} R} : (ρ_ M).hom.toIsometry = (tensorRId _).toIsometry :=
  rfl

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