hom_ext — Mathlib

English

Two magma homomorphisms from the quotient are equal if they agree on the quotient of every generator.

Русский

Две морфизм-умножения из фактор-множества равны, если они согласованы на образах генераторов.

LaTeX

$$$\forall f,g : \mathrm{AssocQuotient}(\alpha) \to_{\mathsf{n}*} \beta,\ (f\circ \mathrm{of} = g\circ \mathrm{of}) \Rightarrow f = g$$$

Lean4

@[to_additive (attr := ext 1100)]
theorem hom_ext {f g : AssocQuotient α →ₙ* β} (h : f.comp of = g.comp of) : f = g :=
  (DFunLike.ext _ _) fun x => AssocQuotient.induction_on x <| DFunLike.congr_fun h

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