id — Mathlib · SciLib

English

The identity map on α is an ordered monoid homomorphism.

Русский

Единичное отображение на α является упорядоченным моноидным гомоморфизмом.

LaTeX

$$OrderMonoidHom.id α$$

Lean4

/-- The identity map as an ordered monoid homomorphism. -/
@[to_additive /-- The identity map as an ordered additive monoid homomorphism. -/
    ]
protected def id : α →*o α :=
  { MonoidHom.id α, OrderHom.id with }

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