Theorems · Definition · order theory
OrderRingHom.id
(α : Type u_2) → [inst : NonAssocSemiring α] → [inst_1 : Preorder α] → α →+*o α
The identity as an ordered ring homomorphism.
- Defined in
- Mathlib.Algebra.Order.Hom.Ring
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
- Assumes
- NonAssocSemiringPreorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idproof · cited by 18,349
- RingHomproof · cited by 10,189
- Preorderstatement and proof · cited by 7,952
- OrderHomproof · cited by 934
- NonAssocSemiringstatement and proof · cited by 805
- OrderRingHomstatement · cited by 132
- OrderHom.idproof · cited by 37
- OrderHom.monotone'proof · cited by 8
Cited by11
Results whose statement or proof uses this declaration.
- OrderRingHom.apply_eq_selfproof · cited by 2
- OrderRingHom.eq_idstatement and proof · cited by 1
- OrderRingHom.coe_idstatement · cited by 0
- OrderRingHom.coe_orderAddMonoidHom_idstatement · cited by 0
- OrderRingHom.coe_orderMonoidWithZeroHom_idstatement · cited by 0
- OrderRingIso.coe_toOrderRingHom_reflstatement · cited by 0
- OrderRingHom.coe_ringHom_idstatement · cited by 0
- ArchimedeanClass.stdPart_realproof · cited by 0
- OrderRingHom.comp_idstatement · cited by 0
- OrderRingHom.id_applystatement · cited by 0
- OrderRingHom.id_compstatement · cited by 0