Theorems · Theorem · order theory

ArchimedeanClass.mk_map_nonneg_of_archimedean

∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) (y : S),
  0 ≤ ArchimedeanClass.mk (f y)

Defined in

Mathlib.Algebra.Order.Ring.Archimedean

Cited by

6 results in Mathlib

Foundations

Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderCommRingIsStrictOrderedRingLinearOrderCommRingIsStrictOrderedRingArchimedean