mathlib3 documentation

algebra.group.order_synonym

Group 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.has_zero {α : Type u_1} [h : has_zero α] :
Equations
@[protected, instance]
def order_dual.has_one {α : Type u_1} [h : has_one α] :
Equations
@[protected, instance]
def order_dual.has_add {α : Type u_1} [h : has_add α] :
Equations
@[protected, instance]
def order_dual.has_mul {α : Type u_1} [h : has_mul α] :
Equations
@[protected, instance]
def order_dual.has_neg {α : Type u_1} [h : has_neg α] :
Equations
@[protected, instance]
def order_dual.has_inv {α : Type u_1} [h : has_inv α] :
Equations
@[protected, instance]
def order_dual.has_sub {α : Type u_1} [h : has_sub α] :
Equations
@[protected, instance]
def order_dual.has_div {α : Type u_1} [h : has_div α] :
Equations
@[protected, instance]
def order_dual.has_smul {α : Type u_1} {β : Type u_2} [h : has_smul α β] :
Equations
@[protected, instance]
def order_dual.has_vadd {α : Type u_1} {β : Type u_2} [h : has_vadd α β] :
Equations
@[protected, instance]
def order_dual.has_smul' {α : Type u_1} {β : Type u_2} [h : has_smul α β] :
Equations
@[protected, instance]
def order_dual.has_vadd' {α : Type u_1} {β : Type u_2} [h : has_vadd α β] :
Equations
@[protected, instance]
def order_dual.has_pow {α : Type u_1} {β : Type u_2} [h : has_pow α β] :
Equations
@[protected, instance]
def order_dual.has_pow' {α : Type u_1} {β : Type u_2} [h : has_pow α β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.semigroup {α : Type u_1} [h : semigroup α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.add_monoid {α : Type u_1} [h : add_monoid α] :
Equations
@[protected, instance]
def order_dual.monoid {α : Type u_1} [h : monoid α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.group {α : Type u_1} [h : group α] :
Equations
@[protected, instance]
def order_dual.add_group {α : Type u_1} [h : add_group α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.comm_group {α : Type u_1} [h : comm_group α] :
Equations
@[simp]
theorem to_dual_zero {α : Type u_1} [has_zero α] :
@[simp]
theorem to_dual_one {α : Type u_1} [has_one α] :
@[simp]
theorem of_dual_zero {α : Type u_1} [has_zero α] :
@[simp]
theorem of_dual_one {α : Type u_1} [has_one α] :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem to_dual_neg {α : Type u_1} [has_neg α] (a : α) :
@[simp]
theorem of_dual_neg {α : Type u_1} [has_neg α] (a : αᵒᵈ) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem to_dual_vadd {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : β) :
@[simp]
theorem to_dual_smul {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : β) :
@[simp]
theorem of_dual_smul {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : βᵒᵈ) :
@[simp]
theorem of_dual_vadd {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : βᵒᵈ) :
@[simp]
theorem to_dual_vadd' {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : β) :
@[simp]
theorem to_dual_smul' {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : β) :
@[simp]
theorem of_dual_smul' {α : Type u_1} {β : Type u_2} [has_smul α β] (a : αᵒᵈ) (b : β) :
@[simp]
theorem of_dual_vadd' {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : αᵒᵈ) (b : β) :
@[simp]
theorem to_dual_pow {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : β) :
@[simp]
theorem of_dual_pow {α : Type u_1} {β : Type u_2} [has_pow α β] (a : αᵒᵈ) (b : β) :
@[simp]
theorem pow_to_dual {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : β) :
@[simp]
theorem pow_of_dual {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : βᵒᵈ) :

Lexicographical order #

@[protected, instance]
def lex.has_one {α : Type u_1} [h : has_one α] :
Equations
@[protected, instance]
def lex.has_zero {α : Type u_1} [h : has_zero α] :
Equations
@[protected, instance]
def lex.has_add {α : Type u_1} [h : has_add α] :
Equations
@[protected, instance]
def lex.has_mul {α : Type u_1} [h : has_mul α] :
Equations
@[protected, instance]
def lex.has_inv {α : Type u_1} [h : has_inv α] :
Equations
@[protected, instance]
def lex.has_neg {α : Type u_1} [h : has_neg α] :
Equations
@[protected, instance]
def lex.has_div {α : Type u_1} [h : has_div α] :
Equations
@[protected, instance]
def lex.has_sub {α : Type u_1} [h : has_sub α] :
Equations
@[protected, instance]
def lex.has_smul {α : Type u_1} {β : Type u_2} [h : has_smul α β] :
has_smul α (lex β)
Equations
@[protected, instance]
def lex.has_vadd {α : Type u_1} {β : Type u_2} [h : has_vadd α β] :
has_vadd α (lex β)
Equations
@[protected, instance]
def lex.has_smul' {α : Type u_1} {β : Type u_2} [h : has_smul α β] :
has_smul (lex α) β
Equations
@[protected, instance]
def lex.has_vadd' {α : Type u_1} {β : Type u_2} [h : has_vadd α β] :
has_vadd (lex α) β
Equations
@[protected, instance]
def lex.has_pow {α : Type u_1} {β : Type u_2} [h : has_pow α β] :
has_pow (lex α) β
Equations
@[protected, instance]
def lex.has_pow' {α : Type u_1} {β : Type u_2} [h : has_pow α β] :
has_pow α (lex β)
Equations
@[protected, instance]
def lex.add_semigroup {α : Type u_1} [h : add_semigroup α] :
Equations
@[protected, instance]
def lex.semigroup {α : Type u_1} [h : semigroup α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.comm_semigroup {α : Type u_1} [h : comm_semigroup α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.mul_one_class {α : Type u_1} [h : mul_one_class α] :
Equations
@[protected, instance]
def lex.add_zero_class {α : Type u_1} [h : add_zero_class α] :
Equations
@[protected, instance]
def lex.monoid {α : Type u_1} [h : monoid α] :
monoid (lex α)
Equations
@[protected, instance]
def lex.add_monoid {α : Type u_1} [h : add_monoid α] :
Equations
@[protected, instance]
def lex.comm_monoid {α : Type u_1} [h : comm_monoid α] :
Equations
@[protected, instance]
def lex.add_comm_monoid {α : Type u_1} [h : add_comm_monoid α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.cancel_monoid {α : Type u_1} [h : cancel_monoid α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.div_inv_monoid {α : Type u_1} [h : div_inv_monoid α] :
Equations
@[protected, instance]
def lex.sub_neg_add_monoid {α : Type u_1} [h : sub_neg_monoid α] :
Equations
@[protected, instance]
def lex.division_monoid {α : Type u_1} [h : division_monoid α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.group {α : Type u_1} [h : group α] :
group (lex α)
Equations
@[protected, instance]
def lex.add_group {α : Type u_1} [h : add_group α] :
Equations
@[protected, instance]
def lex.add_comm_group {α : Type u_1} [h : add_comm_group α] :
Equations
@[protected, instance]
def lex.comm_group {α : Type u_1} [h : comm_group α] :
Equations
@[simp]
theorem to_lex_zero {α : Type u_1} [has_zero α] :
@[simp]
theorem to_lex_one {α : Type u_1} [has_one α] :
@[simp]
theorem of_lex_zero {α : Type u_1} [has_zero α] :
@[simp]
theorem of_lex_one {α : Type u_1} [has_one α] :
@[simp]
theorem to_lex_mul {α : Type u_1} [has_mul α] (a b : α) :
@[simp]
theorem to_lex_add {α : Type u_1} [has_add α] (a b : α) :
@[simp]
theorem of_lex_add {α : Type u_1} [has_add α] (a b : lex α) :
@[simp]
theorem of_lex_mul {α : Type u_1} [has_mul α] (a b : lex α) :
@[simp]
theorem to_lex_inv {α : Type u_1} [has_inv α] (a : α) :
@[simp]
theorem to_lex_neg {α : Type u_1} [has_neg α] (a : α) :
@[simp]
theorem of_lex_neg {α : Type u_1} [has_neg α] (a : lex α) :
@[simp]
theorem of_lex_inv {α : Type u_1} [has_inv α] (a : lex α) :
@[simp]
theorem to_lex_sub {α : Type u_1} [has_sub α] (a b : α) :
@[simp]
theorem to_lex_div {α : Type u_1} [has_div α] (a b : α) :
@[simp]
theorem of_lex_sub {α : Type u_1} [has_sub α] (a b : lex α) :
@[simp]
theorem of_lex_div {α : Type u_1} [has_div α] (a b : lex α) :
@[simp]
theorem to_lex_smul {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : β) :
@[simp]
theorem to_lex_vadd {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : β) :
@[simp]
theorem of_lex_smul {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : lex β) :
@[simp]
theorem of_lex_vadd {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : lex β) :
@[simp]
theorem to_lex_vadd' {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : β) :
@[simp]
theorem to_lex_smul' {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : β) :
to_lex a b = a b
@[simp]
theorem of_lex_vadd' {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : lex α) (b : β) :
@[simp]
theorem of_lex_smul' {α : Type u_1} {β : Type u_2} [has_smul α β] (a : lex α) (b : β) :
of_lex a b = a b
@[simp]
theorem to_lex_pow {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : β) :
to_lex (a ^ b) = to_lex a ^ b
@[simp]
theorem of_lex_pow {α : Type u_1} {β : Type u_2} [has_pow α β] (a : lex α) (b : β) :
of_lex (a ^ b) = of_lex a ^ b
@[simp]
theorem pow_to_lex {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : β) :
a ^ to_lex b = a ^ b
@[simp]
theorem pow_of_lex {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : lex β) :
a ^ of_lex b = a ^ b