hom_ext

Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat

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

English

If two morphisms have the same isometry, they are equal.

Русский

Если две морфизмы имеют одинаковую изометрию, они равны.

LaTeX

$$$ \forall f,g: M \to N, \; f.toIsometry = g.toIsometry \Rightarrow f = g $$$

Lean4

@[ext]
theorem hom_ext {M N : QuadraticModuleCat.{v} R} (f g : M ⟶ N) (h : f.toIsometry = g.toIsometry) : f = g :=
  Hom.ext h

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

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

Разделы

Аффилиация

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