orderedSubtype — Mathlib

English

The inclusion S → R of a subring, as an ordered ring homomorphism.

Русский

Включение S → R как упорядоченного кольцевого однородного отображения.

LaTeX

$$$\text{orderedSubtype}(S) = \text{subtype}(S)$$$

Lean4

/-- The inclusion `S → R` of a subring, as an ordered ring homomorphism. -/
def orderedSubtype {R : Type*} [Ring R] [PartialOrder R] (s : Subring R) : s →+*o R
    where
  __ := s.subtype
  monotone' := fun _ _ h ↦ h

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