Documentation

Mathlib.Algebra.Group.OrderSynonym

Group structure on the order type synonyms #

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

OrderDual #

source
ink
instance instZeroOrderDual {α : Type u_1} [h : Zero α] :
Zero αᵒᵈ
Equations
  • instZeroOrderDual = h
source
ink
instance instOneOrderDual {α : Type u_1} [h : One α] :
One αᵒᵈ
Equations
  • instOneOrderDual = h
source
ink
instance instAddOrderDual {α : Type u_1} [h : Add α] :
Add αᵒᵈ
Equations
  • instAddOrderDual = h
source
ink
instance instMulOrderDual {α : Type u_1} [h : Mul α] :
Mul αᵒᵈ
Equations
  • instMulOrderDual = h
source
ink
instance instNegOrderDual {α : Type u_1} [h : Neg α] :
Neg αᵒᵈ
Equations
  • instNegOrderDual = h
source
ink
instance instInvOrderDual {α : Type u_1} [h : Inv α] :
Inv αᵒᵈ
Equations
  • instInvOrderDual = h
source
ink
instance instSubOrderDual {α : Type u_1} [h : Sub α] :
Sub αᵒᵈ
Equations
  • instSubOrderDual = h
source
ink
instance instDivOrderDual {α : Type u_1} [h : Div α] :
Div αᵒᵈ
Equations
  • instDivOrderDual = h
source
ink
instance instVAddOrderDual {β : Type u_2} {α : Type u_1} [h : VAdd β α] :
VAdd β αᵒᵈ
Equations
  • instVAddOrderDual = h
source
ink
instance instSMulOrderDual {β : Type u_2} {α : Type u_1} [h : SMul β α] :
SMul β αᵒᵈ
Equations
  • instSMulOrderDual = h
source
ink
instance instPowOrderDual {α : Type u_1} {β : Type u_2} [h : Pow α β] :
Pow αᵒᵈ β
Equations
  • instPowOrderDual = h
source
ink
instance instSMulOrderDual' {β : Type u_2} {α : Type u_1} [h : SMul β α] :
SMul βᵒᵈ α
Equations
  • instSMulOrderDual' = h
source
ink
instance instVAddOrderDual' {β : Type u_2} {α : Type u_1} [h : VAdd β α] :
VAdd βᵒᵈ α
Equations
  • instVAddOrderDual' = h
source
ink
instance instPowOrderDual' {α : Type u_1} {β : Type u_2} [h : Pow α β] :
Pow α βᵒᵈ
Equations
  • instPowOrderDual' = h
source
ink
instance instAddSemigroupOrderDual {α : Type u_1} [h : AddSemigroup α] :
AddSemigroup αᵒᵈ
Equations
  • instAddSemigroupOrderDual = h
source
ink
instance instSemigroupOrderDual {α : Type u_1} [h : Semigroup α] :
Semigroup αᵒᵈ
Equations
  • instSemigroupOrderDual = h
source
ink
instance instAddCommSemigroupOrderDual {α : Type u_1} [h : AddCommSemigroup α] :
AddCommSemigroup αᵒᵈ
Equations
  • instAddCommSemigroupOrderDual = h
source
ink
instance instCommSemigroupOrderDual {α : Type u_1} [h : CommSemigroup α] :
CommSemigroup αᵒᵈ
Equations
  • instCommSemigroupOrderDual = h
source
ink
instance instAddLeftCancelSemigroupOrderDual {α : Type u_1} [h : AddLeftCancelSemigroup α] :
AddLeftCancelSemigroup αᵒᵈ
Equations
  • instAddLeftCancelSemigroupOrderDual = h
source
ink
instance instLeftCancelSemigroupOrderDual {α : Type u_1} [h : LeftCancelSemigroup α] :
LeftCancelSemigroup αᵒᵈ
Equations
  • instLeftCancelSemigroupOrderDual = h
source
ink
instance instAddRightCancelSemigroupOrderDual {α : Type u_1} [h : AddRightCancelSemigroup α] :
AddRightCancelSemigroup αᵒᵈ
Equations
  • instAddRightCancelSemigroupOrderDual = h
source
ink
instance instRightCancelSemigroupOrderDual {α : Type u_1} [h : RightCancelSemigroup α] :
RightCancelSemigroup αᵒᵈ
Equations
  • instRightCancelSemigroupOrderDual = h
source
ink
instance instAddZeroClassOrderDual {α : Type u_1} [h : AddZeroClass α] :
AddZeroClass αᵒᵈ
Equations
  • instAddZeroClassOrderDual = h
source
ink
instance instMulOneClassOrderDual {α : Type u_1} [h : MulOneClass α] :
MulOneClass αᵒᵈ
Equations
  • instMulOneClassOrderDual = h
source
ink
instance instAddMonoidOrderDual {α : Type u_1} [h : AddMonoid α] :
AddMonoid αᵒᵈ
Equations
  • instAddMonoidOrderDual = h
source
ink
instance instMonoidOrderDual {α : Type u_1} [h : Monoid α] :
Monoid αᵒᵈ
Equations
  • instMonoidOrderDual = h
source
ink
instance instAddCommMonoidOrderDual {α : Type u_1} [h : AddCommMonoid α] :
AddCommMonoid αᵒᵈ
Equations
  • instAddCommMonoidOrderDual = h
source
ink
instance instCommMonoidOrderDual {α : Type u_1} [h : CommMonoid α] :
CommMonoid αᵒᵈ
Equations
  • instCommMonoidOrderDual = h
source
ink
instance instAddLeftCancelMonoidOrderDual {α : Type u_1} [h : AddLeftCancelMonoid α] :
AddLeftCancelMonoid αᵒᵈ
Equations
  • instAddLeftCancelMonoidOrderDual = h
source
ink
instance instLeftCancelMonoidOrderDual {α : Type u_1} [h : LeftCancelMonoid α] :
LeftCancelMonoid αᵒᵈ
Equations
  • instLeftCancelMonoidOrderDual = h
source
ink
instance instAddRightCancelMonoidOrderDual {α : Type u_1} [h : AddRightCancelMonoid α] :
AddRightCancelMonoid αᵒᵈ
Equations
  • instAddRightCancelMonoidOrderDual = h
source
ink
instance instRightCancelMonoidOrderDual {α : Type u_1} [h : RightCancelMonoid α] :
RightCancelMonoid αᵒᵈ
Equations
  • instRightCancelMonoidOrderDual = h
source
ink
instance instAddCancelMonoidOrderDual {α : Type u_1} [h : AddCancelMonoid α] :
AddCancelMonoid αᵒᵈ
Equations
  • instAddCancelMonoidOrderDual = h
source
ink
instance instCancelMonoidOrderDual {α : Type u_1} [h : CancelMonoid α] :
CancelMonoid αᵒᵈ
Equations
  • instCancelMonoidOrderDual = h
source
ink
instance instAddCancelCommMonoidOrderDual {α : Type u_1} [h : AddCancelCommMonoid α] :
AddCancelCommMonoid αᵒᵈ
Equations
  • instAddCancelCommMonoidOrderDual = h
source
ink
instance instCancelCommMonoidOrderDual {α : Type u_1} [h : CancelCommMonoid α] :
CancelCommMonoid αᵒᵈ
Equations
  • instCancelCommMonoidOrderDual = h
source
ink
instance instInvolutiveNegOrderDual {α : Type u_1} [h : InvolutiveNeg α] :
InvolutiveNeg αᵒᵈ
Equations
  • instInvolutiveNegOrderDual = h
source
ink
instance instInvolutiveInvOrderDual {α : Type u_1} [h : InvolutiveInv α] :
InvolutiveInv αᵒᵈ
Equations
  • instInvolutiveInvOrderDual = h
source
ink
instance instSubNegAddMonoidOrderDual {α : Type u_1} [h : SubNegMonoid α] :
SubNegMonoid αᵒᵈ
Equations
  • instSubNegAddMonoidOrderDual = h
source
ink
instance instDivInvMonoidOrderDual {α : Type u_1} [h : DivInvMonoid α] :
DivInvMonoid αᵒᵈ
Equations
  • instDivInvMonoidOrderDual = h
source
ink
instance OrderDual.subtractionMonoid {α : Type u_1} [h : SubtractionMonoid α] :
SubtractionMonoid αᵒᵈ
Equations
  • OrderDual.subtractionMonoid = h
source
ink
instance instDivisionMonoidOrderDual {α : Type u_1} [h : DivisionMonoid α] :
DivisionMonoid αᵒᵈ
Equations
  • instDivisionMonoidOrderDual = h
source
ink
instance OrderDual.subtractionCommMonoid {α : Type u_1} [h : SubtractionCommMonoid α] :
SubtractionCommMonoid αᵒᵈ
Equations
  • OrderDual.subtractionCommMonoid = h
source
ink
instance instDivisionCommMonoidOrderDual {α : Type u_1} [h : DivisionCommMonoid α] :
DivisionCommMonoid αᵒᵈ
Equations
  • instDivisionCommMonoidOrderDual = h
source
ink
instance instAddGroupOrderDual {α : Type u_1} [h : AddGroup α] :
AddGroup αᵒᵈ
Equations
  • instAddGroupOrderDual = h
source
ink
instance instGroupOrderDual {α : Type u_1} [h : Group α] :
Group αᵒᵈ
Equations
  • instGroupOrderDual = h
source
ink
instance instAddCommGroupOrderDual {α : Type u_1} [h : AddCommGroup α] :
AddCommGroup αᵒᵈ
Equations
  • instAddCommGroupOrderDual = h
source
ink
instance instCommGroupOrderDual {α : Type u_1} [h : CommGroup α] :
CommGroup αᵒᵈ
Equations
  • instCommGroupOrderDual = h
source
ink
@[simp]
theorem toDual_zero {α : Type u_1} [inst : Zero α] :
↑OrderDual.toDual 0 = 0
source
ink
@[simp]
theorem toDual_one {α : Type u_1} [inst : One α] :
↑OrderDual.toDual 1 = 1
source
ink
@[simp]
theorem ofDual_zero {α : Type u_1} [inst : Zero α] :
↑OrderDual.ofDual 0 = 0
source
ink
@[simp]
theorem ofDual_one {α : Type u_1} [inst : One α] :
↑OrderDual.ofDual 1 = 1
source
ink
@[simp]
theorem toDual_add {α : Type u_1} [inst : Add α] (a : α) (b : α) :
↑OrderDual.toDual (a + b) = ↑OrderDual.toDual a + ↑OrderDual.toDual b
source
ink
@[simp]
theorem toDual_mul {α : Type u_1} [inst : Mul α] (a : α) (b : α) :
↑OrderDual.toDual (a * b) = ↑OrderDual.toDual a * ↑OrderDual.toDual b
source
ink
@[simp]
theorem ofDual_add {α : Type u_1} [inst : Add α] (a : αᵒᵈ) (b : αᵒᵈ) :
↑OrderDual.ofDual (a + b) = ↑OrderDual.ofDual a + ↑OrderDual.ofDual b
source
ink
@[simp]
theorem ofDual_mul {α : Type u_1} [inst : Mul α] (a : αᵒᵈ) (b : αᵒᵈ) :
↑OrderDual.ofDual (a * b) = ↑OrderDual.ofDual a * ↑OrderDual.ofDual b
source
ink
@[simp]
theorem toDual_neg {α : Type u_1} [inst : Neg α] (a : α) :
↑OrderDual.toDual (-a) = -↑OrderDual.toDual a
source
ink
@[simp]
theorem toDual_inv {α : Type u_1} [inst : Inv α] (a : α) :
↑OrderDual.toDual a⁻¹ = (↑OrderDual.toDual a)⁻¹
source
ink
@[simp]
theorem ofDual_neg {α : Type u_1} [inst : Neg α] (a : αᵒᵈ) :
↑OrderDual.ofDual (-a) = -↑OrderDual.ofDual a
source
ink
@[simp]
theorem ofDual_inv {α : Type u_1} [inst : Inv α] (a : αᵒᵈ) :
↑OrderDual.ofDual a⁻¹ = (↑OrderDual.ofDual a)⁻¹
source
ink
@[simp]
theorem toDual_sub {α : Type u_1} [inst : Sub α] (a : α) (b : α) :
↑OrderDual.toDual (a - b) = ↑OrderDual.toDual a - ↑OrderDual.toDual b
source
ink
@[simp]
theorem toDual_div {α : Type u_1} [inst : Div α] (a : α) (b : α) :
↑OrderDual.toDual (a / b) = ↑OrderDual.toDual a / ↑OrderDual.toDual b
source
ink
@[simp]
theorem ofDual_sub {α : Type u_1} [inst : Sub α] (a : αᵒᵈ) (b : αᵒᵈ) :
↑OrderDual.ofDual (a - b) = ↑OrderDual.ofDual a - ↑OrderDual.ofDual b
source
ink
@[simp]
theorem ofDual_div {α : Type u_1} [inst : Div α] (a : αᵒᵈ) (b : αᵒᵈ) :
↑OrderDual.ofDual (a / b) = ↑OrderDual.ofDual a / ↑OrderDual.ofDual b
source
ink
@[simp]
theorem toDual_vadd {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α) :
↑OrderDual.toDual (b +ᵥ a) = b +ᵥ ↑OrderDual.toDual a
source
ink
@[simp]
theorem toDual_smul {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α) :
↑OrderDual.toDual (b • a) = b • ↑OrderDual.toDual a
source
ink
@[simp]
theorem toDual_pow {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β) :
↑OrderDual.toDual (a ^ b) = ↑OrderDual.toDual a ^ b
source
ink
@[simp]
theorem ofDual_vadd {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : αᵒᵈ) :
↑OrderDual.ofDual (b +ᵥ a) = b +ᵥ ↑OrderDual.ofDual a
source
ink
@[simp]
theorem ofDual_smul {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : αᵒᵈ) :
↑OrderDual.ofDual (b • a) = b • ↑OrderDual.ofDual a
source
ink
@[simp]
theorem ofDual_pow {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : αᵒᵈ) (b : β) :
↑OrderDual.ofDual (a ^ b) = ↑OrderDual.ofDual a ^ b
source
ink
@[simp]
theorem toDual_smul' {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α) :
↑OrderDual.toDual b • a = b • a
source
ink
@[simp]
theorem toDual_vadd' {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α) :
↑OrderDual.toDual b +ᵥ a = b +ᵥ a
source
ink
@[simp]
theorem pow_toDual {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β) :
a ^ ↑OrderDual.toDual b = a ^ b
source
ink
@[simp]
theorem ofDual_smul' {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : βᵒᵈ) (a : α) :
↑OrderDual.ofDual b • a = b • a
source
ink
@[simp]
theorem ofDual_vadd' {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : βᵒᵈ) (a : α) :
↑OrderDual.ofDual b +ᵥ a = b +ᵥ a
source
ink
@[simp]
theorem pow_ofDual {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : βᵒᵈ) :
a ^ ↑OrderDual.ofDual b = a ^ b

Lexicographical order #

source
ink
instance instZeroLex {α : Type u_1} [h : Zero α] :
Zero (Lex α)
Equations
  • instZeroLex = h
source
ink
instance instOneLex {α : Type u_1} [h : One α] :
One (Lex α)
Equations
  • instOneLex = h
source
ink
instance instAddLex {α : Type u_1} [h : Add α] :
Add (Lex α)
Equations
  • instAddLex = h
source
ink
instance instMulLex {α : Type u_1} [h : Mul α] :
Mul (Lex α)
Equations
  • instMulLex = h
source
ink
instance instNegLex {α : Type u_1} [h : Neg α] :
Neg (Lex α)
Equations
  • instNegLex = h
source
ink
instance instInvLex {α : Type u_1} [h : Inv α] :
Inv (Lex α)
Equations
  • instInvLex = h
source
ink
instance instSubLex {α : Type u_1} [h : Sub α] :
Sub (Lex α)
Equations
  • instSubLex = h
source
ink
instance instDivLex {α : Type u_1} [h : Div α] :
Div (Lex α)
Equations
  • instDivLex = h
source
ink
instance instSMulLex {β : Type u_2} {α : Type u_1} [h : SMul β α] :
SMul β (Lex α)
Equations
  • instSMulLex = h
source
ink
instance instVAddLex {β : Type u_2} {α : Type u_1} [h : VAdd β α] :
VAdd β (Lex α)
Equations
  • instVAddLex = h
source
ink
instance instPowLex {α : Type u_1} {β : Type u_2} [h : Pow α β] :
Pow (Lex α) β
Equations
  • instPowLex = h
source
ink
instance instSMulLex' {β : Type u_2} {α : Type u_1} [h : SMul β α] :
SMul (Lex β) α
Equations
  • instSMulLex' = h
source
ink
instance instVAddLex' {β : Type u_2} {α : Type u_1} [h : VAdd β α] :
VAdd (Lex β) α
Equations
  • instVAddLex' = h
source
ink
instance instPowLex' {α : Type u_1} {β : Type u_2} [h : Pow α β] :
Pow α (Lex β)
Equations
  • instPowLex' = h
source
ink
instance instAddSemigroupLex {α : Type u_1} [h : AddSemigroup α] :
AddSemigroup (Lex α)
Equations
  • instAddSemigroupLex = h
source
ink
instance instSemigroupLex {α : Type u_1} [h : Semigroup α] :
Semigroup (Lex α)
Equations
  • instSemigroupLex = h
source
ink
instance instAddCommSemigroupLex {α : Type u_1} [h : AddCommSemigroup α] :
AddCommSemigroup (Lex α)
Equations
  • instAddCommSemigroupLex = h
source
ink
instance instCommSemigroupLex {α : Type u_1} [h : CommSemigroup α] :
CommSemigroup (Lex α)
Equations
  • instCommSemigroupLex = h
source
ink
instance instAddLeftCancelSemigroupLex {α : Type u_1} [h : AddLeftCancelSemigroup α] :
AddLeftCancelSemigroup (Lex α)
Equations
  • instAddLeftCancelSemigroupLex = h
source
ink
instance instLeftCancelSemigroupLex {α : Type u_1} [h : LeftCancelSemigroup α] :
LeftCancelSemigroup (Lex α)
Equations
  • instLeftCancelSemigroupLex = h
source
ink
instance instAddRightCancelSemigroupLex {α : Type u_1} [h : AddRightCancelSemigroup α] :
AddRightCancelSemigroup (Lex α)
Equations
  • instAddRightCancelSemigroupLex = h
source
ink
instance instRightCancelSemigroupLex {α : Type u_1} [h : RightCancelSemigroup α] :
RightCancelSemigroup (Lex α)
Equations
  • instRightCancelSemigroupLex = h
source
ink
instance instAddZeroClassLex {α : Type u_1} [h : AddZeroClass α] :
AddZeroClass (Lex α)
Equations
  • instAddZeroClassLex = h
source
ink
instance instMulOneClassLex {α : Type u_1} [h : MulOneClass α] :
MulOneClass (Lex α)
Equations
  • instMulOneClassLex = h
source
ink
instance instAddMonoidLex {α : Type u_1} [h : AddMonoid α] :
AddMonoid (Lex α)
Equations
  • instAddMonoidLex = h
source
ink
instance instMonoidLex {α : Type u_1} [h : Monoid α] :
Monoid (Lex α)
Equations
  • instMonoidLex = h
source
ink
instance instAddCommMonoidLex {α : Type u_1} [h : AddCommMonoid α] :
AddCommMonoid (Lex α)
Equations
  • instAddCommMonoidLex = h
source
ink
instance instCommMonoidLex {α : Type u_1} [h : CommMonoid α] :
CommMonoid (Lex α)
Equations
  • instCommMonoidLex = h
source
ink
instance instAddLeftCancelMonoidLex {α : Type u_1} [h : AddLeftCancelMonoid α] :
AddLeftCancelMonoid (Lex α)
Equations
  • instAddLeftCancelMonoidLex = h
source
ink
instance instLeftCancelMonoidLex {α : Type u_1} [h : LeftCancelMonoid α] :
LeftCancelMonoid (Lex α)
Equations
  • instLeftCancelMonoidLex = h
source
ink
instance instAddRightCancelMonoidLex {α : Type u_1} [h : AddRightCancelMonoid α] :
AddRightCancelMonoid (Lex α)
Equations
  • instAddRightCancelMonoidLex = h
source
ink
instance instRightCancelMonoidLex {α : Type u_1} [h : RightCancelMonoid α] :
RightCancelMonoid (Lex α)
Equations
  • instRightCancelMonoidLex = h
source
ink
instance instAddCancelMonoidLex {α : Type u_1} [h : AddCancelMonoid α] :
AddCancelMonoid (Lex α)
Equations
  • instAddCancelMonoidLex = h
source
ink
instance instCancelMonoidLex {α : Type u_1} [h : CancelMonoid α] :
CancelMonoid (Lex α)
Equations
  • instCancelMonoidLex = h
source
ink
instance instAddCancelCommMonoidLex {α : Type u_1} [h : AddCancelCommMonoid α] :
AddCancelCommMonoid (Lex α)
Equations
  • instAddCancelCommMonoidLex = h
source
ink
instance instCancelCommMonoidLex {α : Type u_1} [h : CancelCommMonoid α] :
CancelCommMonoid (Lex α)
Equations
  • instCancelCommMonoidLex = h
source
ink
instance instInvolutiveNegLex {α : Type u_1} [h : InvolutiveNeg α] :
InvolutiveNeg (Lex α)
Equations
  • instInvolutiveNegLex = h
source
ink
instance instInvolutiveInvLex {α : Type u_1} [h : InvolutiveInv α] :
InvolutiveInv (Lex α)
Equations
  • instInvolutiveInvLex = h
source
ink
instance instSubNegAddMonoidLex {α : Type u_1} [h : SubNegMonoid α] :
SubNegMonoid (Lex α)
Equations
  • instSubNegAddMonoidLex = h
source
ink
instance instDivInvMonoidLex {α : Type u_1} [h : DivInvMonoid α] :
DivInvMonoid (Lex α)
Equations
  • instDivInvMonoidLex = h
source
ink
instance instDivisionMonoidLex {α : Type u_1} [h : DivisionMonoid α] :
DivisionMonoid (Lex α)
Equations
  • instDivisionMonoidLex = h
source
ink
instance instDivisionCommMonoidLex {α : Type u_1} [h : DivisionCommMonoid α] :
DivisionCommMonoid (Lex α)
Equations
  • instDivisionCommMonoidLex = h
source
ink
instance instAddGroupLex {α : Type u_1} [h : AddGroup α] :
AddGroup (Lex α)
Equations
  • instAddGroupLex = h
source
ink
instance instGroupLex {α : Type u_1} [h : Group α] :
Group (Lex α)
Equations
  • instGroupLex = h
source
ink
instance instAddCommGroupLex {α : Type u_1} [h : AddCommGroup α] :
AddCommGroup (Lex α)
Equations
  • instAddCommGroupLex = h
source
ink
instance instCommGroupLex {α : Type u_1} [h : CommGroup α] :
CommGroup (Lex α)
Equations
  • instCommGroupLex = h
source
ink
@[simp]
theorem toLex_zero {α : Type u_1} [inst : Zero α] :
↑toLex 0 = 0
source
ink
@[simp]
theorem toLex_one {α : Type u_1} [inst : One α] :
↑toLex 1 = 1
source
ink
@[simp]
theorem ofLex_zero {α : Type u_1} [inst : Zero α] :
↑ofLex 0 = 0
source
ink
@[simp]
theorem ofLex_one {α : Type u_1} [inst : One α] :
↑ofLex 1 = 1
source
ink
@[simp]
theorem toLex_add {α : Type u_1} [inst : Add α] (a : α) (b : α) :
↑toLex (a + b) = ↑toLex a + ↑toLex b
source
ink
@[simp]
theorem toLex_mul {α : Type u_1} [inst : Mul α] (a : α) (b : α) :
↑toLex (a * b) = ↑toLex a * ↑toLex b
source
ink
@[simp]
theorem ofLex_add {α : Type u_1} [inst : Add α] (a : Lex α) (b : Lex α) :
↑ofLex (a + b) = ↑ofLex a + ↑ofLex b
source
ink
@[simp]
theorem ofLex_mul {α : Type u_1} [inst : Mul α] (a : Lex α) (b : Lex α) :
↑ofLex (a * b) = ↑ofLex a * ↑ofLex b
source
ink
@[simp]
theorem toLex_neg {α : Type u_1} [inst : Neg α] (a : α) :
↑toLex (-a) = -↑toLex a
source
ink
@[simp]
theorem toLex_inv {α : Type u_1} [inst : Inv α] (a : α) :
↑toLex a⁻¹ = (↑toLex a)⁻¹
source
ink
@[simp]
theorem ofLex_neg {α : Type u_1} [inst : Neg α] (a : Lex α) :
↑ofLex (-a) = -↑ofLex a
source
ink
@[simp]
theorem ofLex_inv {α : Type u_1} [inst : Inv α] (a : Lex α) :
↑ofLex a⁻¹ = (↑ofLex a)⁻¹
source
ink
@[simp]
theorem toLex_sub {α : Type u_1} [inst : Sub α] (a : α) (b : α) :
↑toLex (a - b) = ↑toLex a - ↑toLex b
source
ink
@[simp]
theorem toLex_div {α : Type u_1} [inst : Div α] (a : α) (b : α) :
↑toLex (a / b) = ↑toLex a / ↑toLex b
source
ink
@[simp]
theorem ofLex_sub {α : Type u_1} [inst : Sub α] (a : Lex α) (b : Lex α) :
↑ofLex (a - b) = ↑ofLex a - ↑ofLex b
source
ink
@[simp]
theorem ofLex_div {α : Type u_1} [inst : Div α] (a : Lex α) (b : Lex α) :
↑ofLex (a / b) = ↑ofLex a / ↑ofLex b
source
ink
@[simp]
theorem toLex_smul {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α) :
↑toLex (b • a) = b • ↑toLex a
source
ink
@[simp]
theorem toLex_vadd {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α) :
↑toLex (b +ᵥ a) = b +ᵥ ↑toLex a
source
ink
@[simp]
theorem toLex_pow {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β) :
↑toLex (a ^ b) = ↑toLex a ^ b
source
ink
@[simp]
theorem ofLex_smul {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : Lex α) :
↑ofLex (b • a) = b • ↑ofLex a
source
ink
@[simp]
theorem ofLex_vadd {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : Lex α) :
↑ofLex (b +ᵥ a) = b +ᵥ ↑ofLex a
source
ink
@[simp]
theorem ofLex_pow {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : Lex α) (b : β) :
↑ofLex (a ^ b) = ↑ofLex a ^ b
source
ink
@[simp]
theorem toLex_smul' {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α) :
↑toLex b • a = b • a
source
ink
@[simp]
theorem toLex_vadd' {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α) :
↑toLex b +ᵥ a = b +ᵥ a
source
ink
@[simp]
theorem pow_toLex {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β) :
a ^ ↑toLex b = a ^ b
source
ink
@[simp]
theorem ofLex_vadd' {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : Lex β) (a : α) :
↑ofLex b +ᵥ a = b +ᵥ a
source
ink
@[simp]
theorem ofLex_smul' {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : Lex β) (a : α) :
↑ofLex b • a = b • a
source
ink
@[simp]
theorem pow_ofLex {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : Lex β) :
a ^ ↑ofLex b = a ^ b