toIsStrictOrderedRing — Mathlib

English

A subfield of an ordered field is itself an ordered field (with the inherited order).

Русский

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

LaTeX

$$$\text{If } K \text{ is an ordered field and } S \subseteq K \text{ is a subfield, then } S \text{ inherits an ordered field structure.}$$$

Lean4

/-- A subfield of an ordered field is a ordered field. -/
instance toIsStrictOrderedRing [Field K] [LinearOrder K] [IsStrictOrderedRing K] (s : Subfield K) :
    IsStrictOrderedRing s :=
  Function.Injective.isStrictOrderedRing Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) .rfl .rfl

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