ext — Mathlib

English

Extensionality for group-object morphisms: if underlying objects are equal, the group morphisms are equal.

Русский

Экстенциональность гомоморфизмов объектов группы: если базовые объекты равны, то и сами гомоморфизмы равны.

LaTeX

$$$\text{GrpObj.ext}$$$

Lean4

@[ext]
theorem ext {X : C} (h₁ h₂ : GrpObj X) (H : h₁.toMonObj = h₂.toMonObj) : h₁ = h₂ :=
  GrpObj.toMonObj_injective H

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