hom_ext — Mathlib

English

Extensionality for fg morphisms in FGModuleCat; equality of homs yields equality of morphisms.

Русский

Расширенная редукция для морфизмов FGModuleCat; равенство гомоморфизмов влечёт равенство морфизмов.

LaTeX

$$$f.\\mathrm{hom} = g.\\mathrm{hom} \\Rightarrow f = g$$$

Lean4

@[ext]
theorem hom_ext {V W : FGModuleCat.{v} R} {f g : V ⟶ W} (h : f.hom = g.hom) : f = g :=
  ModuleCat.hom_ext h

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