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 #

source
@[protected, instance]
def order_dual.distrib {α : Type u_1} [h : distrib α] :
distrib αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.left_distrib_class {α : Type u_1} [has_mul α] [has_add α] [h : left_distrib_class α] :
left_distrib_class αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.right_distrib_class {α : Type u_1} [has_mul α] [has_add α] [h : right_distrib_class α] :
right_distrib_class αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.non_unital_non_assoc_semiring {α : Type u_1} [h : non_unital_non_assoc_semiring α] :
non_unital_non_assoc_semiring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.non_unital_semiring {α : Type u_1} [h : non_unital_semiring α] :
non_unital_semiring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.non_assoc_semiring {α : Type u_1} [h : non_assoc_semiring α] :
non_assoc_semiring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.semiring {α : Type u_1} [h : semiring α] :
semiring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.non_unital_comm_semiring {α : Type u_1} [h : non_unital_comm_semiring α] :
non_unital_comm_semiring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.comm_semiring {α : Type u_1} [h : comm_semiring α] :
comm_semiring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_distrib_neg {α : Type u_1} [has_mul α] [h : has_distrib_neg α] :
has_distrib_neg αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.non_unital_non_assoc_ring {α : Type u_1} [h : non_unital_non_assoc_ring α] :
non_unital_non_assoc_ring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.non_unital_ring {α : Type u_1} [h : non_unital_ring α] :
non_unital_ring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.non_assoc_ring {α : Type u_1} [h : non_assoc_ring α] :
non_assoc_ring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.ring {α : Type u_1} [h : ring α] :
ring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.non_unital_comm_ring {α : Type u_1} [h : non_unital_comm_ring α] :
non_unital_comm_ring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.comm_ring {α : Type u_1} [h : comm_ring α] :
comm_ring αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.is_domain {α : Type u_1} [ring α] [h : is_domain α] :
is_domain αᵒᵈ

Lexicographical order #

source
@[protected, instance]
def lex.distrib {α : Type u_1} [h : distrib α] :
distrib (lex α)
Equations
source
@[protected, instance]
def lex.left_distrib_class {α : Type u_1} [has_mul α] [has_add α] [h : left_distrib_class α] :
left_distrib_class (lex α)
Equations
source
@[protected, instance]
def lex.right_distrib_class {α : Type u_1} [has_mul α] [has_add α] [h : right_distrib_class α] :
right_distrib_class (lex α)
Equations
source
@[protected, instance]
def lex.non_unital_non_assoc_semiring {α : Type u_1} [h : non_unital_non_assoc_semiring α] :
non_unital_non_assoc_semiring (lex α)
Equations
source
@[protected, instance]
def lex.non_unital_semiring {α : Type u_1} [h : non_unital_semiring α] :
non_unital_semiring (lex α)
Equations
source
@[protected, instance]
def lex.non_assoc_semiring {α : Type u_1} [h : non_assoc_semiring α] :
non_assoc_semiring (lex α)
Equations
source
@[protected, instance]
def lex.semiring {α : Type u_1} [h : semiring α] :
semiring (lex α)
Equations
source
@[protected, instance]
def lex.non_unital_comm_semiring {α : Type u_1} [h : non_unital_comm_semiring α] :
non_unital_comm_semiring (lex α)
Equations
source
@[protected, instance]
def lex.comm_semiring {α : Type u_1} [h : comm_semiring α] :
comm_semiring (lex α)
Equations
source
@[protected, instance]
def lex.has_distrib_neg {α : Type u_1} [has_mul α] [h : has_distrib_neg α] :
has_distrib_neg (lex α)
Equations
source
@[protected, instance]
def lex.non_unital_non_assoc_ring {α : Type u_1} [h : non_unital_non_assoc_ring α] :
non_unital_non_assoc_ring (lex α)
Equations
source
@[protected, instance]
def lex.non_unital_ring {α : Type u_1} [h : non_unital_ring α] :
non_unital_ring (lex α)
Equations
source
@[protected, instance]
def lex.non_assoc_ring {α : Type u_1} [h : non_assoc_ring α] :
non_assoc_ring (lex α)
Equations
source
@[protected, instance]
def lex.ring {α : Type u_1} [h : ring α] :
ring (lex α)
Equations
source
@[protected, instance]
def lex.non_unital_comm_ring {α : Type u_1} [h : non_unital_comm_ring α] :
non_unital_comm_ring (lex α)
Equations
source
@[protected, instance]
def lex.comm_ring {α : Type u_1} [h : comm_ring α] :
comm_ring (lex α)
Equations
source
@[protected, instance]
def lex.is_domain {α : Type u_1} [ring α] [h : is_domain α] :
is_domain (lex α)