toIsometry_id

Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat

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

English

The isometry of a composition equals the composition of the isometries.

Русский

Изометрия композиции равна композиции изометрий.

LaTeX

$$$ (f \circ g).toIsometry = (g.toIsometry) \circ (f.toIsometry) $$$

Lean4

@[simp]
theorem toIsometry_id {M : QuadraticModuleCat.{v} R} : Hom.toIsometry (𝟙 M) = Isometry.id _ :=
  rfl

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

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

Разделы

Аффилиация

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