toMonoidWithZeroHom_injective — Mathlib

English

The map sending an ordered monoid with zero homomorphism to its underlying MonoidWithZeroHom is injective; equality of the underlying monoid map implies equality of the original homomorphisms.

Русский

Отображение в MonoidWithZeroHom инъективно: равенство подлежащих моноидных нулевых гомоморфизмов порождает равенство исходных гомоморфизмов.

LaTeX

$$$\forall f,g:\alpha\to_*_0o\beta,\; \big(\operatorname{toMonoidWithZeroHom}(f) = \operatorname{toMonoidWithZeroHom}(g)\big) \Rightarrow f=g$$$

Lean4

theorem toMonoidWithZeroHom_injective : Injective (toMonoidWithZeroHom : _ → α →*₀ β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

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