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 #

source
@[protected, instance]
def order_dual.has_zero {α : Type u_1} [h : has_zero α] :
has_zero αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_one {α : Type u_1} [h : has_one α] :
has_one αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_add {α : Type u_1} [h : has_add α] :
has_add αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_mul {α : Type u_1} [h : has_mul α] :
has_mul αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_neg {α : Type u_1} [h : has_neg α] :
has_neg αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_inv {α : Type u_1} [h : has_inv α] :
has_inv αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_sub {α : Type u_1} [h : has_sub α] :
has_sub αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_div {α : Type u_1} [h : has_div α] :
has_div αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_smul {α : Type u_1} {β : Type u_2} [h : has_smul α β] :
has_smul α βᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_vadd {α : Type u_1} {β : Type u_2} [h : has_vadd α β] :
has_vadd α βᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_smul' {α : Type u_1} {β : Type u_2} [h : has_smul α β] :
has_smul αᵒᵈ β
Equations
source
@[protected, instance]
def order_dual.has_vadd' {α : Type u_1} {β : Type u_2} [h : has_vadd α β] :
has_vadd αᵒᵈ β
Equations
source
@[protected, instance]
def order_dual.has_pow {α : Type u_1} {β : Type u_2} [h : has_pow α β] :
has_pow αᵒᵈ β
Equations
source
@[protected, instance]
def order_dual.has_pow' {α : Type u_1} {β : Type u_2} [h : has_pow α β] :
has_pow α βᵒᵈ
Equations
source
@[protected, instance]
def order_dual.add_semigroup {α : Type u_1} [h : add_semigroup α] :
add_semigroup αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.semigroup {α : Type u_1} [h : semigroup α] :
semigroup αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.add_comm_semigroup {α : Type u_1} [h : add_comm_semigroup α] :
add_comm_semigroup αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.comm_semigroup {α : Type u_1} [h : comm_semigroup α] :
comm_semigroup αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.left_cancel_add_semigroup {α : Type u_1} [h : add_left_cancel_semigroup α] :
add_left_cancel_semigroup αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.left_cancel_semigroup {α : Type u_1} [h : left_cancel_semigroup α] :
left_cancel_semigroup αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.right_cancel_add_semigroup {α : Type u_1} [h : add_right_cancel_semigroup α] :
add_right_cancel_semigroup αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.right_cancel_semigroup {α : Type u_1} [h : right_cancel_semigroup α] :
right_cancel_semigroup αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.mul_one_class {α : Type u_1} [h : mul_one_class α] :
mul_one_class αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.add_zero_class {α : Type u_1} [h : add_zero_class α] :
add_zero_class αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.add_monoid {α : Type u_1} [h : add_monoid α] :
add_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.monoid {α : Type u_1} [h : monoid α] :
monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.comm_monoid {α : Type u_1} [h : comm_monoid α] :
comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.add_comm_monoid {α : Type u_1} [h : add_comm_monoid α] :
add_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.left_cancel_monoid {α : Type u_1} [h : left_cancel_monoid α] :
left_cancel_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.left_cancel_add_monoid {α : Type u_1} [h : add_left_cancel_monoid α] :
add_left_cancel_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.right_cancel_monoid {α : Type u_1} [h : right_cancel_monoid α] :
right_cancel_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.right_cancel_add_monoid {α : Type u_1} [h : add_right_cancel_monoid α] :
add_right_cancel_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.cancel_monoid {α : Type u_1} [h : cancel_monoid α] :
cancel_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.cancel_add_monoid {α : Type u_1} [h : add_cancel_monoid α] :
add_cancel_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.cancel_add_comm_monoid {α : Type u_1} [h : add_cancel_comm_monoid α] :
add_cancel_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.cancel_comm_monoid {α : Type u_1} [h : cancel_comm_monoid α] :
cancel_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_involutive_neg {α : Type u_1} [h : has_involutive_neg α] :
has_involutive_neg αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_involutive_inv {α : Type u_1} [h : has_involutive_inv α] :
has_involutive_inv αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.div_inv_monoid {α : Type u_1} [h : div_inv_monoid α] :
div_inv_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.sub_neg_add_monoid {α : Type u_1} [h : sub_neg_monoid α] :
sub_neg_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.division_monoid {α : Type u_1} [h : division_monoid α] :
division_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.subtraction_monoid {α : Type u_1} [h : subtraction_monoid α] :
subtraction_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.subtraction_comm_monoid {α : Type u_1} [h : subtraction_comm_monoid α] :
subtraction_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.division_comm_monoid {α : Type u_1} [h : division_comm_monoid α] :
division_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.group {α : Type u_1} [h : group α] :
group αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.add_group {α : Type u_1} [h : add_group α] :
add_group αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.add_comm_group {α : Type u_1} [h : add_comm_group α] :
add_comm_group αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.comm_group {α : Type u_1} [h : comm_group α] :
comm_group αᵒᵈ
Equations
source
@[simp]
theorem to_dual_zero {α : Type u_1} [has_zero α] :
⇑order_dual.to_dual 0 = 0
source
@[simp]
theorem to_dual_one {α : Type u_1} [has_one α] :
⇑order_dual.to_dual 1 = 1
source
@[simp]
theorem of_dual_zero {α : Type u_1} [has_zero α] :
⇑order_dual.of_dual 0 = 0
source
@[simp]
theorem of_dual_one {α : Type u_1} [has_one α] :
⇑order_dual.of_dual 1 = 1
source
@[simp]
theorem to_dual_mul {α : Type u_1} [has_mul α] (a b : α) :
⇑order_dual.to_dual (a * b) = ⇑order_dual.to_dual a * ⇑order_dual.to_dual b
source
@[simp]
theorem to_dual_add {α : Type u_1} [has_add α] (a b : α) :
⇑order_dual.to_dual (a + b) = ⇑order_dual.to_dual a + ⇑order_dual.to_dual b
source
@[simp]
theorem of_dual_mul {α : Type u_1} [has_mul α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (a * b) = ⇑order_dual.of_dual a * ⇑order_dual.of_dual b
source
@[simp]
theorem of_dual_add {α : Type u_1} [has_add α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (a + b) = ⇑order_dual.of_dual a + ⇑order_dual.of_dual b
source
@[simp]
theorem to_dual_inv {α : Type u_1} [has_inv α] (a : α) :
⇑order_dual.to_dual a⁻¹ = (⇑order_dual.to_dual a)⁻¹
source
@[simp]
theorem to_dual_neg {α : Type u_1} [has_neg α] (a : α) :
⇑order_dual.to_dual (-a) = -⇑order_dual.to_dual a
source
@[simp]
theorem of_dual_neg {α : Type u_1} [has_neg α] (a : αᵒᵈ) :
⇑order_dual.of_dual (-a) = -⇑order_dual.of_dual a
source
@[simp]
theorem of_dual_inv {α : Type u_1} [has_inv α] (a : αᵒᵈ) :
⇑order_dual.of_dual a⁻¹ = (⇑order_dual.of_dual a)⁻¹
source
@[simp]
theorem to_dual_div {α : Type u_1} [has_div α] (a b : α) :
⇑order_dual.to_dual (a / b) = ⇑order_dual.to_dual a / ⇑order_dual.to_dual b
source
@[simp]
theorem to_dual_sub {α : Type u_1} [has_sub α] (a b : α) :
⇑order_dual.to_dual (a - b) = ⇑order_dual.to_dual a - ⇑order_dual.to_dual b
source
@[simp]
theorem of_dual_sub {α : Type u_1} [has_sub α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (a - b) = ⇑order_dual.of_dual a - ⇑order_dual.of_dual b
source
@[simp]
theorem of_dual_div {α : Type u_1} [has_div α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (a / b) = ⇑order_dual.of_dual a / ⇑order_dual.of_dual b
source
@[simp]
theorem to_dual_vadd {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : β) :
⇑order_dual.to_dual (a +ᵥ b) = a +ᵥ ⇑order_dual.to_dual b
source
@[simp]
theorem to_dual_smul {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : β) :
⇑order_dual.to_dual (a • b) = a • ⇑order_dual.to_dual b
source
@[simp]
theorem of_dual_smul {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : βᵒᵈ) :
⇑order_dual.of_dual (a • b) = a • ⇑order_dual.of_dual b
source
@[simp]
theorem of_dual_vadd {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : βᵒᵈ) :
⇑order_dual.of_dual (a +ᵥ b) = a +ᵥ ⇑order_dual.of_dual b
source
@[simp]
theorem to_dual_vadd' {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : β) :
⇑order_dual.to_dual a +ᵥ b = a +ᵥ b
source
@[simp]
theorem to_dual_smul' {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : β) :
⇑order_dual.to_dual a • b = a • b
source
@[simp]
theorem of_dual_smul' {α : Type u_1} {β : Type u_2} [has_smul α β] (a : αᵒᵈ) (b : β) :
⇑order_dual.of_dual a • b = a • b
source
@[simp]
theorem of_dual_vadd' {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : αᵒᵈ) (b : β) :
⇑order_dual.of_dual a +ᵥ b = a +ᵥ b
source
@[simp]
theorem to_dual_pow {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : β) :
⇑order_dual.to_dual (a ^ b) = ⇑order_dual.to_dual a ^ b
source
@[simp]
theorem of_dual_pow {α : Type u_1} {β : Type u_2} [has_pow α β] (a : αᵒᵈ) (b : β) :
⇑order_dual.of_dual (a ^ b) = ⇑order_dual.of_dual a ^ b
source
@[simp]
theorem pow_to_dual {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : β) :
a ^ ⇑order_dual.to_dual b = a ^ b
source
@[simp]
theorem pow_of_dual {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : βᵒᵈ) :
a ^ ⇑order_dual.of_dual b = a ^ b

Lexicographical order #

source
@[protected, instance]
def lex.has_one {α : Type u_1} [h : has_one α] :
has_one (lex α)
Equations
source
@[protected, instance]
def lex.has_zero {α : Type u_1} [h : has_zero α] :
has_zero (lex α)
Equations
source
@[protected, instance]
def lex.has_add {α : Type u_1} [h : has_add α] :
has_add (lex α)
Equations
source
@[protected, instance]
def lex.has_mul {α : Type u_1} [h : has_mul α] :
has_mul (lex α)
Equations
source
@[protected, instance]
def lex.has_inv {α : Type u_1} [h : has_inv α] :
has_inv (lex α)
Equations
source
@[protected, instance]
def lex.has_neg {α : Type u_1} [h : has_neg α] :
has_neg (lex α)
Equations
source
@[protected, instance]
def lex.has_div {α : Type u_1} [h : has_div α] :
has_div (lex α)
Equations
source
@[protected, instance]
def lex.has_sub {α : Type u_1} [h : has_sub α] :
has_sub (lex α)
Equations
source
@[protected, instance]
def lex.has_smul {α : Type u_1} {β : Type u_2} [h : has_smul α β] :
has_smul α (lex β)
Equations
source
@[protected, instance]
def lex.has_vadd {α : Type u_1} {β : Type u_2} [h : has_vadd α β] :
has_vadd α (lex β)
Equations
source
@[protected, instance]
def lex.has_smul' {α : Type u_1} {β : Type u_2} [h : has_smul α β] :
has_smul (lex α) β
Equations
source
@[protected, instance]
def lex.has_vadd' {α : Type u_1} {β : Type u_2} [h : has_vadd α β] :
has_vadd (lex α) β
Equations
source
@[protected, instance]
def lex.has_pow {α : Type u_1} {β : Type u_2} [h : has_pow α β] :
has_pow (lex α) β
Equations
source
@[protected, instance]
def lex.has_pow' {α : Type u_1} {β : Type u_2} [h : has_pow α β] :
has_pow α (lex β)
Equations
source
@[protected, instance]
def lex.add_semigroup {α : Type u_1} [h : add_semigroup α] :
add_semigroup (lex α)
Equations
source
@[protected, instance]
def lex.semigroup {α : Type u_1} [h : semigroup α] :
semigroup (lex α)
Equations
source
@[protected, instance]
def lex.add_comm_semigroup {α : Type u_1} [h : add_comm_semigroup α] :
add_comm_semigroup (lex α)
Equations
source
@[protected, instance]
def lex.comm_semigroup {α : Type u_1} [h : comm_semigroup α] :
comm_semigroup (lex α)
Equations
source
@[protected, instance]
def lex.left_cancel_add_semigroup {α : Type u_1} [h : add_left_cancel_semigroup α] :
add_left_cancel_semigroup (lex α)
Equations
source
@[protected, instance]
def lex.left_cancel_semigroup {α : Type u_1} [h : left_cancel_semigroup α] :
left_cancel_semigroup (lex α)
Equations
source
@[protected, instance]
def lex.right_cancel_add_semigroup {α : Type u_1} [h : add_right_cancel_semigroup α] :
add_right_cancel_semigroup (lex α)
Equations
source
@[protected, instance]
def lex.right_cancel_semigroup {α : Type u_1} [h : right_cancel_semigroup α] :
right_cancel_semigroup (lex α)
Equations
source
@[protected, instance]
def lex.mul_one_class {α : Type u_1} [h : mul_one_class α] :
mul_one_class (lex α)
Equations
source
@[protected, instance]
def lex.add_zero_class {α : Type u_1} [h : add_zero_class α] :
add_zero_class (lex α)
Equations
source
@[protected, instance]
def lex.monoid {α : Type u_1} [h : monoid α] :
monoid (lex α)
Equations
source
@[protected, instance]
def lex.add_monoid {α : Type u_1} [h : add_monoid α] :
add_monoid (lex α)
Equations
source
@[protected, instance]
def lex.comm_monoid {α : Type u_1} [h : comm_monoid α] :
comm_monoid (lex α)
Equations
source
@[protected, instance]
def lex.add_comm_monoid {α : Type u_1} [h : add_comm_monoid α] :
add_comm_monoid (lex α)
Equations
source
@[protected, instance]
def lex.left_cancel_add_monoid {α : Type u_1} [h : add_left_cancel_monoid α] :
add_left_cancel_monoid (lex α)
Equations
source
@[protected, instance]
def lex.left_cancel_monoid {α : Type u_1} [h : left_cancel_monoid α] :
left_cancel_monoid (lex α)
Equations
source
@[protected, instance]
def lex.right_cancel_monoid {α : Type u_1} [h : right_cancel_monoid α] :
right_cancel_monoid (lex α)
Equations
source
@[protected, instance]
def lex.right_cancel_add_monoid {α : Type u_1} [h : add_right_cancel_monoid α] :
add_right_cancel_monoid (lex α)
Equations
source
@[protected, instance]
def lex.cancel_monoid {α : Type u_1} [h : cancel_monoid α] :
cancel_monoid (lex α)
Equations
source
@[protected, instance]
def lex.cancel_add_monoid {α : Type u_1} [h : add_cancel_monoid α] :
add_cancel_monoid (lex α)
Equations
source
@[protected, instance]
def lex.cancel_comm_monoid {α : Type u_1} [h : cancel_comm_monoid α] :
cancel_comm_monoid (lex α)
Equations
source
@[protected, instance]
def lex.cancel_add_comm_monoid {α : Type u_1} [h : add_cancel_comm_monoid α] :
add_cancel_comm_monoid (lex α)
Equations
source
@[protected, instance]
def lex.has_involutive_neg {α : Type u_1} [h : has_involutive_neg α] :
has_involutive_neg (lex α)
Equations
source
@[protected, instance]
def lex.has_involutive_inv {α : Type u_1} [h : has_involutive_inv α] :
has_involutive_inv (lex α)
Equations
source
@[protected, instance]
def lex.div_inv_monoid {α : Type u_1} [h : div_inv_monoid α] :
div_inv_monoid (lex α)
Equations
source
@[protected, instance]
def lex.sub_neg_add_monoid {α : Type u_1} [h : sub_neg_monoid α] :
sub_neg_monoid (lex α)
Equations
source
@[protected, instance]
def lex.division_monoid {α : Type u_1} [h : division_monoid α] :
division_monoid (lex α)
Equations
source
@[protected, instance]
def lex.division_comm_monoid {α : Type u_1} [h : division_comm_monoid α] :
division_comm_monoid (lex α)
Equations
source
@[protected, instance]
def lex.group {α : Type u_1} [h : group α] :
group (lex α)
Equations
source
@[protected, instance]
def lex.add_group {α : Type u_1} [h : add_group α] :
add_group (lex α)
Equations
source
@[protected, instance]
def lex.add_comm_group {α : Type u_1} [h : add_comm_group α] :
add_comm_group (lex α)
Equations
source
@[protected, instance]
def lex.comm_group {α : Type u_1} [h : comm_group α] :
comm_group (lex α)
Equations
source
@[simp]
theorem to_lex_zero {α : Type u_1} [has_zero α] :
⇑to_lex 0 = 0
source
@[simp]
theorem to_lex_one {α : Type u_1} [has_one α] :
⇑to_lex 1 = 1
source
@[simp]
theorem of_lex_zero {α : Type u_1} [has_zero α] :
⇑of_lex 0 = 0
source
@[simp]
theorem of_lex_one {α : Type u_1} [has_one α] :
⇑of_lex 1 = 1
source
@[simp]
theorem to_lex_mul {α : Type u_1} [has_mul α] (a b : α) :
⇑to_lex (a * b) = ⇑to_lex a * ⇑to_lex b
source
@[simp]
theorem to_lex_add {α : Type u_1} [has_add α] (a b : α) :
⇑to_lex (a + b) = ⇑to_lex a + ⇑to_lex b
source
@[simp]
theorem of_lex_add {α : Type u_1} [has_add α] (a b : lex α) :
⇑of_lex (a + b) = ⇑of_lex a + ⇑of_lex b
source
@[simp]
theorem of_lex_mul {α : Type u_1} [has_mul α] (a b : lex α) :
⇑of_lex (a * b) = ⇑of_lex a * ⇑of_lex b
source
@[simp]
theorem to_lex_inv {α : Type u_1} [has_inv α] (a : α) :
⇑to_lex a⁻¹ = (⇑to_lex a)⁻¹
source
@[simp]
theorem to_lex_neg {α : Type u_1} [has_neg α] (a : α) :
⇑to_lex (-a) = -⇑to_lex a
source
@[simp]
theorem of_lex_neg {α : Type u_1} [has_neg α] (a : lex α) :
⇑of_lex (-a) = -⇑of_lex a
source
@[simp]
theorem of_lex_inv {α : Type u_1} [has_inv α] (a : lex α) :
⇑of_lex a⁻¹ = (⇑of_lex a)⁻¹
source
@[simp]
theorem to_lex_sub {α : Type u_1} [has_sub α] (a b : α) :
⇑to_lex (a - b) = ⇑to_lex a - ⇑to_lex b
source
@[simp]
theorem to_lex_div {α : Type u_1} [has_div α] (a b : α) :
⇑to_lex (a / b) = ⇑to_lex a / ⇑to_lex b
source
@[simp]
theorem of_lex_sub {α : Type u_1} [has_sub α] (a b : lex α) :
⇑of_lex (a - b) = ⇑of_lex a - ⇑of_lex b
source
@[simp]
theorem of_lex_div {α : Type u_1} [has_div α] (a b : lex α) :
⇑of_lex (a / b) = ⇑of_lex a / ⇑of_lex b
source
@[simp]
theorem to_lex_smul {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : β) :
⇑to_lex (a • b) = a • ⇑to_lex b
source
@[simp]
theorem to_lex_vadd {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : β) :
⇑to_lex (a +ᵥ b) = a +ᵥ ⇑to_lex b
source
@[simp]
theorem of_lex_smul {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : lex β) :
⇑of_lex (a • b) = a • ⇑of_lex b
source
@[simp]
theorem of_lex_vadd {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : lex β) :
⇑of_lex (a +ᵥ b) = a +ᵥ ⇑of_lex b
source
@[simp]
theorem to_lex_vadd' {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : β) :
⇑to_lex a +ᵥ b = a +ᵥ b
source
@[simp]
theorem to_lex_smul' {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : β) :
⇑to_lex a • b = a • b
source
@[simp]
theorem of_lex_vadd' {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : lex α) (b : β) :
⇑of_lex a +ᵥ b = a +ᵥ b
source
@[simp]
theorem of_lex_smul' {α : Type u_1} {β : Type u_2} [has_smul α β] (a : lex α) (b : β) :
⇑of_lex a • b = a • b
source
@[simp]
theorem to_lex_pow {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : β) :
⇑to_lex (a ^ b) = ⇑to_lex a ^ b
source
@[simp]
theorem of_lex_pow {α : Type u_1} {β : Type u_2} [has_pow α β] (a : lex α) (b : β) :
⇑of_lex (a ^ b) = ⇑of_lex a ^ b
source
@[simp]
theorem pow_to_lex {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : β) :
a ^ ⇑to_lex b = a ^ b
source
@[simp]
theorem pow_of_lex {α : Type u_1} {β : Type u_2} [has_pow α β] (a : α) (b : lex β) :
a ^ ⇑of_lex b = a ^ b