Add/Mul equivalence for order type synonyms

def toLexMulEquiv (α : Type u_1) [Mul α] : α ≃* Lex α

toLex as a MulEquiv.

Equations

• toLexMulEquiv α = { toEquiv := toLex, map_mul' := ⋯ }

def toLexAddEquiv (α : Type u_1) [Add α] : α ≃+ Lex α

toLex as an AddEquiv.

Equations

• toLexAddEquiv α = { toEquiv := toLex, map_add' := ⋯ }

def ofLexMulEquiv (α : Type u_1) [Mul α] : Lex α ≃* α

ofLex as a MulEquiv.

Equations

• ofLexMulEquiv α = { toEquiv := ofLex, map_mul' := ⋯ }

def ofLexAddEquiv (α : Type u_1) [Add α] : Lex α ≃+ α

ofLex as an AddEquiv.

Equations

• ofLexAddEquiv α = { toEquiv := ofLex, map_add' := ⋯ }

@[simp]

theorem coe_toLexMulEquiv (α : Type u_1) [Mul α] : ⇑(toLexMulEquiv α) = ⇑toLex

@[simp]

theorem coe_toLexAddEquiv (α : Type u_1) [Add α] : ⇑(toLexAddEquiv α) = ⇑toLex

@[simp]

theorem coe_ofLexMulEquiv (α : Type u_1) [Mul α] : ⇑(ofLexMulEquiv α) = ⇑ofLex

@[simp]

theorem coe_ofLexAddEquiv (α : Type u_1) [Add α] : ⇑(ofLexAddEquiv α) = ⇑ofLex

@[simp]

theorem symm_toLexMulEquiv (α : Type u_1) [Mul α] : (toLexMulEquiv α).symm = ofLexMulEquiv α

@[simp]

theorem symm_toLexAddEquiv (α : Type u_1) [Add α] : (toLexAddEquiv α).symm = ofLexAddEquiv α

@[simp]

theorem symm_ofLexMulEquiv (α : Type u_1) [Mul α] : (ofLexMulEquiv α).symm = toLexMulEquiv α

@[simp]

theorem symm_ofLexAddEquiv (α : Type u_1) [Add α] : (ofLexAddEquiv α).symm = toLexAddEquiv α

@[simp]

theorem toEquiv_toLexMulEquiv (α : Type u_1) [Mul α] : ↑(toLexMulEquiv α) = toLex

@[simp]

theorem toEquiv_toLexAddEquiv (α : Type u_1) [Add α] : ↑(toLexAddEquiv α) = toLex

@[simp]

theorem toEquiv_ofLexMulEquiv (α : Type u_1) [Mul α] : ↑(ofLexMulEquiv α) = ofLex

@[simp]

theorem toEquiv_ofLexAddEquiv (α : Type u_1) [Add α] : ↑(ofLexAddEquiv α) = ofLex