Theorems · Inductive type · order theory

OrderRingIso

(α : Type u_6) → (β : Type u_7) → [Mul α] → [Add α] → [Mul β] → [Add β] → [LE α] → [LE β] → Type (max u_6 u_7)

OrderRingIso α β, denoted as α ≃+*o β, is the type of order-preserving semiring isomorphisms between α and β. When possible, instead of parametrizing results over (f : OrderRingIso α β), you should parametrize over (F : Type*) [OrderRingIsoClass F α β] (f : F). When you extend this structure, make sure to extend OrderRingIsoClass.

Defined in

Mathlib.Algebra.Order.Hom.Ring

Cited by

43 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

MulAddMulAddLELE