toMulActionHom_injective — Mathlib

English

If two equivariant additive monoid homomorphisms f and g have the same underlying function, 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 toMulActionHom_injective {f g : A →ₑ+[φ] B} (h : (f : A →ₑ[φ] B) = (g : A →ₑ[φ] B)) : f = g :=
  by
  ext a
  exact MulActionHom.congr_fun h a

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