Documentation

Mathlib.Algebra.Order.Module.Equiv

Linear equivalence for order type synonyms #

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

toLex as a linear equivalence

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

      ofLex as a linear equivalence

      Equations
        Instances For
          source
          @[simp]
          theorem coe_toLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] :
          ⇑(toLexLinearEquiv α β) = ⇑toLex
          source
          @[simp]
          theorem coe_ofLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] :
          ⇑(ofLexLinearEquiv α β) = ⇑ofLex
          source
          @[simp]
          theorem symm_toLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] :
          (toLexLinearEquiv α β).symm = ofLexLinearEquiv α β
          source
          @[simp]
          theorem symm_ofLexLinearEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] :
          (ofLexLinearEquiv α β).symm = toLexLinearEquiv α β