mapMulHom_injective' — Mathlib

English

The map that sends a semigroup homomorphism to the corresponding monoid homomorphism is injective.

Русский

Отображение, переводящее полугомоморфизм в соответствующий монойд-гомоморфизм, инъективно.

LaTeX

$$$\text{mapMulHom}$ : injective$$

Lean4

@[to_additive]
theorem mapMulHom_injective' : Function.Injective (WithOne.mapMulHom (α := α) (β := β)) := fun f g h ↦
  MulHom.ext fun x ↦ coe_injective <| by simp only [← mapMulHom_coe, h]

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