Mathlib Map

Theorems · Definition · order theory

OrderRingHom.toRingHom

{α : Type u_6} →
  {β : Type u_7} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] → [inst_2 : NonAssocSemiring β] → [inst_3 : Preorder β] → α →+*o β → α →+* β

Reinterpret an ordered ring homomorphism as a ring homomorphism.

Defined in
Mathlib.Algebra.Order.Hom.Ring
Cited by
3 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
NonAssocSemiringPreorderNonAssocSemiringPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

OrderRingHom.comp · cited by 15OrderRingHom.compOrderRingHom.monotone' · cited by 10OrderRingHom.monotone'OrderRingHom.toRingHom_eq_coe · cited by 6OrderRingHom.toRingHom_eq…ConditionallyCompleteLinearOrderedField.inducedOrderRingIso · cited by 6ConditionallyCompleteLine…OrderRingHom.toOrderAddMonoidHom · cited by 2OrderRingHom.toOrderAddMo…OrderRingHom.copy · cited by 2OrderRingHom.copyOrderRingHom.toOrderMonoidWithZeroHom · cited by 1OrderRingHom.toOrderMonoi…OrderRingHom.toFun_eq_coe · cited by 0OrderRingHom.toFun_eq_coeRingHom · cited by 10189RingHomPreorder · cited by 7952PreorderNonAssocSemiring · cited by 805NonAssocSemiringOrderRingHom · cited by 132OrderRingHomOrderRingHom.toRingHomCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by8

Results whose statement or proof uses this declaration.