Linear equivalence for order type synonyms

def toLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] : β ≃ₗ[α] Lex β

toLex as a linear equivalence

Equations

• toLexLinearEquiv α β = (toLexAddEquiv β).toLinearEquiv ⋯

def ofLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] : Lex β ≃ₗ[α] β

ofLex as a linear equivalence

Equations

• ofLexLinearEquiv α β = (ofLexAddEquiv β).toLinearEquiv ⋯

@[simp]

theorem coe_toLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] : ⇑(toLexLinearEquiv α β) = ⇑toLex

@[simp]

theorem coe_ofLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] : ⇑(ofLexLinearEquiv α β) = ⇑ofLex

@[simp]

theorem symm_toLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] : (toLexLinearEquiv α β).symm = ofLexLinearEquiv α β

@[simp]

theorem symm_ofLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] : (ofLexLinearEquiv α β).symm = toLexLinearEquiv α β