toAddMonoidHom_injective — Mathlib

English

If two equivariant additive monoid homomorphisms f and g have the same underlying additive monoid homomorphism, then f = g.

Русский

Если два эквариантных аддитивных моноид-гомоморфизма f и g имеют одинаковое подлежащее аддитивному гомоморфизму отображение, то f = g.

LaTeX

$$$ (f : A \\to_{e+[\\phi]} B) = (g : A \\to_{e+[\\phi]} B) \\Rightarrow f = g $$$

Lean4

theorem toAddMonoidHom_injective {f g : A →ₑ+[φ] B} (h : (f : A →+ B) = (g : A →+ B)) : f = g :=
  by
  ext a
  exact DFunLike.congr_fun h a

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