toIsometry_comp

Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat

URI: https://scilib.ai/kg/mathlib#QuadraticModuleCat.toIsometry_comp

← MathLib Explorer

English

The toIsometry of identity morphism is the identity isometry.

Русский

Изометрия от идентичного морфизма равна тождественной изометрии.

LaTeX

$$$ \text{Hom}.\text{toIsometry}(\mathrm{Id}_M) = \mathrm{Isometry.id} _ $$$

Lean4

@[simp]
theorem toIsometry_comp {M N U : QuadraticModuleCat.{v} R} (f : M ⟶ N) (g : N ⟶ U) :
    (f ≫ g).toIsometry = g.toIsometry.comp f.toIsometry :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru