toIsOrderedRing — Mathlib

English

A subring of an ordered ring inherits an ordered ring structure.

Русский

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

LaTeX

$$$IsOrderedRing\; s$ for the subring s, i.e. IsOrderedRing(s)$$

Lean4

/-- A subring of an ordered ring is an ordered ring. -/
instance toIsOrderedRing [Ring R] [PartialOrder R] [IsOrderedRing R] (s : Subring R) : IsOrderedRing s :=
  Function.Injective.isOrderedRing Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) .rfl

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