coe_toAddMonoidHom_injective — Mathlib

English

The natural embedding of CentroidHom α into α →+ α is injective; i.e., different centroid homomorphisms induce different additive monoid homs.

Русский

Естественная вставка CentroidHom α в α →+ α инъективна; разные центроид-гомоморфы порождают разные обратимые подстановки.

LaTeX

$$Injective ((↑) : CentroidHom α → α →+ α)$$

Lean4

theorem coe_toAddMonoidHom_injective : Injective ((↑) : CentroidHom α → α →+ α) := fun _f _g h =>
  ext fun a ↦
    haveI := DFunLike.congr_fun h a
    this

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