id — Mathlib · SciLib

English

The identity as an ordered ring homomorphism acts as the identity on elements: (OrderRingHom.id α)(a) = a for all a.

Русский

Идентичность как упорядоченный кольцевой гомоморфизм действует как тождественный отображение: (OrderRingHom.id α)(a) = a для всех a.

LaTeX

$$$\forall a,\; (OrderRingHom.id\,\alpha)(a) = a$$$

Lean4

/-- The identity as an ordered ring homomorphism. -/
protected def id : α →+*o α :=
  { RingHom.id _, OrderHom.id with }

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