mathlib3 documentation

algebra.ring.order_synonym

Ring structure on the order type synonyms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Transfer algebraic instances from α to αᵒᵈ and lex α.

Order dual #

@[protected, instance]
def order_dual.distrib {α : Type u_1} [h : distrib α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.semiring {α : Type u_1} [h : semiring α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.ring {α : Type u_1} [h : ring α] :
Equations
@[protected, instance]
def order_dual.comm_ring {α : Type u_1} [h : comm_ring α] :
Equations
@[protected, instance]
def order_dual.is_domain {α : Type u_1} [ring α] [h : is_domain α] :

Lexicographical order #

@[protected, instance]
def lex.distrib {α : Type u_1} [h : distrib α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.semiring {α : Type u_1} [h : semiring α] :
Equations
@[protected, instance]
def lex.comm_semiring {α : Type u_1} [h : comm_semiring α] :
Equations
@[protected, instance]
def lex.has_distrib_neg {α : Type u_1} [has_mul α] [h : has_distrib_neg α] :
Equations
@[protected, instance]
def lex.non_unital_ring {α : Type u_1} [h : non_unital_ring α] :
Equations
@[protected, instance]
def lex.non_assoc_ring {α : Type u_1} [h : non_assoc_ring α] :
Equations
@[protected, instance]
def lex.ring {α : Type u_1} [h : ring α] :
ring (lex α)
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.comm_ring {α : Type u_1} [h : comm_ring α] :
Equations
@[protected, instance]
def lex.is_domain {α : Type u_1} [ring α] [h : is_domain α] :