toIsStrictOrderedRing — Mathlib

English

A subring of a strictly ordered ring is a strictly ordered ring.

Русский

Подкольцо строго упорядоченного кольца является строго упорядоченным кольцом.

LaTeX

$$$IsStrictOrderedRing\; s$$$

Lean4

/-- A subring of a strict ordered ring is a strict ordered ring. -/
instance toIsStrictOrderedRing [Ring R] [PartialOrder R] [IsStrictOrderedRing R] (s : Subring R) :
    IsStrictOrderedRing s :=
  Function.Injective.isStrictOrderedRing Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) .rfl .rfl

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