Theorems · Definition · order theory
OrderRingIso.refl
(α : Type u_2) → [inst : Mul α] → [inst_1 : Add α] → [inst_2 : LE α] → α ≃+*o α
The identity map as an ordered ring isomorphism.
- Defined in
- Mathlib.Algebra.Order.Hom.Ring
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingEquiv.reflproof · cited by 72
- OrderRingIsostatement · cited by 43
Cited by9
Results whose statement or proof uses this declaration.
- ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_selfstatement · cited by 1
- OrderRingIso.refl_applystatement and proof · cited by 0
- OrderRingIso.self_trans_symmstatement · cited by 0
- LinearOrderedField.inducedOrderRingIso_selfstatement · cited by 0
- OrderRingIso.coe_orderIso_reflstatement · cited by 0
- OrderRingIso.coe_toOrderRingHom_reflstatement · cited by 0
- OrderRingIso.eq_reflstatement and proof · cited by 0
- OrderRingIso.coe_ringEquiv_reflstatement · cited by 0
- OrderRingIso.symm_trans_selfstatement · cited by 0