toIsometry_hom_leftUnitor — Mathlib

English

Let M be any quadratic module. The isometry coming from the left unitor is equal to the left tensor unit isometry: (λ_ M).hom.toIsometry = (tensorLId _).toIsometry.

Русский

Пусть M — квадратичный модуль. Изометрия левого унитора равна изометрии левого тензорного единичного объекта: (λ_ M).hom.toIsometry = (tensorLId _).toIsometry.

LaTeX

$$$ (\lambda_ M).hom.toIsometry = (tensorLId _).toIsometry $$$

Lean4

theorem toIsometry_hom_leftUnitor {M : QuadraticModuleCat.{u} R} : (λ_ M).hom.toIsometry = (tensorLId _).toIsometry :=
  rfl

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