floorRing — Mathlib

English

A linear ordered field that is a floor ring is Archimedean.

Русский

Линейно упорядоченное кольцо, являющееся floorRing, яв-ется архимедовым.

LaTeX

$$$$ \operatorname{Archimedean}(K) \quad\text{при } [\text{Field } K], [\text{LinearOrder } K], [\text{IsStrictOrderedRing } K], [\text{FloorRing } K]. $$$$

Lean4

/-- A linear ordered archimedean ring is a floor ring. This is not an `instance` because in some
cases we have a computable `floor` function. -/
noncomputable def floorRing (R) [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] : FloorRing R :=
  .ofFloor R (fun a => Classical.choose (exists_floor a)) fun z a => (Classical.choose_spec (exists_floor a) z).symm

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