embDomainOrderAddMonoidHom_injective

English

The map embDomainOrderAddMonoidHom f is injective when R is an additive monoid.

Русский

Отображение embDomainOrderAddMonoidHom инъективно при R как моноидной группе сложения.

LaTeX

$$$\mathrm{Injective}(\mathrm{embDomainOrderAddMonoidHom}(f))$$$

Lean4

theorem embDomainOrderAddMonoidHom_injective [AddMonoid R] :
    Function.Injective (embDomainOrderAddMonoidHom f (R := R)) :=
  (embDomainOrderEmbedding f).injective

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